Полнота теории первого порядка

Кроме исчисления предикатов существуют другие формальные теории, связанные с языком первого порядка. Мы рассмотрим исчисление предикатов. Наиболее простая из них – исчисление ММ. Логические аксиомы в этой системе – предложения q, истинные в любой модели языка первого порядка L. Правило вывода одно – Modus Ponens. Мы будем опираться далее на равносильность этой формальной теории исчислению предикатов, которая в действительности вытекает из теоремы Гёделя о полноте исчисления предикатов.

Теорема о полноте теории первого порядка. Пусть заданы произвольные множества предложений å и предложение q языка L. Вывод å q существует тогда и только тогда, когда каждая модель теории å удовлетворяет предложению q.

Доказательство. В случае å q и A |= å утверждение A |= q доказывается очевидным образом с помощью индукции по длине вывода å q (теорема о корректности). Пусть, наоборот, каждая модель A |= å удовлетворяет q. Так как всякая модель å является моделью для q, то множество предложений å È {Øq} не имеет моделей. По теореме компактности существует такое конечное подмножество {q₁, …, q_n} Í å, что {q₁, …, q_n, Øq} не имеет моделей. Отсюда Ø (q₁ & … & q_n & Øq) – тавтология исчисления ММ. Значит, имеет место логическая аксиома: q₁ ® (q₂ ® (… ® (q_n ® q) …))), из которой будет вытекать вывод: å q.

Упрощение формул

Наша задача: привести произвольную формулу к бескванторной форме. Это можно решить приведением к пренексной нормальной форме с последующей элиминацией кванторов и расширением исходного языка.

Пренексная нормальная форма

Формула Q₁y₁Q₂y₂ … Q_ny_n q, где – Q_i кванторы, а q не имеет кванторов, называется пренексной (или предваренной) нормальной формой. Существует эффективная процедура приведения формулы к пренексной нормальной форме. Она основана на следующих далее правилах преобразования, вытекающих из логических аксиом исчисления предикатов.

Обозначим "¢ = $, $¢ = ". Имеет место эквивалентность формул ØQxq º Q¢xØq. При условии, что переменная х не входит свободно в формулу y, верны равенства:

1) Qxq & y º Qx(q & y);

2) Qxq Ú y º Qx(q Ú y);

3) (y ® Qxq) º Qx(y ® q);

4) (Qxq ® y) º Q¢x(q ® y);

Имеет место эквивалентность формул:

5) Qxq º Qyq(x/y)

Пример 1

Найдём пренексную нормальную форму формулы $xq «y, где q и y не содержат кванторов, и х не входит свободно в y. Представим её как

($xq ® y) & (y ® $xq).

С помощью равенств 3 – 4 она приводится к виду:

"x(q ® y) & $x(y ® q).

С помощью равенства 1 – к виду: "x((q ® y) & $x(y ® q)).

С помощью равенства 5 – к виду: "x((q ® y) & $y(y ® q(y/x))),

где y не входит в преобразуемую формулу. Снова из равенства 1 получаем:

"x$y((q ® y) & (y ® q(y/x))).

Элиминация кванторов

По пренексной нормальной форме q строится формула q*, не содержащая кванторов. Кванторы всеобщности удаляются, а кванторы существования заменяются на функциональные символы, добавляемые к языку:

$yq(y, x₁, …, x_n) переходит в q(f(x₁, …, x_n), x₁, …, x_n), и операция f добавляется к языку.

Пример 2

Пусть q º$x₁ "x₂ "x₃ $x₄ $x₅ "x₆ y(x₁, x₂, x₃, x₄, x₅, x₆). Выполним действия для приведения к бескванторной форме:

1) удалим $x₁ и заменим x₁ константой b₁:

"x₂ "x₃ $x₄ $x₅ "x₆ y(b₁, x₂, x₃, x₄, x₅, x₆);

2) удалим два квантора всеобщности:

$x₄ $x₅ "x₆ y(b₁, x₂, x₃, x₄, x₅, x₆);

3) удалим квантор существования и к L добавим символ операции x₄ = f(x₂, x₃):

$x₅ "x₆ y(b₁, x₂, x₃, f(x₂, x₃), x₅, x₆);

4) удалим квантор существования и к L добавим символ операции x₅ = g(x₂, x₃):

"x₆ y(b₁, x₂, x₃, f(x₂, x₃), g(x₂, x₃), x₆);

5) удалим квантор всеобщности:

q¢¢ = y(b₁, x₂, x₃, f(x₂, x₃), g(x₂, x₃), x₆).

Полученная формула определена в языке L¢¢ = L È {b₁, f, g}.

Пусть å – множество предложений в языке L. Обозначим через q¢¢ формулу, полученную из предложения q приведением к пренексной нормальной форме с последующей элиминацией кванторов и преобразованием языка L. Положим . Пусть в результате преобразований формул q Î å в q¢¢ мы пришли к расширенному языку L¢¢.