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

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

Помимо логики первого порядка существуют также логики высших порядков, в которых кванторы могут применяться не только к переменным, но и к предикатам. Термины логика предикатов и исчисление предикатов могут означать как логику первого порядка, так и логики первого и высшего порядка вместе; в первом случае иногда говорится о чистой логике предикатов или чистом исчислении предикатов.

Основные определения

Язык логики первого порядка строится на основе сигнатуры, состоящей из множества функциональных символов $ℱ$ и множества предикатных символов $𝒫$. С каждым функциональным и предикатным символом связана арность, то есть число возможных аргументов. Допускаются как функциональные, так и предикатные символы арности 0. Первые иногда выделяют в отдельное множество констант. Кроме того, используются следующие дополнительные символы:

• символы переменных (обычно $x$, $y$, $z$, $x_1$, $y_1$, $z_1$, $x_2$, $y_2$, $z_2$ и т. д.);
• логические операции:

Символ	Значение
$\mathrm{\neg }$	Отрицание («не»)
$\wedge$, $\mathrm{\&}$	Конъюнкция («и»)
$\vee$	Дизъюнкция («или»)
$\to$, $\supset$	Импликация («если …, то …»)

• кванторы:

Символ	Значение
$\mathrm{\forall }$	Квантор всеобщности
$\mathrm{\exists }$	Квантор существования

• служебные символы: скобки и запятая.

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

• Терм есть символ переменной, либо имеет вид $f(t_1,\dots ,t_n)$, где $f$ — функциональный символ арности $n$, а $t_1,\dots ,t_n$ — термы.
• Атом (атомарная формула) имеет вид $p(t_1,\dots ,t_n)$, где $p$ — предикатный символ арности $n$, а $t_1,\dots ,t_n$ — термы.
  • Например, $(x+1)\times (x+1)⩾0$ это атомарная формула, истинная для любого действительного числа $x$. Формула состоит из 2-арного предиката $⩾$, аргументами которого являются термы $(x+1)\times (x+1)$ и 0. При этом терм $(x+1)\times (x+1)$ состоит из константы 1 (которую можно считать 0-арной функцией), переменной $x$ и символов бинарных (2-арных) функций + и ×.
• Формула — это либо атом, либо одна из следующих конструкций: $\mathrm{\neg }F$, $F_1\vee F_2$, $F_1\wedge F_2$, $F_1\to F_2$, $\mathrm{\forall }xF$, $\mathrm{\exists }xF$, где $F,F_1,F_2$ — формулы, а $x$ — переменная.

Переменная $x$ называется связанной в формуле $F$, если $F$ имеет вид $\mathrm{\forall }xG$ либо $\mathrm{\exists }xG$, или же представима в одной из форм $\mathrm{\neg }H$, $F_1\vee F_2$, $F_1\wedge F_2$, $F_1\to F_2$, причём $x$ уже связана в $H$, $F_1$ и $F_2$. Если $x$ не связана в $F$, её называют свободной в $F$. Формулу без свободных переменных называют замкнутой формулой, или предложением. Теорией первого порядка называют любое множество предложений.

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

Система логических аксиом логики первого порядка состоит из аксиом исчисления высказываний дополненной двумя новыми аксиомами:

• $\mathrm{\forall }xA\to A[t/x]$,
• $A[t/x]\to \mathrm{\exists }xA$,

где $A[t/x]$ — формула, полученная в результате подстановки терма $t$ вместо каждой свободной переменной $x$, встречающейся в формуле $A$.

В логике первого порядка используется два правила вывода:

• Modus ponens (это правило используется также и в логике высказываний):

  $\frac{A,A\to B}{B}$

• Шаблон:Нп1:

  $\frac{A}{\mathrm{\forall }xA}$

Интерпретация

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

• Несущее множество $𝒟$,
• Семантическая функция $\sigma$, отображающая
  • каждый $n$-арный функциональный символ $f$ из $ℱ$ в $n$-арную функцию $\sigma (f):𝒟\times \dots \times 𝒟\to 𝒟$,
  • каждый $n$-арный предикатный символ $p$ из $𝒫$ в $n$-арное отношение $\sigma (p)\subseteq 𝒟\times \dots \times 𝒟$.

Обычно принято отождествлять несущее множество $𝒟$ и саму модель, подразумевая неявно семантическую функцию, если это не ведёт к неоднозначности.

Предположим, $s$ — функция, отображающая каждую переменную в некоторый элемент из $𝒟$, которую мы будем называть подстановкой. Интерпретация $[[t]{]}_s$ терма $t$ на $𝒟$ относительно подстановки $s$ задаётся индуктивно:

1. $[[x]{]}_s=s(x)$, если $x$ — переменная,
2. $[[f(x_1,\dots ,x_n)]{]}_s=\sigma (f)([[x_1]{]}_s,\dots ,[[x_n]{]}_s)$

