Логика второго порядка

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

Язык и синтаксисПравить

Формальные языки логики второго порядка строятся на основе множества функциональных символов $\mathcal{F}$${\mathcal {F}}$  и множества предикатных символов $\mathcal{P}$${\mathcal {P}}$ . С каждым функциональным и предикатным символом связана арность (число аргументов). Также используются дополнительные символы

• Символы индивидуальных переменных, обычно $x,y,z,x_1,y_1,z_1,x_2,y_2,z_2$$\ 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$$\ 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$$\ P,R,S,P_{1},R_{1},S_{1},P_{2},R_{2},S_{2}$  и т. д. Каждой предикатной переменной соответствует некоторое положительное число — арность предиката.
• Пропозициональные связи: $\vee <!--\; \vee \; -->,\wedge <!--\; \wedge \; -->,\mathrm{\neg <!--\; \neg \; -->},\to <!--\; \to \; -->$$\lor ,\land ,\neg ,\to$ ,
• Кванторы общности $\mathrm{\forall <!--\; \forall \; -->}$$\forall$  и существования $\mathrm{\exists <!--\; \exists \; -->}$$\exists$ ,
• Служебные символы: скобки и запятая.

Перечисленные символы вместе с символами $\mathcal{P}$${\mathcal {P}}$  и $\mathcal{F}$${\mathcal {F}}$  образуют алфавит логики первого порядка. Более сложные конструкции определяются индуктивно.

• Терм — это символ индивидуальной переменной, либо выражение, которое имеет вид $f(t_1,\dots <!--\; \dots \; -->,t_n)$$\ f(t_{1},\ldots ,t_{n})$ , где $f$$\ f$  — функциональный символ арности $n$$\ n$ , а $t_1,\dots <!--\; \dots \; -->,t_n$$\ t_{1},\ldots ,t_{n}$  — термы либо выражение вида $F(t_1,\dots <!--\; \dots \; -->,t_n)$$\ F(t_{1},\ldots ,t_{n})$ , где $F$$\ F$  — функциональная переменная арности $n$$\ n$ , а $t_1,\dots <!--\; \dots \; -->,t_n$$\ t_{1},\ldots ,t_{n}$  — термы.
• Атом — имеет вид $p(t_1,\dots <!--\; \dots \; -->,t_n)$$\ p(t_{1},\ldots ,t_{n})$ , где $p$$p$  — предикатный символ арности $n$$\ n$ , а $t_1,\dots <!--\; \dots \; -->,t_n$$\ t_{1},\ldots ,t_{n}$  — термы или $P(t_1,\dots <!--\; \dots \; -->,t_n)$$\ P(t_{1},\ldots ,t_{n})$ , где $P$$P$  — предикатная переменная арности $n$$\ n$ , а $t_1,\dots <!--\; \dots \; -->,t_n$$\ t_{1},\ldots ,t_{n}$  — термы.
• Формула — это или атом, или одна из следующих конструкций: $\mathrm{\neg <!--\; \neg \; -->}A,(A_1\vee <!--\; \vee \; -->A_2),(A_1\wedge <!--\; \wedge \; -->A_2),(A_1\to <!--\; \to \; -->A_2),\mathrm{\forall <!--\; \forall \; -->}xA,\mathrm{\exists <!--\; \exists \; -->}xA,\mathrm{\forall <!--\; \forall \; -->}FA,\mathrm{\exists <!--\; \exists \; -->}FA,\mathrm{\forall <!--\; \forall \; -->}PA,\mathrm{\exists <!--\; \exists \; -->}PA$$\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$$\ A,A_{1},A_{2}$  — формулы, а $x,F,P$$\ x,F,P$  — индивидуальная, функциональная и предикатная переменные. (Конструкции $\mathrm{\forall <!--\; \forall \; -->}FA,\mathrm{\exists <!--\; \exists \; -->}FA,\mathrm{\forall <!--\; \forall \; -->}PA,\mathrm{\exists <!--\; \exists \; -->}PA$$\forall FA,\exists FA,\forall PA,\exists PA$  являются формулами второго и не первого порядка).

СемантикаПравить

В классической логике интерпретация формул логики второго порядка задаётся на модели второго порядка, которая определяется следующими данными.

• Базовое множество $\mathcal{D}$$\mathcal{D}$ ,
• Семантическая функция $\mathrm{\sigma <!--\; \sigma \; -->}$$\sigma$ , которая отображает
  • каждый $n$$n$ -арный функциональный символ $f$$f$  из $\mathcal{F}$${\mathcal {F}}$  в $n$$n$ -арную функцию $\mathrm{\sigma <!--\; \sigma \; -->}(f):\mathcal{D}\times <!--\; \times \; -->\dots <!--\; \dots \; -->\times <!--\; \times \; -->\mathcal{D}\to <!--\; \to \; -->\mathcal{D}$$\sigma (f):{\mathcal {D}}\times \ldots \times {\mathcal {D}}\rightarrow {\mathcal {D}}$ ,
  • каждый $n$$n$ -арный предикатный символ $p$$p$  из $\mathcal{P}$${\mathcal {P}}$  в $n$$n$ -арное отношение $\mathrm{\sigma <!--\; \sigma \; -->}(p)\subseteq <!--\; \subseteq \; -->\mathcal{D}\times <!--\; \times \; -->\dots <!--\; \dots \; -->\times <!--\; \times \; -->\mathcal{D}$$\sigma (p)\subseteq {\mathcal {D}}\times \ldots \times {\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.