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

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

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

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

• Символи індивідуальних змінних, зазвичай $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,$. Кожній предикатній змінній відповідає деяке додатне число — арність предикату.
• Пропозиційні зв'язки: $\vee ,\wedge ,\mathrm{\neg },\to$,
• Квантори: загальності $\mathrm{\forall }$ і існування $\mathrm{\exists }$,
• Службові символи: дужки і кома.

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

• Терм — це символ змінної, або має вид $f(t_1,\dots ,t_n)$, де $f$ — функціональний символ арності $n$, а $t_1,\dots ,t_n$ — терми або $F(t_1,\dots ,t_n)$, де $F$ — функціональна змінна арності $n$, а $t_1,\dots ,t_n$ — терми.
• Атом — має вид $p(t_1,\dots ,t_n)$, де $p$ — предикатний символ арності $n$, а $t_1,\dots ,t_n$ — терми або $P(t_1,\dots ,t_n)$, де $P$ — предикатна змінна арності $n$, а $t_1,\dots ,t_n$ — терми.
• Формула — це або атом, або одна з наступних конструкцій: $\mathrm{\neg }A,(A_1\vee A_2),(A_1\wedge A_2),(A_1\to A_2),\mathrm{\forall }xA,\mathrm{\exists }xA,\mathrm{\forall }FA,\mathrm{\exists }FA,\mathrm{\forall }PA,\mathrm{\exists }PA$, де $A,A_1,A_2$ — формули, а $x,F,P$ — індивідуальна, функційна і предикатна змінні.

Семантика

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

• Базова множина $𝒟$,
• Семантична функція $\sigma$, що відображає
  • кожен $n$-арний функціональний символ $f$ із $ℱ$ в $n$-арну функцію $\sigma (f):𝒟\times \dots \times 𝒟\to 𝒟$,
  • кожен $n$-арний предикатний символ $p$ із $𝒫$ в $n$-арне відношення $\sigma (p)\subseteq 𝒟\times \dots \times 𝒟$.

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

• $[[x]{]}_s=s(x)$, якщо $x$ — змінна,
• $[[f(x_1,\dots ,x_n)]{]}_s=\sigma (f)([x_1]{]}_s,\dots ,[x_n]{]}_s)$ для функційного символу $f$
• $[[f(x_1,\dots ,x_n)]{]}_s=s(f)([x_1]{]}_s,\dots ,[x_n]{]}_s)$ для функційної змінної $F$

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

• $𝒟{\models }_{s}p(t_1,\dots ,t_n)$, тоді і тільки тоді коли $\sigma (p)([x_1]{]}_s,\dots ,[x_n]{]}_s)$,
• $𝒟{\models }_{s}P(t_1,\dots ,t_n)$, тоді і тільки тоді коли $s(P)([x_1]{]}_s,\dots ,[x_n]{]}_s)$,
• $𝒟{\models }_s\mathrm{\neg }\varphi$, тоді і тільки тоді коли $𝒟{\models }_s\varphi$ — хибно,
• $𝒟{\models }_s\varphi \wedge \psi$, тоді і тільки тоді коли $𝒟{\models }_s\varphi$ і $𝒟{\models }_s\psi$ істинні,'
• $𝒟{\models }_s\varphi \vee \psi$, тоді і тільки тоді коли $𝒟{\models }_s\varphi$ або $𝒟{\models }_s\psi$ істинно,
• $𝒟{\models }_s\varphi \to \psi$, тоді і тільки тоді коли з $𝒟{\models }_s\varphi$ випливає $𝒟{\models }_s\psi$,
• $𝒟{\models }_s\mathrm{\exists }x\varphi$, тоді і тільки тоді коли $𝒟{\models }_{s^{\prime }}\varphi$ для деякої підстановки $s^{\prime }$, яка відрізняється від $s$ тільки на індивідуальній змінній $x$,
• $𝒟{\models }_s\mathrm{\exists }F\varphi$, тоді і тільки тоді коли $𝒟{\models }_{s^{\prime }}\varphi$ для деякої підстановки $s^{\prime }$, яка відрізняється від $s$ тільки на функційній змінній $F$,
• $𝒟{\models }_s\mathrm{\exists }P\varphi$, тоді і тільки тоді коли $𝒟{\models }_{s^{\prime }}\varphi$ для деякої підстановки $s^{\prime }$, яка відрізняється від $s$ тільки на предикатній змінній $x$,
• $𝒟{\models }_s\mathrm{\forall }x\varphi$, тоді і тільки тоді коли $𝒟{\models }_{s^{\prime }}\varphi$ для всіх підстановок $s^{\prime }$, які відрізняються від $s$ тільки на індивідуальній змінній $x$,
• $𝒟{\models }_s\mathrm{\forall }F\varphi$, тоді і тільки тоді коли $𝒟{\models }_{s^{\prime }}\varphi$ для всіх підстановок $s^{\prime }$, які відрізняються від $s$ тільки на функційній змінній $F$,
• $𝒟{\models }_s\mathrm{\forall }P\varphi$, тоді і тільки тоді коли $𝒟{\models }_{s^{\prime }}\varphi$ для всіх підстановок $s^{\prime }$, які відрізняються від $s$ тільки на предикатній змінній $P$.

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

Властивості

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

Див. також

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

Джерела

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.