Логика второго порядка
Логика второго порядка в математической логике — формальная система, расширяющая логику первого порядка[1] возможностью квантификации общности и существования не только над переменными, но и над предикатами и функциональными символами. Логика второго порядка несводима к логике первого порядка. В свою очередь, она расширяется логикой высших порядков и теорией типов.
Язык и синтаксис
Формальные языки логики второго порядка строятся на основе множества функциональных символов [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].
Свойства
В отличие от логики первого порядка, логика второго порядка не имеет свойств полноты и компактности. Также в этой логике является неверным утверждение теоремы Лёвенгейма — Скулема.
Примечания
- ↑ Shapiro (1991) and Hinman (2005) give complete introductions to the subject, with full definitions.
Литература
- Henkin, L. (1950). «Completeness in the theory of types». Journal of Symbolic Logic 15 (2): 81-91.
- Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0.
- Shapiro, S. (2000). Foundations without Foundationalism: A Case for Second-order Logic. Oxford University Press. ISBN 0-19-825029-0.
- Rossberg, M. (2004). «First-Order Logic, Second-Order Logic, and Completeness». in V. Hendricks et al., eds.. First-order logic revisited. Berlin: Logos-Verlag.
- Vaananen, J. (2001). «Second-Order Logic and Foundations of Mathematics». Bulletin of Symbolic Logic 7 (4): 504—520.