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

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

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

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

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

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

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

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

Припустимо ${\displaystyle s}$ — функція, що відображає кожну індивідуальну змінну в деякий елемент із ${\displaystyle {\mathcal {D}$, кожну функційну змінну арності ${\displaystyle n}$ в ${\displaystyle n}$-арну функцію ${\displaystyle \sigma (f):{\mathcal {D}\times \ldots \times {\mathcal {D}\rightarrow {\mathcal {D}$ і кожну предикатну змінну арності ${\displaystyle n}$ в ${\displaystyle n}$-арне відношення ${\displaystyle \sigma (p)\subseteq {\mathcal {D}\times \ldots \times {\mathcal {D}$. Функцію ${\displaystyle s}$ називатимемо також підстановкою. Інтерпретація ${\displaystyle [\![t]\!]_{s}$ терма ${\displaystyle t}$ на${\displaystyle {\mathcal {D}$ відносно підстановки ${\displaystyle s}$ задається індуктивно

• ${\displaystyle [\![x]\!]_{s}=s(x)}$, якщо ${\displaystyle x}$ — змінна,
• ${\displaystyle [\![f(x_{1},\ldots ,x_{n})]\!]_{s}=\sigma (f)(\![x_{1}]\!]_{s},\ldots ,\![x_{n}]\!]_{s})}$ для функційного символу ${\displaystyle f}$
• ${\displaystyle [\![f(x_{1},\ldots ,x_{n})]\!]_{s}=s(f)(\![x_{1}]\!]_{s},\ldots ,\![x_{n}]\!]_{s})}$ для функційної змінної ${\displaystyle F}$

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

• ${\displaystyle {\mathcal {D}\models _{s}p(t_{1},\ldots ,t_{n})}$, тоді і тільки тоді коли ${\displaystyle \sigma (p)(\![x_{1}]\!]_{s},\ldots ,\![x_{n}]\!]_{s})}$,
• ${\displaystyle {\mathcal {D}\models _{s}P(t_{1},\ldots ,t_{n})}$, тоді і тільки тоді коли ${\displaystyle s(P)(\![x_{1}]\!]_{s},\ldots ,\![x_{n}]\!]_{s})}$,
• ${\displaystyle {\mathcal {D}\models _{s}\neg \phi }$, тоді і тільки тоді коли ${\displaystyle {\mathcal {D}\models _{s}\phi }$ — хибно,
• ${\displaystyle {\mathcal {D}\models _{s}\phi \land \psi }$, тоді і тільки тоді коли ${\displaystyle {\mathcal {D}\models _{s}\phi }$ і ${\displaystyle {\mathcal {D}\models _{s}\psi }$ істинні,'
• ${\displaystyle {\mathcal {D}\models _{s}\phi \lor \psi }$, тоді і тільки тоді коли ${\displaystyle {\mathcal {D}\models _{s}\phi }$ або ${\displaystyle {\mathcal {D}\models _{s}\psi }$ істинно,
• ${\displaystyle {\mathcal {D}\models _{s}\phi \to \psi }$, тоді і тільки тоді коли з ${\displaystyle {\mathcal {D}\models _{s}\phi }$ випливає ${\displaystyle {\mathcal {D}\models _{s}\psi }$,
• ${\displaystyle {\mathcal {D}\models _{s}\exists x\,\phi }$, тоді і тільки тоді коли ${\displaystyle {\mathcal {D}\models _{s'}\phi }$ для деякої підстановки ${\displaystyle s'}$, яка відрізняється від ${\displaystyle s}$ тільки на індивідуальній змінній ${\displaystyle x}$,
• ${\displaystyle {\mathcal {D}\models _{s}\exists F\,\phi }$, тоді і тільки тоді коли ${\displaystyle {\mathcal {D}\models _{s'}\phi }$ для деякої підстановки ${\displaystyle s'}$, яка відрізняється від ${\displaystyle s}$ тільки на функційній змінній ${\displaystyle F}$,
• ${\displaystyle {\mathcal {D}\models _{s}\exists P\,\phi }$, тоді і тільки тоді коли ${\displaystyle {\mathcal {D}\models _{s'}\phi }$ для деякої підстановки ${\displaystyle s'}$, яка відрізняється від ${\displaystyle s}$ тільки на предикатній змінній ${\displaystyle x}$,
• ${\displaystyle {\mathcal {D}\models _{s}\forall x\,\phi }$, тоді і тільки тоді коли ${\displaystyle {\mathcal {D}\models _{s'}\phi }$ для всіх підстановок ${\displaystyle s'}$, які відрізняються від ${\displaystyle s}$ тільки на індивідуальній змінній ${\displaystyle x}$,
• ${\displaystyle {\mathcal {D}\models _{s}\forall F\,\phi }$, тоді і тільки тоді коли ${\displaystyle {\mathcal {D}\models _{s'}\phi }$ для всіх підстановок ${\displaystyle s'}$, які відрізняються від ${\displaystyle s}$ тільки на функційній змінній ${\displaystyle F}$,
• ${\displaystyle {\mathcal {D}\models _{s}\forall P\,\phi }$, тоді і тільки тоді коли ${\displaystyle {\mathcal {D}\models _{s'}\phi }$ для всіх підстановок ${\displaystyle s'}$, які відрізняються від ${\displaystyle s}$ тільки на предикатній змінній ${\displaystyle P}$.

Формула ${\displaystyle \phi }$, істинна на ${\displaystyle {\mathcal {D}$, що позначається ${\displaystyle {\mathcal {D}\models \phi }$, якщо ${\displaystyle {\mathcal {D}\models _{s}\phi }$, для всіх підстановок ${\displaystyle s}$. Формула ${\displaystyle \phi }$ називається загальнозначимою, (позначається ${\displaystyle \models \phi }$), якщо ${\displaystyle {\mathcal {D}\models \phi }$ для всіх моделей ${\displaystyle {\mathcal {D}$. Формула ${\displaystyle \phi }$ називається виконуваною , якщо ${\displaystyle {\mathcal {D}\models \phi }$ хоча б для однієї ${\displaystyle {\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.