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

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

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

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

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

  • Символы индивидуальных переменных, обычно и т. д.
  • Символы функциональных переменных . Каждой функциональной переменной соответствует некоторое положительное число — арность функции.
  • Символы предикатных переменных . Каждой предикатной переменной соответствует некоторое положительное число — арность предиката.
  • Пропозициональные связи: ,
  • Кванторы общности и существования ,
  • Служебные символы: скобки и запятая.

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

  • Терм — это символ индивидуальной переменной, либо выражение которое имеет вид , где  — функциональный символ арности , а  — термы либо выражение вида , где  — функциональная переменная арности , а  — термы.
  • Атом — имеет вид , где  — предикатный символ арности , а  — термы или , где  — предикатная переменная арности , а  — термы.
  • Формула — это или атом или одна из следующих конструкций: , где  — формулы, а  — индивидуальная, функциональная и предикатная переменные.

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

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

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

  • Базовое множество ,
  • Семантическая функция , которая отображает
    • каждый -арный функциональный символ из в -арную функцию ,
    • каждый -арный предикатный символ из в -арное отношение .

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

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

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

  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.