В таком же духе определяется отношение истинности ${\models }_s$ формул на $𝒟$ относительно $s$:

• $𝒟{\models }_{s}p(t_1,\dots ,t_n)$, тогда и только тогда, когда $\sigma (p)([[t_1]{]}_s,\dots ,[[t_n]{]}_s)$,
• $𝒟{\models }_s\mathrm{\neg }\varphi$, тогда и только тогда, когда $𝒟{\models }_s\varphi$ — ложно,
• $𝒟{\models }_s\varphi \wedge \psi$, тогда и только тогда, когда $𝒟{\models }_s\varphi$ и $𝒟{\models }_s\psi$ истинны,
• $𝒟{\models }_s\varphi \vee \psi$, тогда и только тогда, когда $𝒟{\models }_s\varphi$ или $𝒟{\models }_s\psi$ истинно,
• $𝒟{\models }_s\varphi \to \psi$, тогда и только тогда, когда $𝒟{\models }_s\varphi$ влечёт $𝒟{\models }_s\psi$,
• $𝒟{\models }_s\mathrm{\exists }x\varphi$, тогда и только тогда, когда $𝒟{\models }_{s^{\prime }}\varphi$ для некоторой подстановки $s^{\prime }$, которая отличается от $s$ только значением на переменной $x$,
• $𝒟{\models }_s\mathrm{\forall }x\varphi$, тогда и только тогда, когда $𝒟{\models }_{s^{\prime }}\varphi$ для всех подстановок $s^{\prime }$, которые отличается от $s$ только значением на переменной $x$.

Формула $\varphi$ истинна на $𝒟$ (что обозначается как $𝒟\models \varphi$), если $𝒟{\models }_s\varphi$ для всех подстановок $s$. Формула $\varphi$ называется общезначимой (что обозначается как $\models \varphi$), если $𝒟\models \varphi$ для всех моделей $𝒟$. Формула $\varphi$ называется выполнимой, если $𝒟\models \varphi$ хотя бы для одной $𝒟$.

Свойства и основные результаты

Логика первого порядка обладает рядом полезных свойств, которые делают её очень привлекательной в качестве основного инструмента формализации математики. Главными из них являются:

• полнота (это означает, что любая общезначимая формула выводима);
• непротиворечивость (ни одна формула не может быть выведена одновременно со своим отрицанием).

При этом если непротиворечивость более или менее очевидна, то полнота — нетривиальный результат, полученный Гёделем в 1930 году (теорема Гёделя о полноте). По сути теорема Гёделя устанавливает фундаментальную эквивалентность понятий доказуемости и общезначимости.

Логика первого порядка обладает свойством компактности, доказанным Мальцевым: если некоторое множество формул не выполнимо, то невыполнимо также некоторое его конечное подмножество.

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

Логика первого порядка с равенством

Во многих теориях первого порядка участвует символ равенства. Его часто относят к символам логики и дополняют её соответствующими аксиомами, определяющими его. Такая логика называется логикой первого порядка с равенством, а соответствующие теории — теориями первого порядка с равенством. Символ равенства вводится как двуместный предикатный символ $=$. Вводимые для него дополнительные аксиомы следующие:

• $\mathrm{\forall }x(x=x)$
• $\mathrm{\forall }x\mathrm{\forall }y(x=y)\to (F(x)\to F(y))$

Использование

Логика первого порядка как формальная модель рассуждений

Являясь формализованным аналогом обычной логики, логика первого порядка даёт возможность строго рассуждать об истинности и ложности утверждений и об их взаимосвязи, в частности, о логическом следовании одного утверждения из другого, или, например, об их эквивалентности. Рассмотрим классический пример формализации утверждений естественного языка в логике первого порядка.

Возьмём рассуждение «Каждый человек смертен. Сократ — человек. Следовательно, Сократ смертен». Обозначим «x есть человек» через ЧЕЛОВЕК(x) и «x смертен» через СМЕРТЕН(x). Тогда утверждение «каждый человек смертен» может быть представлено формулой: $\mathrm{\forall }$x(ЧЕЛОВЕК(x) → СМЕРТЕН(x)) утверждение «Сократ — человек» формулой ЧЕЛОВЕК(Сократ), и «Сократ смертен» формулой СМЕРТЕН(Сократ). Утверждение в целом теперь может быть записано формулой

($\mathrm{\forall }$x(ЧЕЛОВЕК(x) → СМЕРТЕН(x)) $\wedge$ ЧЕЛОВЕК(Сократ)) → СМЕРТЕН(Сократ)

См. также

• Логика высказываний
• Логика второго порядка
• Алгоритм Тарского

Литература

• Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947
• Клини С. К. Введение в метаматематику. М., 1957
• Шаблон:НФЭ
• Шаблон:Нп4 Введение в математическую логику. М., 1976
• Новиков П. С. Элементы математической логики. М., 1959
• Черч А. Введение в математическую логику, т. I. М. 1960