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

Запрос «Исчисление предикатов»^[d] перенаправляется сюда. На эту тему нужно создать отдельную статью.

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

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

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

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

• символы переменных (обычно $x$, $y$, $z$, $x_{1}$, $y_{1}$, $z_{1}$, $x_{2}$, $y_{2}$, $z_{2}$ и т. д.);
• логические операции:

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

• кванторы:

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

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

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

• Терм есть символ переменной, либо имеет вид $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}$ — термы.
  • Например, $(x+1)\times (x+1)\geqslant 0$ это атомарная формула, истинная для любого действительного числа $x$. Формула состоит из 2-арного предиката $\geqslant$, аргументами которого являются термы $(x+1)\times (x+1)$ и 0. При этом терм $(x+1)\times (x+1)$ состоит из константы 1 (которую можно считать 0-арной функцией), переменной $x$ и символов бинарных (2-арных) функций + и ×.
• Формула — это либо атом, либо одна из следующих конструкций: $\neg F$, $F_{1}\lor F_{2}$, $F_{1}\land F_{2}$, $F_{1}\to F_{2}$, $\forall xF$, $\exists xF$, где $F,F_{1},F_{2}$ — формулы, а $x$ — переменная.

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

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

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

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

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

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

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

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

• Правило обобщения:

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

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

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

• Несущее множество ${\mathcal {D}}$,
• Семантическая функция $\sigma$, отображающая
  • каждый $n$-арный функциональный символ $f$ из ${\mathcal {F}}$ в $n$-арную функцию $\sigma (f)\colon \,{\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}}$.

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

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

1. $[\![x]\!]_{s}=s(x)$, если $x$ — переменная,
2. $[\![f(x_{1},\ldots ,x_{n})]\!]_{s}=\sigma (f)([\!\![\,x_{1}]\!]_{s},\ldots ,[\![x_{n}]\!]_{s})$

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

• ${\mathcal {D}}\models _{s}p(t_{1},\ldots ,t_{n})$, тогда и только тогда, когда $\sigma (p)([\!\![\,t_{1}]\!]_{s},\ldots ,[\![t_{n}]\!]_{s})$,
• ${\mathcal {D}}\models _{s}\neg \phi$, тогда и только тогда, когда ${\mathcal {D}}\models _{s}\phi$ — ложно,
• ${\mathcal {D}}\models _{s}\phi \land \psi$, тогда и только тогда, когда ${\mathcal {D}}\models _{s}\phi$ и ${\mathcal {D}}\models _{s}\psi$ истинны,
• ${\mathcal {D}}\models _{s}\phi \lor \psi$, тогда и только тогда, когда ${\mathcal {D}}\models _{s}\phi$ или ${\mathcal {D}}\models _{s}\psi$ истинно,
• ${\mathcal {D}}\models _{s}\phi \to \psi$, тогда и только тогда, когда ${\mathcal {D}}\models _{s}\phi$ влечёт ${\mathcal {D}}\models _{s}\psi$,
• ${\mathcal {D}}\models _{s}\exists x\,\phi$, тогда и только тогда, когда ${\mathcal {D}}\models _{s'}\phi$ для некоторой подстановки $s'$, которая отличается от $s$ только значением на переменной $x$,
• ${\mathcal {D}}\models _{s}\forall x\,\phi$, тогда и только тогда, когда ${\mathcal {D}}\models _{s'}\phi$ для всех подстановок $s'$, которые отличается от $s$ только значением на переменной $x$.

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

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

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

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

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

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

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

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

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

• $\forall x(x=x)$
• $\forall x\forall y(x=y)\to (F(x)\to F(y))$

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

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

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

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

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

См. также

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

Литература

• Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947
• Клини С. К. Введение в метаматематику. М., 1957
• В. И. Маркин. Логика предикатов // Новая философская энциклопедия : в 4 т. / пред. науч.-ред. совета В. С. Стёпин. — 2-е изд., испр. и доп. — М. : Мысль, 2010. — 2816 с.
• Мендельсон Э. Введение в математическую логику. М., 1976
• Новиков П. С. Элементы математической логики. М., 1959
• Черч А. Введение в математическую логику, т. I. М. 1960