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

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

Язык и синтаксис

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

• Символы индивидуальных переменных, обычно [math]\displaystyle{ \ x, y, z, x_1, y_1, z_1, x_2, y_2, z_2 }[/math] и т. д.
• Символы функциональных переменных [math]\displaystyle{ \ F, G, H, F_1, G_1, H_1, F_2, G_2, H_2 }[/math] и т. д. Каждой функциональной переменной соответствует некоторое положительное число — арность функции.
• Символы предикатных переменных [math]\displaystyle{ \ P, R, S, P_1, R_1, S_1, P_2, R_2, S_2 }[/math] и т. д. Каждой предикатной переменной соответствует некоторое положительное число — арность предиката.
• Пропозициональные связи: [math]\displaystyle{ \lor,\land,\neg,\to }[/math],
• Кванторы общности [math]\displaystyle{ \forall }[/math] и существования [math]\displaystyle{ \exists }[/math],
• Служебные символы: скобки и запятая.

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

• Терм — это символ индивидуальной переменной, либо выражение, которое имеет вид [math]\displaystyle{ \ f(t_1,\ldots,t_n) }[/math], где [math]\displaystyle{ \ f }[/math] — функциональный символ арности [math]\displaystyle{ \ n }[/math], а [math]\displaystyle{ \ t_1,\ldots,t_n }[/math] — термы либо выражение вида [math]\displaystyle{ \ F(t_1,\ldots,t_n) }[/math], где [math]\displaystyle{ \ F }[/math] — функциональная переменная арности [math]\displaystyle{ \ n }[/math], а [math]\displaystyle{ \ t_1,\ldots,t_n }[/math] — термы.
• Атом — имеет вид [math]\displaystyle{ \ p(t_1,\ldots,t_n) }[/math], где [math]\displaystyle{ p }[/math] — предикатный символ арности [math]\displaystyle{ \ n }[/math], а [math]\displaystyle{ \ t_1,\ldots,t_n }[/math] — термы или [math]\displaystyle{ \ P(t_1,\ldots,t_n) }[/math], где [math]\displaystyle{ P }[/math] — предикатная переменная арности [math]\displaystyle{ \ n }[/math], а [math]\displaystyle{ \ t_1,\ldots,t_n }[/math] — термы.
• Формула — это или атом, или одна из следующих конструкций: [math]\displaystyle{ \neg A, (A_1\lor A_2), (A_1\land A_2), (A_1\to A_2), \forall x A, \exists x A, \forall F A, \exists F A, \forall P A, \exists P A }[/math], где [math]\displaystyle{ \ A, A_1, A_2 }[/math] — формулы, а [math]\displaystyle{ \ x, F, P }[/math] — индивидуальная, функциональная и предикатная переменные. (Конструкции [math]\displaystyle{ \forall F A, \exists F A, \forall P A, \exists P A }[/math] являются формулами второго и не первого порядка).

Семантика

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

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

Свойства

В отличие от логики первого порядка, логика второго порядка не имеет свойств полноты и компактности. Также в этой логике является неверным утверждение теоремы Лёвенгейма — Скулема.

Литература

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.