Логіка першого порядку

Логіка першого порядку (числення предикатів) — це формальна система в математичній логіці, в якій допускаються висловлення відносно змінних, фіксованих функцій, і предикатів. Є розширенням логіки висловлювань. В свою чергу є частковим випадком логіки вищого порядку (англ.).

Визначення

Мови логіки першого порядку будуються на основі: множини функціональних символів $\mathcal{F}$ і множини предикатних символів $\mathcal{P}$. З кожним функціональним і предикатним символом пов'язана арність (число агрументів). Крім того використовуються додаткові символи:

• Символи змінних, зазвичай $\ x, y, z, x_1, y_1, z_1, x_2, y_2, z_2,$ і т. д.,
• Пропозиційні зв'язки: $\lor,\land,\neg,\to$,
• Квантори: загальності $\forall$ та існування $\exists$,
• Службові символи: дужки і кома.

Перелічені символи разом із символами з $\mathcal{P}$ і $\mathcal{F}$ утворюють Алфавіт логіки першого порядку. Складніші конструкції визначаються індуктивно:

• Терм — це символ змінної, або має вид $\ f(t_1,\ldots,t_n)$, де $\ f$ — функціональний символ арності $\ n$, а $\ t_1,\ldots,t_n$ — терми.
• Атом — має вид $\ p(t_1,\ldots,t_n)$, де $p$ — предикатний символ арності $\ n$, а $\ t_1,\ldots,t_n$ — терми.
• Формула — це або атом, або одна з наступних конструкцій: $\neg F, (F_1\lor F_2), (F_1\land F_2), (F_1\to F_2), \forall x F, \exists x F$, де $\ F, F_1, F_2$ — формули, а $\ x$ — змінна.

Змінна $\ x$ називається зв'язаною в формулі $\ F$, якщо $\ F$ має вид $\forall x G$ або $\exists x G$, або може бути представлена в одній з форм $\neg H, (F_1\lor F_2), (F_1\land F_2), (F_1\to F_2)$, причому $\ x$ вже зв'язана в $H$, $F_1$ і $F_2$.

Якщо $\ x$ не зв'язана в $\ F$, її називають незв'язаною в $\ F$. Формулу без незв'язаних змінних називають замкнутою формулою. Теорією першого порядку називають довільну множину замкнутих формул.

Аксіоматика

Наступна система логічних аксіом логіки першого порядку містить усі аксіоми числення висловлень (у наведеному випадку — аксіоми Лукасевича) та дві додаткові аксіоми:

1. $(A \to (B \to C))$
2. $((A \to (B \to C)) \to ((A \to B) \to (A \to C)))$
3. $((\neg A \to \neg B) \to (B \to A))$
4. $\forall x A \to A[t/x]$,
5. $\forall x (A \to B)\to (A \to \forall x B)$, якщо $x\;$ не присутній в $A\;$ в незвязаному стані

У четвертій аксіомі $A[t/x]\;$ — формула, одержана внаслідок підстановки терма $t\;$ замість змінної $x$ в формулі $A\;$. Підстановка деякого терма замість змінної можлива не в усіх випадках. Умови існування такої підстановки та її результат можна визначити індуктивно.

• Якщо $A$ — атомарна формула, то терм $t\;$ може замінити довільну змінну $x\;$ цієї формули. Результат позначається $A[t/x]\;$.
• Якщо $A\;$ має вигляд $\lnot B$ тоді підстановка $t\;$ замість $x\;$ можлива лише тоді, коли така підстановка можлива для формули $B\;$ і $A[t/x]\;$ тоді дорівнює $\lnot B[t/x].$
• Якщо $A$ має вигляд $B \to C$, тоді підстановка $t\;$ замість $x\;$ можлива лише тоді, коли така підстановка можлива для формул $B\;$ і $C.\;$ $A[t/x]\;$ тоді рівна $B[t/x] \to C[t/x].$
• Якщо $A\;$ має вигляд $\forall y B$, тоді підстановка $t\;$ замість $x\;$ можлива у двох випадках:
  • Змінна $x\;$ зустрічається у формулі $B\;$ лише у зв'язаному стані.
  • змінна $y\;$ не зустрічається у термі $t\;$ і підстановка $t\;$ замість $x\;$ можлива у формулі $B.\;$ Тоді результат визначається наступним чином:
  • Якщо $x\;$ дорівнює $y$, то $A[t/x]\;$ дорівнює $\forall y B$
  • Якщо $x\;$ не дорівнює $y\;$, то $A[t/x]\;$ дорівнює $\forall y B[t/x]$

