Математическая логика и теория алгоритмов. Для изучающих компьютерные науки
Отметим, что стандартная форма As формулы А определяется не единст венным образом, ибо сколемовские функции можно вводить неоднозначно. Пусть формула А приведена в предваренную нормальную форму, а ее мат рица представлена в к.н.ф., т.е. А = (QiXiQ2X2...QnXr) В = (QiXiQ2X2...QnXr) Di&D2&...&Dm, где {QiXiQ2X2...QnXn) - префикс формулы А, а Di,D2,...,Dm - элементарные суммы (в логике предикатов). Положим, что стандартная форма J для Л травяа As=(QixiQ2X2... QnXn) Ci&C2&...&Cnt, где в префиксе опущены кван торы существования, а Q получены из Z)/ (1< i< т) введением сколемовских функций вместо переменных кванторов существования. Имеет место следую щая теорема. Теорема 3.8. (теорема Сколема) Замкнутая формула А является противо речием тогда и только тогда, когда её стандартная форма As является проти воречием. Очевидно, что эту теорему можно сформулировать следующим образом. Замкнутая формула А выполнима тогда и только тогда, когда её стандартная форма As выполнима. Доказательство. Приведём/! в предваренную нормальную форму: А= QiXi Q2X2 ... QnXnB. Пусть имеется только один квантор существования QrX^\ A =VXi... VXr-iBXrVXr+l... VXnB(Xi,X2, ... ,Xr). Положим b ±7... VXr-lVXr+1... VXnB(Xi,X2, ... ,Xr.i,f(Xi,X2, ... ,Xr.i), Xr+1, ... ,Xn), гдс f(xi, X2,... ,Xr.i) - сколемовская функция. Покажем, чтоЛ противоречива тогда и только тогда, когда противоречива Пусть А - противоречие. Допустим, что As не противоречие, следователь но, существует интерпретация, в которой As выполнима, т.е. для Vxi, \/х2,, Vxr- I Вхг =f(xi,x2, ... ,Xr.i), ЧТО при Vxr+1, ..., Vxn формула В принимает значение "И " а это противоречит тому, что А - противоречие. Следовательно, As противоре чие. Обратно, пусть As - противоречие. Допустим, что А - не противоречие, т.е. существует интерпретация, в которой А - выполнимо. Следовательно, для Vxi, Vx2,. . .,VX]..i найдется Х]. такое, что при Vx^+i,. . .,Vxn, формула В при нимает значение И. Введем функцию f(xi,. . .,X]..i)=X].. Тогда ясно, что As =n, что противоречит условию As - противоречие. Если в префиксе имеется т кванторов существования, то доказательство проводится аналогично. Следствие 3.1. Если Л - противоречие и ...,Qn) С1&С2&... &Ст, то A-Ci&C2&,...,&Cm.. Следствие 3.2. Пусть As - стандартная форма формулы А и пусть А - противоречие. Тогда ~ А. 72
Made with FlippingBook
RkJQdWJsaXNoZXIy MTY0OTYy