Исчисление предикатов - NiNa.Az

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

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

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

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

Язык логики первого порядка строится на основе сигнатуры, состоящей из множества функциональных символов ${\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