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

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

Визначення

Мови логіки першого порядку будуються на основі сигнатури, що складається із множини функціональних символів ${\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 xF,\exists xF$, де $\ F,F_{1},F_{2}$ — формули, а $\ x$ — змінна.

Змінна $\ x$ називається зв'язаною в формулі $\ F$, якщо $\ F$ має вид $\forall xG$ або $\exists xG$, або може бути представлена в одній з форм $\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 A))$
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 xA\to A[t/x]$,
5. $\forall x(A\to B)\to (A\to \forall xB)$, якщо $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 yB$, тоді підстановка $t\;$ замість $x\;$ можлива у двох випадках:
  • Змінна $x\;$ зустрічається у формулі $B\;$ лише у зв'язаному стані.
  • змінна $y\;$ не зустрічається у термі $t\;$ і підстановка $t\;$ замість $x\;$ можлива у формулі $B.\;$ Тоді результат визначається наступним чином:
  • Якщо $x\;$ дорівнює $y$, то $A[t/x]\;$ дорівнює $\forall yB$
  • Якщо $x\;$ не дорівнює $y\;$, то $A[t/x]\;$ дорівнює $\forall yB[t/x]$

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

• Modus ponens:

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

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

  ${\frac {A}{\forall xA}}$

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

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

• $(A\lor B)$ позначає $(\lnot (A\to (\lnot B)))$
• $(A\land B)$ позначає $((\lnot A)\to B)$
• $(\exists xA)$ позначає $(\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 xA\to B)\vdash \forall xB$

Приклад виводу
Номер	Формула	Спосіб одержання
1	$A$	Гіпотеза
2	$\forall xA$	Правило узагальнення і 1
3	$\forall xA\to B$	Гіпотеза
4	$B$	2, 3 і modus ponens
5	$\forall xB$	Правило узагальнення і 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 (за винятком рівності), тобто немає ефективного методу визначення «існує чи не існує виведення деякої формули?» у певній теорії першого порядку.

Див. також

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

Література

• Силогістика // Філософський енциклопедичний словник / В. І. Шинкарук (гол. редкол.) та ін. — Київ : Інститут філософії імені Григорія Сковороди НАН України : Абрис, 2002. — С. 578. — 742 с. — 1000 екз. — ББК 87я2. — ISBN 966-531-128-X.
• Числення предикатів // ФЕС, с.714
• Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947
• Клини С. К. Введение в метаматематику. М., 1957
• Мендельсон Э. Введение в математическую логику. М., 1976
• Новиков П. С. Элементы математической логики. М., 1959
• Черч А. Введение в математическую логику, т. I. М. 1960
• Філософський словник / за ред. В. І. Шинкарука. — 2-ге вид., перероб. і доп. — К. : Головна ред. УРЕ, 1986.