Математическая логика и теория алгоритмов

в префиксе QiXuQiXi,--- ,QnXi „ п. Если никакой квантор всеобщ­ ности не стоит в префиксе левее Q^Xr, то выбираем новую предметную постоянную с, отличную от всех предметных постоянных в Д и заменяем все А >, встречающиеся в Л, на с и вычергшваем G,AV из префикса. Покажем это на примере. Пусть имеем формулу Зх\^у(Р\{х,у)^0\ {х,а)). Тогда для исключения квантора Зх введем постоянную с. В результате получим формулу; VXP? ic,y)==>Q^i (с,а)). Рассмотрим другой пример. Пусть имеем формулу 3x3y\/z{Pl{x,y,z)=>Q^ {а,Ь,х,у)). Тогда, исключая кванторы существо­ вания, получим: Vz(Pi {c,d,z)^ Qj (a,b,c,d)). Если Qxs^jQxs^!.. ,Qxs^ - список всех квшпхзров всеобщности, встречающихся левее квантора существования Q^r,, 1:^ Si< S2<...< s „,< n, TO выберем новую m-местную функциональную букву/", отличную от других функциональных букв, из В, и заменим все хг в в на f"Xxs 1 j^s 2 J • • •Л „,) и вычеркнем g,jc,. из префикса. Пример. Пусть имеем формулу\/д:ЗХ/''('^.Л')=>б(/1{«).зО)- Введя функцию j(2, с аргументом х и исключая импликацию, получим: Vx(l Р(х, f2ix))vQ(fi(al /2(х))). Пример. Пусть имеем формулу: \/х\/уЗг(Р(д:,у)=> R{x,z/\{x)f2{fi{zy))). Вводя необходимую функцию и исключая импли­ кацию, получим: VxVXl^(^:,}')v/?(x/4(x,>')/i(x)/2(fj(f4(A',j;))))), Проводим описанную процедуру до тех пор, пока не исключим все кванторы существования. Полученная в результате формула есть сколемовская стандартная форма, для краткости стандартная форма формулы Л. Константы и функции, используемые для замены переменных квантора существования, называются сколемовскими функциями. 104