Окрім того є два правила виводу:

• Modus ponens:

  $\frac{A, A \to B}{B}$

• Правило узагальнення (GEN):

  $\frac{A}{\forall x A}$

Ці аксіоми і правила виводу є схемами і $A, B, C$ можна заміняти довільними формулами.

В цій аксіоматиці використовуються лише дві пропозиційні зв'язки: $\neg,\to$ і квантор загальності $\forall$. Інші пропозиційні зв'язки і квантор існування можна визначити наступним чином:

• $(A \lor B)$ позначає $(\lnot (A \to (\lnot B)))$
• $(A \land B)$ позначає $((\lnot A) \to B)$
• $(\exists x A)$ позначає $(\lnot \forall x (\lnot A))$

Усі наведені вище аксіоми називаються логічними. Якщо не існує інших аксіом, то таку формальну систему називають численням предикатів першого порядку. Числення предикатів першого порядку є прикладом теорії першого порядку. Усі теорії першого порядку визначаються подібно до числення предикатів першого порядку, однак вони мають додаткові аксіоми, які ще називають власними аксомами теорії.

Виведення формул і теорем

Нехай $\Sigma\;$ деяка множина формул мови першого порядку, а $A\;$ — деяка задана формула. Тоді кажуть, що формула $A\;$ виводиться з множини формул $\Sigma\;$ (позначається $\Sigma \vdash A$), якщо існує така скінченна послідовність формул $A_1, A_2 \ldots A_n = A$, де для кожної формули $A_i\;$:

1. $A_i$ є аксіомою, або
2. $A_i$ належить множині $\Sigma\;$ або
3. $A_i$ виводиться з попередніх формул послідовності за допомогою котрогось із правил виводу.

Якщо при цьому множина $\Sigma\;$ — порожня (формула $A$ виводиться лише за допомогою аксіом і правил виводу), то формула $A$ називається теоремою (для цього використовується позначення $\vdash A$).

Множина $\Sigma\;$ формул називається несуперечливою, якщо для довільної формули $A\;$ не виконується одночасно $\Sigma \vdash A$ і $\Sigma \vdash \lnot A$.

Приклад виведення

Доведемо, що $A, (\forall x A to B) \vdash \forall x B$

Приклад виводу
Номер	Формула	Спосіб одержання
1	$A$	Гіпотеза
2	$\forall x A$	Правило узагальнення і 1
3	$\forall x A \to B$	Гіпотеза
4	$B$	2, 3 і modus ponens
5	$\forall x B$	Правило узагальнення і 4.

Приклади теорій першого порядку

Теорія груп

У цьому випадку маємо один функціональний символ арності 0 (позначимо його $e$), один функціональний символ арності 2 (позначимо його $\circ$) і один предикатний символ арності 2 (позначимо його $=$). Також писатимемо $x = y$ і $x \circ y$ замість $=(x,y)$ і $\circ (x,y)$.

Власні формули теорії:

1. $\forall x \forall y \forall z (x\circ (y\circ z)=(x\circ y)\circ z)$ (асоціативність)
2. $\forall x (e \circ x= x$ (властивість нейтрального елемента)
3. $\forall x \exists y (x \circ y = e)$ (існування оберненого елемента)
4. $\forall x (x = x)$ (рефлексивність рівності)
5. $\forall x \forall y (x = y \to y = x)$ (симетричність рівності)
6. $\forall x \forall y \forall z (x = y \to (y = z \to x = z))$ (транзитивність рівності)
7. $\forall x \forall y \forall z (x = y \to (z \circ x = z \circ y \land x \circ z = y \circ z))$ (підстановка рівності)

Теорія абелевих груп

Використовуються усі позначення і аксіоми попереднього пункту, а також додаткова аксіома комутативності:

$\forall x \forall y (x \circ y = y \circ x)$

Семантика

У класичній логіці інтерпретація формул логіки першого порядку задається на моделі першого порядку, яка визначається такими даними:

• Базова множина $\mathcal{D}$,
• Семантична функція $\sigma$, що відображає
  • кожен $n$-арний функціональний символ $f$ із $\mathcal{F}$ в $n$-арну функцію $\sigma(f):\mathcal{D}\times\ldots\times\mathcal{D}\rightarrow\mathcal{D}$,
  • кожен $n$-арний предикатний символ $p$ із $\mathcal{P}$ в $n$-арне відношення $\sigma(p)\subseteq\mathcal{D}\times\ldots\times\mathcal{D}$.

Припустимо $s$ — функція, що відображає кожну змінну в деякий елемент із $\mathcal{D}$, яку і називатимемо підстановкою. Інтерпретація $[\![t]\!]_s$ терма $t$ на$\mathcal{D}$ відносно підстановки $s$ задається індуктивно:

• $[\![x]\!]_s = s(x)$, якщо $x$ — змінна,
• $[\![f(x_1,\ldots,x_n)]\!]_s = \sigma(f)(\![x_1]\!]_s,\ldots,\![x_n]\!]_s)$

