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

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

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

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

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

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

• кванторы:

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

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

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

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

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

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

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

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

• Правило обобщения^[англ.]:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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