Логіка першого порядку — Вікіпедія
Логіка першого порядку (числення предикатів) — це формальна система в математичній логіці, в якій допускаються висловлення відносно змінних, фіксованих функцій, і предикатів. Є розширенням логіки висловлювань. В свою чергу є частковим випадком логіки вищого порядку[en].
Визначення[ред. | ред. код]
Мови логіки першого порядку будуються на основі сигнатури, що складається із множини функціональних символів і множини предикатних символів . З кожним функціональним і предикатним символом пов'язана арність (число агрументів). Крім того використовуються додаткові символи:
- Символи змінних, зазвичай і т. д.,
- Пропозиційні зв'язки: ,
- Квантори: загальності та існування ,
- Службові символи: дужки і кома.
Перелічені символи разом із символами з і утворюють Алфавіт логіки першого порядку. Складніші конструкції визначаються індуктивно:
- Терм — це символ змінної, або має вид , де — функціональний символ арності , а — терми.
- Атом — має вид , де — предикатний символ арності , а — атоми.
- Формула — це або атом, або одна з наступних конструкцій: , де — формули, а — змінна.
Змінна називається зв'язаною в формулі , якщо має вид або , або може бути представлена в одній з форм , причому вже зв'язана в , і .
Якщо не зв'язана в , її називають незв'язаною в . Формулу без незв'язаних змінних називають замкнутою формулою. Теорією першого порядку називають довільну множину замкнутих формул.
Аксіоматика[ред. | ред. код]
Наступна система логічних аксіом логіки першого порядку містить усі аксіоми числення висловлень (у наведеному випадку — аксіоми Лукашевича) та дві додаткові аксіоми:
- ,
- , якщо не присутній в в незвязаному стані
У четвертій аксіомі — формула, одержана внаслідок підстановки терма замість змінної в формулі . Підстановка деякого терма замість змінної можлива не в усіх випадках. Умови існування такої підстановки та її результат можна визначити індуктивно.
- Якщо — атомарна формула, то терм може замінити довільну змінну цієї формули. Результат позначається .
- Якщо має вигляд тоді підстановка замість можлива лише тоді, коли така підстановка можлива для формули і тоді дорівнює
- Якщо має вигляд , тоді підстановка замість можлива лише тоді, коли така підстановка можлива для формул і тоді рівна
- Якщо має вигляд , тоді підстановка замість можлива у двох випадках:
- Змінна зустрічається у формулі лише у зв'язаному стані.
- змінна не зустрічається у термі і підстановка замість можлива у формулі Тоді результат визначається наступним чином:
- Якщо дорівнює , то дорівнює
- Якщо не дорівнює , то дорівнює
Окрім того є два правила виводу:
- Modus ponens:
- Правило узагальнення (GEN):
Ці аксіоми і правила виводу є схемами і можна заміняти довільними формулами.
В цій аксіоматиці використовуються лише дві пропозиційні зв'язки: і квантор загальності . Інші пропозиційні зв'язки і квантор існування можна визначити наступним чином:
- позначає
- позначає
- позначає
Усі наведені вище аксіоми називаються логічними. Якщо не існує інших аксіом, то таку формальну систему називають численням предикатів першого порядку. Числення предикатів першого порядку є прикладом теорії першого порядку. Усі теорії першого порядку визначаються подібно до числення предикатів першого порядку, однак вони мають додаткові аксіоми, які ще називають власними аксіомами теорії.
Виведення формул і теорем[ред. | ред. код]
Нехай деяка множина формул мови першого порядку, а — деяка задана формула. Тоді кажуть, що формула виводиться з множини формул (позначається ), якщо існує така скінченна послідовність формул , де для кожної формули :
- є аксіомою, або
- належить множині або
- виводиться з попередніх формул послідовності за допомогою котрогось із правил виводу.
Якщо при цьому множина — порожня (формула виводиться лише за допомогою аксіом і правил виводу), то формула називається теоремою (для цього використовується позначення ).
Множина формул називається несуперечливою, якщо для довільної формули не виконується одночасно і .
Приклад виведення[ред. | ред. код]
Доведемо, що
Приклад виводу | ||
---|---|---|
Номер | Формула | Спосіб одержання |
1 | Гіпотеза | |
2 | Правило узагальнення і 1 | |
3 | Гіпотеза | |
4 | 2, 3 і modus ponens | |
5 | Правило узагальнення і 4. |
Приклади теорій першого порядку[ред. | ред. код]
Теорія груп[ред. | ред. код]
У цьому випадку маємо один функціональний символ арності 0 (позначимо його ), один функціональний символ арності 2 (позначимо його ) і один предикатний символ арності 2 (позначимо його ). Також писатимемо і замість і .
Власні формули теорії:
- (властивість асоціативності)
- (властивість нейтрального елемента)
- (існування оберненого елемента)
- (рефлексивність рівності)
- (симетричність рівності)
- (транзитивність рівності)
- (підстановка рівності)
Теорія абелевих груп[ред. | ред. код]
Використовуються усі позначення і аксіоми попереднього пункту, а також додаткова аксіома комутативності:
Семантика[ред. | ред. код]
У класичній логіці інтерпретація формул логіки першого порядку задається на моделі першого порядку, яка визначається такими даними:
- Базова множина[en] ,
- Семантична функція , що відображає
- кожен -арний функціональний символ із в -арну функцію ,
- кожен -арний предикатний символ із в -арне відношення .
Припустимо — функція, що відображає кожну змінну в деякий елемент із , яку і називатимемо підстановкою. Інтерпретація терму на відносно підстановки задається індуктивно:
- , якщо — змінна,
Подібним чином визначається істинність формул на відносно
- , тоді і тільки тоді коли ,
- , тоді і тільки тоді коли — хибно,
- , тоді і тільки тоді коли і істинні,'
- , тоді і тільки тоді коли або істинно,
- , тоді і тільки тоді коли з випливає ,
- , тоді і тільки тоді коли для деякої підстановки , яка відрізняється від тільки на змінній ,
- , тоді і тільки тоді коли для всіх підстановок , які відрізняються від тільки на змінній .
Формула , істинна на , що позначається , якщо , для всіх підстановок . Формула називається загальнозначимою, (позначається ), якщо для всіх моделей . Формула називається виконуваною , якщо хоча б для однієї .
Властивості[ред. | ред. код]
Коректність і повнота[ред. | ред. код]
Наведена вище система аксіом і правил виводу є коректною, тобто для будь-якої множини формул із випливає . Також дана система є повною: із випливає . Зокрема, з цих тверджень випливає, що для числення предикатів першого порядку загальнозначимі формули збігаються із теоремами формальної системи. Також у будь-якій теорії першого порядку всі виведені у ній формули збігаються з формулами, істинними в усіх моделях цієї теорії.
Компактність[ред. | ред. код]
Деяка множина формул є виконуваною тоді і тільки тоді, коли виконуваними є всі її скінченні підмножини.
Нерозв'язність[ред. | ред. код]
На відміну від логіки висловлень логіка першого порядку є нерозв'язною у разі наявності принаймні одного предиката арності не менше 2 (за винятком рівності), тобто немає ефективного методу визначення «існує чи не існує виведення деякої формули?» у певній теорії першого порядку.
Див. також[ред. | ред. код]
- Логіка предикатів
- Числення висловлень
- Предикатна логіка
- Квантор
- Правило резолюцій
- Числення секвенцій
- Логіка другого порядку
- Теорема Льовенгейма—Сколема
- Нормальна форма Сколема
Література[ред. | ред. код]
- Силогістика // Філософський енциклопедичний словник / В. І. Шинкарук (гол. редкол.) та ін. — Київ : Інститут філософії імені Григорія Сковороди НАН України : Абрис, 2002. — С. 578. — 742 с. — 1000 екз. — ББК 87я2. — ISBN 966-531-128-X.
- Числення предикатів // ФЕС, с.714
- Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947
- Клини С. К. Введение в метаматематику. М., 1957
- Мендельсон Э. Введение в математическую логику. М., 1976
- Новиков П. С. Элементы математической логики. М., 1959
- Черч А. Введение в математическую логику, т. I. М. 1960
- Філософський словник / за ред. В. І. Шинкарука. — 2-ге вид., перероб. і доп. — К. : Головна ред. УРЕ, 1986.
|