Подібним чином визначається істинність $\models_s$ формул на $\mathcal{D}$ відносно $s$

• $\mathcal{D}\models_s p(t_1,\ldots,t_n)$, тоді і тільки тоді коли $\sigma(p)( \![x_1]\!]_s,\ldots,\![x_n]\!]_s)$,
• $\mathcal{D}\models_s \neg\phi$, тоді і тільки тоді коли $\mathcal{D}\models_s \phi$ — хибно,
• $\mathcal{D}\models_s \phi\land\psi$, тоді і тільки тоді коли $\mathcal{D}\models_s \phi$ і $\mathcal{D}\models_s \psi$ істинні,'
• $\mathcal{D}\models_s \phi\lor\psi$, тоді і тільки тоді коли $\mathcal{D}\models_s \phi$ або $\mathcal{D}\models_s \psi$ істинно,
• $\mathcal{D}\models_s \phi\to\psi$, тоді і тільки тоді коли з $\mathcal{D}\models_s \phi$ випливає $\mathcal{D}\models_s \psi$,
• $\mathcal{D}\models_s \exists x\, \phi$, тоді і тільки тоді коли $\mathcal{D}\models_{s'} \phi$ для деякої підстановки $s'$, яка відрізняється від $s$ тільки на змінній $x$,
• $\mathcal{D}\models_s \forall x\, \phi$, тоді і тільки тоді коли $\mathcal{D}\models_{s'} \phi$ для всіх підстановок $s'$, які відрізняються від $s$ тільки на змінній $x$.

Формула $\phi$, істинна на $\mathcal{D}$, що позначається $\mathcal{D}\models \phi$, якщо $\mathcal{D}\models_s \phi$, для всіх підстановок $s$. Формула $\phi$ називається загальнозначимою, (позначається $\models \phi$), якщо $\mathcal{D}\models \phi$ для всіх моделей $\mathcal{D}$. Формула $\phi$ називається виконуваною , якщо $\mathcal{D}\models \phi$ хоча б для однієї $\mathcal{D}$.

Властивості

Коректність і повнота

Подана вище система аксіом і правил виводу є коректною, тобто для будь-якої множини формул $\Sigma\;$ із $\Sigma \vdash A$ випливає $\Sigma \vDash A$. Також дана система є повною: із $\Sigma \vDash A$ випливає $\Sigma \vdash A$. Зокрема, з цих тверджень випливає, що для числення предикатів першого порядку загальнозначимі формули збігаються із теоремами формальної системи. Також у будь-якій теорії першого порядку всі виведені у ній формули збігаються з формулами, істинними в усіх моделях цієї теорії.

Компактність

Деяка множина формул є виконуваною тоді і тільки тоді, коли виконуваними є всі її скінченні підмножини.

Нерозв'язність

На відміну від логіки висловлень логіка першого порядку є нерозв'язною у разі наявності принаймі одного предиката арності не менше 2 (за винятком рівності), тобто немає ефективного методу визначення «існує чи не існує виведення деякої формули?» у певній теорії першого порядку.

Див. також

• Числення висловлень
• Квантор
• Правило резолюцій
• Числення секвенцій
• Логіка другого порядку
• Теорема Льовенгейма—Сколема
• Нормальна форма Сколема

Література

• Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947
• Клини С. К. Введение в метаматематику. М., 1957
• Мендельсон Э. Введение в математическую логику. М., 1976
• Новиков П. С. Элементы математической логики. М., 1959
• Черч А. Введение в математическую логику, т. I. М. 1960
• «Філософський словник» / За ред. В. І. Шинкарука. — 2.вид., перероб. і доп. — К.: Голов. Ред. УРЕ, 1986.