Скулемовская форма

Допустим, некоторая формула представлена в ПНФ c матрицей в виде конъюнкции дизъюнкций:

А¢ =(Q₁ (x₁) Q₂ (x₂)...Q_n (x_n))(D₁ & D₂ &...& D_k).

Пусть Q_r - первый слева квантор существования, т.е. перед ним стоят только кванторы всеобщности: Q₁ =... = Q_{r -1} = ". Операция замены квантора существования $ заклю-чается в следующем.

1) Исключаем из префикса $х_r .

2) Вместо него вводим ранее не встречавшийся в формуле символ функциональной переменной f и рассматриваем функцию f(x₁,x₂,...,x_{r -1}), которую подставляем в матрицу вместо всех вхождений переменной х_r.

Замечание. Если r =1, то вместо переменной х_r в мат-рицу подставляем константу (функцию, которая не зависит ни от одной переменной).

Определение. Описанная выше операция называется заменой квантора существования. Вводимые при этом функ-ции и константы называют скулемовскими, а получаемая после выполнения всех замен квантора существования (сле-ва направо) формула называется стандартной формой Ску-лема.

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

Теорема. Формула А невыполнима тогда и только тогда, когда её стандартная форма Скулема невыполнима.

Пример 1. Привести к стандартной форме Скулема формулу из п.6.1.

Решение. Поскольку префикс формулы не содержит кванто-ров всеобщности, то при замене обоих кванторов $х и $y в матрицу необходимо подставить скулемовские константы. Обозначим их, соответственно, а и b. Итоговое выражение имеет вид:

S(А)= ((Ø Р(а) Ú ØQ(z, b) Ú Р(z)) & (Ø Р(а) Ú Ø Р(z) Ú Q(z, b))).

Пример 2. Привести к стандартной форме Скулема формулу А = $х"у$zР(х, y, z).

Решение. Выполняя замены: x ® a, z ® f(y), получим: S(А) = "уР(a, y, f(y)).

Скулемовская форма не содержит кванторов суще-ствования. Все переменные в ней управляются кванторами всеобщности либо свободны. Такая формула невыпол-нима тогда и только тогда, когда невыполнима и формула, не содержащая кванторов. В частном случае для матрицы скулемовской формы, не содержащей функциональных сим-волов, доказательство сводится к доказательству невыпол-нимости обычной формулы ИВ.