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

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

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

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

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

символы переменных (обычно [math]\displaystyle{ x }[/math], [math]\displaystyle{ y }[/math], [math]\displaystyle{ z }[/math], [math]\displaystyle{ x_1 }[/math], [math]\displaystyle{ y_1 }[/math], [math]\displaystyle{ z_1 }[/math], [math]\displaystyle{ x_2 }[/math], [math]\displaystyle{ y_2 }[/math], [math]\displaystyle{ z_2 }[/math] и т. д.);
логические операции:

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

кванторы:

Символ	Значение
[math]\displaystyle{ \forall }[/math]	Квантор всеобщности
[math]\displaystyle{ \exists }[/math]	Квантор существования

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

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

Терм есть символ переменной, либо имеет вид [math]\displaystyle{ f( t_1, \ldots, t_n ) }[/math], где [math]\displaystyle{ f }[/math] — функциональный символ арности [math]\displaystyle{ n }[/math], а [math]\displaystyle{ t_1, \ldots, t_n }[/math] — термы.
Атом (атомарная формула) имеет вид [math]\displaystyle{ p( t_1, \ldots, t_n ) }[/math], где [math]\displaystyle{ p }[/math] — предикатный символ арности [math]\displaystyle{ n }[/math], а [math]\displaystyle{ t_1, \ldots, t_n }[/math] — термы.
- Например, [math]\displaystyle{ (x+1)\times(x+1) \geqslant 0 }[/math] это атомарная формула, истинная для любого действительного числа [math]\displaystyle{ x }[/math]. Формула состоит из 2-арного предиката [math]\displaystyle{ \geqslant }[/math], аргументами которого являются термы [math]\displaystyle{ (x+1)\times(x+1) }[/math] и 0. При этом терм [math]\displaystyle{ (x+1)\times(x+1) }[/math] состоит из константы 1 (которую можно считать 0-арной функцией), переменной [math]\displaystyle{ x }[/math] и символов бинарных (2-арных) функций + и ×.
Формула — это либо атом, либо одна из следующих конструкций: [math]\displaystyle{ \neg F }[/math], [math]\displaystyle{ F_1\lor F_2 }[/math], [math]\displaystyle{ F_1\land F_2 }[/math], [math]\displaystyle{ F_1\to F_2 }[/math], [math]\displaystyle{ \forall x F }[/math], [math]\displaystyle{ \exists x F }[/math], где [math]\displaystyle{ F, F_1, F_2 }[/math] — функции, а [math]\displaystyle{ x }[/math] — переменная.

Переменная [math]\displaystyle{ x }[/math] называется связанной в формуле [math]\displaystyle{ F }[/math], если [math]\displaystyle{ F }[/math] имеет вид [math]\displaystyle{ \forall x G }[/math] либо [math]\displaystyle{ \exists x G }[/math], или же представима в одной из форм [math]\displaystyle{ \neg H }[/math], [math]\displaystyle{ F_1\lor F_2 }[/math], [math]\displaystyle{ F_1\land F_2 }[/math], [math]\displaystyle{ F_1\to F_2 }[/math], причём [math]\displaystyle{ x }[/math] уже связана в [math]\displaystyle{ H }[/math], [math]\displaystyle{ F_1 }[/math] и [math]\displaystyle{ F_2 }[/math]. Если [math]\displaystyle{ x }[/math] не связана в [math]\displaystyle{ F }[/math], её называют свободной в [math]\displaystyle{ F }[/math]. Формулу без свободных переменных называют замкнутой формулой, или предложением. Теорией первого порядка называют любое множество предложений.

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

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

[math]\displaystyle{ \forall x A \to A[t/x] }[/math],
[math]\displaystyle{ A[t/x] \to \exists x A }[/math],

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

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

Modus ponens (это правило используется также и в логике высказываний):
[math]\displaystyle{ \frac{A, A \to B}{B} }[/math]
Правило обобщения^[en]:
[math]\displaystyle{ \frac{A}{\forall x A} }[/math]

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

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

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

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

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

[math]\displaystyle{ [\![x]\!]_s = s(x) }[/math], если [math]\displaystyle{ x }[/math] — переменная,
[math]\displaystyle{ [\![f(x_1,\ldots,x_n)]\!]_s = \sigma(f)([\!\![\,x_1]\!]_s,\ldots,[\![x_n]\!]_s) }[/math]

В таком же духе определяется отношение истинности [math]\displaystyle{ \models_s }[/math] формул на [math]\displaystyle{ \mathcal{D} }[/math] относительно [math]\displaystyle{ s }[/math]:

[math]\displaystyle{ \mathcal{D}\models_s p(t_1,\ldots,t_n) }[/math], тогда и только тогда, когда [math]\displaystyle{ \sigma(p)([\!\![\,t_1]\!]_s,\ldots,[\![t_n]\!]_s) }[/math],
[math]\displaystyle{ \mathcal{D}\models_s \neg\phi }[/math], тогда и только тогда, когда [math]\displaystyle{ \mathcal{D}\models_s \phi }[/math] — ложно,
[math]\displaystyle{ \mathcal{D}\models_s \phi\land\psi }[/math], тогда и только тогда, когда [math]\displaystyle{ \mathcal{D}\models_s \phi }[/math] и [math]\displaystyle{ \mathcal{D}\models_s \psi }[/math] истинны,
[math]\displaystyle{ \mathcal{D}\models_s \phi\lor\psi }[/math], тогда и только тогда, когда [math]\displaystyle{ \mathcal{D}\models_s \phi }[/math] или [math]\displaystyle{ \mathcal{D}\models_s \psi }[/math] истинно,
[math]\displaystyle{ \mathcal{D}\models_s \phi\to\psi }[/math], тогда и только тогда, когда [math]\displaystyle{ \mathcal{D}\models_s \phi }[/math] влечёт [math]\displaystyle{ \mathcal{D}\models_s \psi }[/math],
[math]\displaystyle{ \mathcal{D}\models_s \exists x\, \phi }[/math], тогда и только тогда, когда [math]\displaystyle{ \mathcal{D}\models_{s'} \phi }[/math] для некоторой подстановки [math]\displaystyle{ s' }[/math], которая отличается от [math]\displaystyle{ s }[/math] только значением на переменной [math]\displaystyle{ x }[/math],
[math]\displaystyle{ \mathcal{D}\models_s \forall x\, \phi }[/math], тогда и только тогда, когда [math]\displaystyle{ \mathcal{D}\models_{s'} \phi }[/math] для всех подстановок [math]\displaystyle{ s' }[/math], которые отличается от [math]\displaystyle{ s }[/math] только значением на переменной [math]\displaystyle{ x }[/math].

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

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

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

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

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

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

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

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

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

[math]\displaystyle{ \forall x( x = x) }[/math]
[math]\displaystyle{ \forall x \forall y (x = y) \to (F(x) \to F(y)) }[/math]

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

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

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

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

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

См. также

Литература

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