yandex rtb 1
ГоловнаЗворотній зв'язок
yande share
Главная->Математика і інформатика->Содержание->5.3. Скулемовская  стандартная форма

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

5.3. Скулемовская  стандартная форма

Пусть формула F находится в предваренной нормальной форме (Qlxl)...(Qnxn)M где М есть конъюнктивная нормальная форма. Положим, Qr есть квантор существования в префиксе (Qlxl)...(Qnxn), lrn. Если никакой квантор всеобщности не стоит в префиксе левее Qr, мы выберем константу с, отличную от других констант, входящих в М, заменим все хг, встречающиеся в М, на с и вычеркнем (Qrxr) из префикса. Если Qs,,...,Qsm-список всех кванторов всеобщности, встречающихся левее Qr ls1<s2<…<sm<r, мы выберем новый m-местный функциональный символ f, отличный от других функциональных символов, заменим все х, в М на f(Xs1,...,Xsm) и вычеркнем (Qгхг) из префикса. Затем весь этот процесс применим для всех кванторов существования в префиксе; последняя из полученных формул есть скулемовская стандартная форма - для краткости, стандартная форма (ССФ) формулы F. Константы и функции, используемые для замены переменных квантора существования, называются скулемовскими функциями.

Пример.    Получим стандартную форму формулы xyzuvwP(x,y,u,v,w).

В этой формуле левее х нет никаких кванторов всеобщности, левее u стоят y и z, а левее w стоят y, z и v. Следовательно, мы заменим переменную х на константу а, переменную u - на двуместную функцию f(y,z), Переменную w - на трехместную функцию g(y,z,v). Таким образом, мы получаем следующую стандартную форму написанной выше формулы: yzv P(a,y,z,f(y,z),v,g(y,z,v)).

Для рассмотренных выше посылок из примера 4.2 ССФ имеет вид:

xy((D(y)vL(x,y))&P(x))  y((D(y)vL(a,y))&P(a)), xy(Q(y)v¬L(x,y)vP(x)).

Определение 5.2. Дизъюнкт есть дизъюнкция литер.

Однолитерный дизъюнкт называется единичным дизъюнктом. Когда дизъюнкт не содержит никаких литер, его называют пустым дизъюнктом. Так как пустой дизъюнкт не содержит литер, которые могли бы быть истинными при любых интерпретациях, то пустой дизъюнкт всегда ложен. Пустой дизъюнкт обозначается посредством□.

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

Теорема 5.2. Пусть S - множество дизъюнктов, которые представляют стандартную форму формулы F. Тогда F противоречива в том и только в том случае, когда S противоречива.

Доказательство. Без потери общности можно положить, что F находится в ПНФ, т. е. F=(Qlxl)...(Qnxn)M [x1,…,xn]. (Мы используем М[х1,...,хn], чтобы указать, что матрица М содержит переменные (х1,...,хn). Пусть Qr - первый квантор существования. Пусть

F1=(xl)...( xr-1)(Qr+1 xr+l)...(Qnxn)M[x1,...,xr-1,…,f(x1,...,xr-1),xr+1,...,xn],      где      f      -скулемовская функция, соответствующая хr, 1гn. Мы хотим показать, что F    противоречива    тогда    и    только    тогда,     когда     F,     противоречива. Предположим,    что    F    противоречива.    Если    F,    непротиворечива,    то существует такая интерпретация I, что F1, истинна в I, т.е. для всех х1,...,хг., существует   по   крайней   мере   один   элемент   (а   именно   f(x1,...,xr-1,)),   для которого   (Qr+1 xr+l)...(Qnxn)M[x1,...,xr-1f(xl....,xr-1,),xr+1,...,xn].  истинна   в    I.   Таким образом    F     истинна    в    I,    что    противоречит    предположению,    что    F противоречива.  Следовательно,  F1 должна  быть  противоречива.  С  другой стороны, предположим, что F1 противоречива. Если F непротиворечива, то существует такая интерпретация I на области D, что F истинна в I, т.е. для всех        х1,..,хг-1        существует        такой        элемент        хг,        что (Qr+lxr+1)...(Qnxn)M[x1,…,xrl, f(x1,...,xr-l),xr+1,...,xn]      истинна       в       I.       Расширим интерпретацию   I,   для   всех   х1,...,xr-1 в   D,   т.e.   f(xl,…,xг-1)=xr.   Пусть   это расширение      I      обозначается      Г.      Ясно,      что      для      всех      x1,...,хr-1 (Qr+1 xr+1)...(Qnxn)M[xl,...,xr-1.,f(x1,...,xr-1.,),xr+1,...,xn] истинна в I', т. е. F, истинна в I`, что противоречит предположению, что F противоречива. Следовательно, F должна противоречивой. Предположим теперь, что в F имеется m кванторов существования. Пусть F0=F. Пусть Fk получается из Fk-1, заменой первого квантора существования в Fк-1 скулемовской функцией. k=l,...,m. Ясно, что S=Fm.  используя те  же  рассуждения  что даны были  выше,   мы  можем показать,    что    Fk.:    противоречива    тогда    и    только    тогда,    когда     Fk противоречива    при     к=1,...,m.    Следовательно,    мы     заключаем,    что     F противоречива    тогда    и    только    тогда,    когда    S    противоречива,    что    и требовалось доказать.

Пусть S - стандартная форма формулы F. Если F противоречива, то по доказанной выше теореме FS. Если F непротиворечива, заметим, что, вообще говоря, F не эквивалентна В. Например, пусть F=xP(x) и =Р(а) есть стандартная форма формулы F. Пусть I есть следующая интерпретация: область D = {1, 2}, значение для а: а = 1, значения для Р: P(1)=F, Р(2)=Т. Тогда ясно, что F истинна в I, но S ложна в I. Таким образом FS.

Далее, если мы имеем F=F1^...^Fn мы можем отдельно получить множество дизъюнктов S1, где каждый S, представляет стандартную форму F1 i=l,...n. Затем пусть S=S1v...vSn. Тогда F противоречива тогда и только тогда, когда S противоречива.

 

33