Русская Википедия:Логика второго порядка

Содержание

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

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

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

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

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

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

• Терм — это символ индивидуальной переменной, либо выражение, которое имеет вид <math>\ f(t_1,\ldots,t_n)</math>, где <math>\ f</math> — функциональный символ арности <math>\ n</math>, а <math>\ t_1,\ldots,t_n</math> — термы либо выражение вида <math>\ F(t_1,\ldots,t_n)</math>, где <math>\ F</math> — функциональная переменная арности <math>\ n</math>, а <math>\ t_1,\ldots,t_n</math> — термы.
• Атом — имеет вид <math>\ p(t_1,\ldots,t_n)</math>, где <math>p</math> — предикатный символ арности <math>\ n</math>, а <math>\ t_1,\ldots,t_n</math> — термы или <math>\ P(t_1,\ldots,t_n)</math>, где <math>P</math> — предикатная переменная арности <math>\ n</math>, а <math>\ t_1,\ldots,t_n</math> — термы.
• Формула — это или атом, или одна из следующих конструкций: <math>\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>\ A, A_1, A_2</math> — формулы, а <math>\ x, F, P</math> — индивидуальная, функциональная и предикатная переменные. (Конструкции <math>\forall F A, \exists F A, \forall P A, \exists P A</math> являются формулами второго и не первого порядка).

Семантика

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

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