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

Ло́гіка другого́ поря́дку — у логіці є розширенням логіки першого порядку в якій допускаються змінні-функції і змінні-предикати, а також квантифікація над цими змінними. Дана логіка не спрощується до логіки першого порядку.

Мова і синтаксис

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

• Символи індивідуальних змінних, зазвичай $\ x,y,z,x_{1},y_{1},z_{1},x_{2},y_{2},z_{2},$ і т.д.,
• Символи функційних змінних $\ F,G,H,F_{1},G_{1},H_{1},F_{2},G_{2},H_{2},$. Кожній функційній змінній відповідає деяке додатне число — арність функції.
• Символи предикатних змінних $\ P,R,S,P_{1},R_{1},S_{1},P_{2},R_{2},S_{2},$. Кожній предикатній змінній відповідає деяке додатне число — арність предикату.
• Пропозиційні зв'язки: $\lor ,\land ,\neg ,\to$,
• Квантори: загальності $\forall$ і існування $\exists$,
• Службові символи: дужки і кома.

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

• Терм — це символ змінної, або має вид $\ f(t_{1},\ldots ,t_{n})$, де $\ f$ — функціональний символ арності $\ n$, а $\ t_{1},\ldots ,t_{n}$ — терми або $\ 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}$ — терми або $\ P(t_{1},\ldots ,t_{n})$, де $P$ — предикатна змінна арності $\ n$, а $\ t_{1},\ldots ,t_{n}$ — терми.
• Формула — це або атом, або одна з наступних конструкцій: $\neg A,(A_{1}\lor A_{2}),(A_{1}\land A_{2}),(A_{1}\to A_{2}),\forall xA,\exists xA,\forall FA,\exists FA,\forall PA,\exists PA$, де $\ A,A_{1},A_{2}$ — формули, а $\ x,F,P$ — індивідуальна, функційна і предикатна змінні.

Семантика

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

• Базова множина ${\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}}$, кожну функційну змінну арності $n$ в $n$-арну функцію $\sigma (f):{\mathcal {D}}\times \ldots \times {\mathcal {D}}\rightarrow {\mathcal {D}}$ і кожну предикатну змінну арності $n$ в $n$-арне відношення $\sigma (p)\subseteq {\mathcal {D}}\times \ldots \times {\mathcal {D}}$. Функцію $s$ називатимемо також підстановкою. Інтерпретація $[\![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})$ для функційного символу $f$
• $[\![f(x_{1},\ldots ,x_{n})]\!]_{s}=s(f)(\![x_{1}]\!]_{s},\ldots ,\![x_{n}]\!]_{s})$ для функційної змінної $F$

Подібним чином визначається істинність $\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}P(t_{1},\ldots ,t_{n})$, тоді і тільки тоді коли $s(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}\exists F\,\phi$, тоді і тільки тоді коли ${\mathcal {D}}\models _{s'}\phi$ для деякої підстановки $s'$, яка відрізняється від $s$ тільки на функційній змінній $F$,
• ${\mathcal {D}}\models _{s}\exists P\,\phi$, тоді і тільки тоді коли ${\mathcal {D}}\models _{s'}\phi$ для деякої підстановки $s'$, яка відрізняється від $s$ тільки на предикатній змінній $x$,
• ${\mathcal {D}}\models _{s}\forall x\,\phi$, тоді і тільки тоді коли ${\mathcal {D}}\models _{s'}\phi$ для всіх підстановок $s'$, які відрізняються від $s$ тільки на індивідуальній змінній $x$,
• ${\mathcal {D}}\models _{s}\forall F\,\phi$, тоді і тільки тоді коли ${\mathcal {D}}\models _{s'}\phi$ для всіх підстановок $s'$, які відрізняються від $s$ тільки на функційній змінній $F$,
• ${\mathcal {D}}\models _{s}\forall P\,\phi$, тоді і тільки тоді коли ${\mathcal {D}}\models _{s'}\phi$ для всіх підстановок $s'$, які відрізняються від $s$ тільки на предикатній змінній $P$.

Формула $\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}}$.

Властивості

На відміну від логіки першого логіка другого порядку не має властивостей повноти і компактності. Також у цій логіці є невірним твердження теореми Ловенгейма—Сколема.

Див. також

• Логіка першого порядку
• Числення висловлень

Джерела

1. Henkin, L. (1950). "Completeness in the theory of types". Journal of Symbolic Logic 15 (2): 81–91.
2. Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0.
3. Shapiro, S. (2000). Foundations without Foundationalism: A Case for Second-order Logic. Oxford University Press. ISBN 0-19-825029-0.
4. Rossberg, M. (2004). "First-Order Logic, Second-Order Logic, and Completeness". in V. Hendricks et al., eds. First-order logic revisited. Berlin: Logos-Verlag.
5. Vaananen, J. (2001). "Second-Order Logic and Foundations of Mathematics". Bulletin of Symbolic Logic 7 (4): 504–520.