Зарипова, Э.Р. Дискретная математика Часть II. Математическая логика

64 Пусть формула F находится в предваренной нормальной форме (Q 1 x 1 )…(Q n x n )M . Пусть Q r есть квантор существования в префиксе (Q 1 x 1 )…(Q n x n ), 1  r  n . Если никакой квантор всеобщности не стоит в префиксе левее Q r , выбираем константу C , отличную от других констант, входящих в M , заменяем все x r , встречающиеся в M , на C и вычеркиваем (Q r x r ) из префикса. Если m 1 s s Q Q ,..., - список всех кванторов всеобщности, встречающихся левее , ... , s r Q 1 s s 1 2 m r     выбираем новый m -местный функциональный символ f , отличный от других функциональных символов из M , заменяем все x r из M на ) ,..., ( , m 2 1 s s s f x x x и вычеркиваем (Q r x r ) из префикса. Применяем эту процедуру для всех кванторов существования, имеющихся в префиксе формулы F . Последняя из полученных формул есть скулемовская стандартная форма формулы F или просто стандартная форма формулы F . Константы и функции, используемые для замены переменных квантора существования, называются скулемовскими функциями. Пример 13.1. Получить стандартную форму формулы F . )( ) ( , , , , , ). )( )( )( ( )( x y z u v w P x y z u v w       Заменяем переменную x на константу a , переменную u на двухместную функцию f(y,z) , переменную w - на трехместную функцию g(y,z,v) . Получаем следующую стандартную форму формулы F : )( ) ( , , , ( , ), , ( , , )) ( )( y z v P a y z f y z v g y z v    . Будем считать, что множество дизъюнктов S есть конъюнкция всех дизъюнктов из S , где каждая переменная в S управляется квантором всеобщности. Тогда стандартная форма формулы F может быть представлена множеством дизъюнктов S . Теорема. Пусть S - множество дизъюнктов, представляющее стандартную форму формулы F . Тогда F