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

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

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

Язык логики первого порядка строится на основе сигнатуры , состоящей из множества функциональных символов ${\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 с.
• _en Введение в математическую логику. М., 1976
• Новиков П. С. Элементы математической логики. М., 1959
• Черч А. Введение в математическую логику, т. I. М. 1960