Шаг 1 – Шаг 3 – те же, что и в предыдущем алгоритме.
Шаг 4. Бескванторную часть привести к конъюнктивной нормальной форме (алгоритм описан в §5 темы 1).
Шаг 5. Исключить кванторы существования. Этот шаг изложим на примере. Пусть после выполнения четвертого шага имеем формулу F=($x)("y)($z)("u)($v)H(x,y,z,u,v), где Н – не содержит кванторов. Предположим, что формула не содержит константы с, символов одноместной функции f и двухместной функции g. Тогда в формуле Н заменим х на с, z – на f(y), v заменим на g(y,u). Все кванторы существования вычеркнем. Получим формулу G=("y)("u)H(c,y,f(y),u,g(g,u)).
Это и есть результат выполнения шага 5.
Приведем пример приведения к СНФ. Пусть F=($x)("y)[P(x,y)®($z)(Q(x,z)&R(y))].
Применяя законы 20 и 23, получаем формулу F1=($x)("y) )($z)[ØP(x,y)Ú(Q(x,z)&R(y))].
Она имеет предваренную нормальную форму. Используя закон 12 приводим бескванторную часть к КНФ: F2=($x)("y) )($z)[ØP(x,y)Ú(Q(x,z)&(ØP(x,y)Ú(R(y))].
Теорема 3.4. Для всякой формулы F существует формула G, имеющая сколемовскую нормальную форму и одновременно выполнимая (или невыполнимая) с F.
Доказательство. Пусть G – результат работы алгоритма приведения к СНФ. То, что результатом работы алгоритма является формула в сколемовской нормальной форме, ясно из описания алгоритма. Формула, которая получается после выполнения шагов 1-4 равносильна исходной, и в частности, одновременно выполнима или не выполнима.
Проанализируем шаг 5. Предположим вначале, что исключается квантор существования, впереди которого нет кванторов общности. Можно считать, что это первый квантор в записи формулы; т.е. E(u1,…,un)=($y)E′(y,u1,…,un). (Формула E′ может содержать кванторы.) Рассмотрим интерпретацию с областью М, при которой формула E выполнима. Выполнимость означает, что найдутся элементы а1,…,anÎM такие, что высказывание (jE)(a1,…,an) или (что тоже самое) высказывание ($y)(jE′)(y,a1,…,an) истинно. Отсюда следует, что существует элемент bÎM такой что высказывание (jE′)(b,a1,…,an) также истинно. Исключение квантора существования по y на пятом шаге приводит к формуле D=E′(c,u1,…,un), где c – константа, отсутствующая в E′. Рассмотрим интерпретацию y, которая совпадает с j на всех символах предикатов и функций, входящих в запись формулы F, и y(с)=b. Тогда (yD)(a1,…,an)=(jE′)(b,a1,…,an). Мы доказали, что если формула E выполнима, то выполнима и формула D.
Предположим теперь, что выполнима формула D(u1,…,un)=E′(c,u1,…,un). Это означает, что существует интерпретация с областью М и элементы а1,…,anÎM такие, что высказывание (yE′)(y(c),a1,…,an) истинно. Но отсюда следует истинность высказывания ($y)(yE′)(y,a1,…,an). Следовательно, формула E(u1,…,un) выполнима. Мы доказали, что из выполнимости формулы D следует выполнимость формулы E.
Рассмотрим теперь случай, когда исключается квантор существования, впереди которого есть k кванторов общности, т.е. E(u1,…,un)=("x1)…("xk)($y)E/(x1,…,xk,y,u1,…,un).
(Формула E/ может содержать кванторы). Исключение квантора по у на шаге 5 приведет к формуле D(u1,…,un)>("x1)…("xk)E(x1,…,xk,f(x1,…,xk),u1,…,un), где f – символ k–местной функции, не содержащийся в Е. Предположим, что формула Е выполнима. Выполнимость означает существование интерпретации j областью М и элементов a1,…,anÎM таких, что высказывание (jE(a1,…,an) истинно. Истинность этого высказывания означает, что для любых элементов x1,…,xkÎM найдется элемент yÎM такой, что высказывание E/( x1,…,xk,y,a1,…,an) истинно. Если для данных элементов x1,…,xk таких элементов y несколько, то зафиксируем один. Тем самым мы определили на М функцию i:Mx…xM®M такую, что высказывание (jE′)(x1,…,xk,i(x1,…,xk),a1,…,an истинно для всех x1,…,xkÎM. Рассмотрим интерпретацию y, которая совпадает с j на всех символах функций и предикатов, входящих в запись формулы Е, и (yf)( x1,…,xn)=i(x1,…,xn). Тогда (yD)(a1,…,an)=("x1)…("xk)(jE/)(x1,…,xk,i(x1,…,xk),a1,…,an), последнее высказывание, как мы видели истинно. Следовательно, формула D(u1,…,un) выполнима. Мы показали, что из выполнимости формулы Е следует выполнимость формулы D.
Пусть выполнима формула D. Это означает, что существует интерпретация y с областью М и элементы a1,…,anÎM такие, что высказывание (yD)(a1,…,an) или (что то же самое) высказывание ("x1)…("xk)(yE/)( x1,…,xk,(yf)(x1,…,xk),a1,…,an) истинно. Отсюда следует, что для любых x1,…,xk найдется y (равный (jf)( x1,…,xk)) такой, что высказывание (yE/)(x1,…,xk,y,a1,…,an) истинно. Следовательно, истинно высказывание ("x1)…("xk)($y)(yE/)( x1,…,xk,y,a1,…,an), т.е. высказывание (yE)(a1,…,an). Мы доказали, что из выполнимости формулы D следует выполнимость формулы Е.
