WikiSort.ru - Не сортированное

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

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

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

• Символы индивидуальных переменных, обычно ${\displaystyle \ x,y,z,x_{1},y_{1},z_{1},x_{2},y_{2},z_{2},}$ и т. д.
• Символы функциональных переменных ${\displaystyle \ F,G,H,F_{1},G_{1},H_{1},F_{2},G_{2},H_{2},}$ . Каждой функциональной переменной соответствует некоторое положительное число — арность функции.
• Символы предикатных переменных ${\displaystyle \ P,R,S,P_{1},R_{1},S_{1},P_{2},R_{2},S_{2},}$ . Каждой предикатной переменной соответствует некоторое положительное число — арность предиката.
• Пропозициональные связи: ${\displaystyle \lor ,\land ,\neg ,\to }$ ,
• Кванторы общности ${\displaystyle \forall }$ и существования ${\displaystyle \exists }$ ,
• Служебные символы: скобки и запятая.

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

• Терм — это символ индивидуальной переменной, либо выражение которое имеет вид ${\displaystyle \ f(t_{1},\ldots ,t_{n})}$ , где ${\displaystyle \ f}$  — функциональный символ арности ${\displaystyle \ n}$ , а ${\displaystyle \ t_{1},\ldots ,t_{n}}$  — термы либо выражение вида ${\displaystyle \ F(t_{1},\ldots ,t_{n})}$ , где ${\displaystyle \ F}$  — функциональная переменная арности ${\displaystyle \ n}$ , а ${\displaystyle \ t_{1},\ldots ,t_{n}}$  — термы.
• Атом — имеет вид ${\displaystyle \ p(t_{1},\ldots ,t_{n})}$ , где ${\displaystyle p}$  — предикатный символ арности ${\displaystyle \ n}$ , а ${\displaystyle \ t_{1},\ldots ,t_{n}}$  — термы или ${\displaystyle \ P(t_{1},\ldots ,t_{n})}$ , где ${\displaystyle P}$  — предикатная переменная арности ${\displaystyle \ n}$ , а ${\displaystyle \ t_{1},\ldots ,t_{n}}$  — термы.
• Формула — это или атом или одна из следующих конструкций: ${\displaystyle \neg A,(A_{1}\lor A_{2}),(A_{1}\land A_{2}),(A_{1}\to A_{2}),\forall xA,\exists xA,\forall FA,\exists FA,\forall PA,\exists PA}$ , где ${\displaystyle \ A,A_{1},A_{2}}$  — формулы, а ${\displaystyle \ x,F,P}$  — индивидуальная, функциональная и предикатная переменные.

Аксиоматика и доказательство формул

Этот раздел статьи ещё не написан. Согласно замыслу одного или нескольких участников Википедии, на этом месте должен располагаться раздел, посвящённый аксиоматике и правилам вывода. Вы можете помочь проекту, написав этот раздел.

Семантика

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

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

Свойства

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

Примечания

Литература

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.

Это заготовка статьи по логике. Вы можете помочь проекту, дополнив её.

Для улучшения этой статьи по математике желательно: Викифицировать статью. Викифицировать список литературы.