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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

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

Язык и синтаксис[править | править вики-текст]

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

  • Символы индивидуальных переменных, обычно \ 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,. Каждой предикатной переменной соответствует некоторое положительное число — арность предиката.
  • Пропозициональные связи: \lor,\land,\neg,\to,
  • Кванторы общности \forall и существования \exists,
  • Служебные символы: скобки и запятая.

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

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

Аксиоматика и доказательство формул[править | править вики-текст]

Семантика[править | править вики-текст]

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

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

Свойства[править | править вики-текст]

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

Примечания[править | править вики-текст]

  1. Shapiro (1991) and Hinman (2005) give complete introductions to the subject, with full definitions.

Литература[править | править вики-текст]

  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.