 |
|
АкушерствоАнатомияАнестезиологияВакцинопрофилактикаВалеологияВетеринарияГигиенаЗаболеванияИммунологияКардиологияНеврологияНефрологияОнкологияОториноларингологияОфтальмологияПаразитологияПедиатрияПервая помощьПсихиатрияПульмонологияРеанимацияРевматологияСтоматологияТерапияТоксикологияТравматологияУрологияФармакологияФармацевтикаФизиотерапияФтизиатрияХирургияЭндокринологияЭпидемиология |
Теорема о СНФТеорема 3.4. Для всякой формулы F существует формула G, имеющая сколемовскую нормальную форму и одновременно выполнимая (или невыполнимая) с F.
Доказательство. Пусть G – результат работы алгоритма приведения к СНФ. То, что результатом работы алгоритма является формула в сколемовской нормальной форме, ясно из описания алгоритма. Формула, которая получается после выполнения шагов 1-4 равносильна исходной, и в частности, одновременно выполнима или не выполнима. Проанализируем шаг 5. Предположим вначале, что исключается квантор существования, впереди которого нет кванторов общности. Можно считать, что это первый квантор в записи формулы; т.е. E(u1,…,un)=($y)E′(y,u1,…,un). (Формула E′ может содержать кванторы.) Рассмотрим интерпретацию j с областью М, при которой формула 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). Это означает, что существует интерпретация y с областью М и элементы а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 следует выполнимость формулы Е. Дата добавления: 2015-09-27 | Просмотры: 462 | Нарушение авторских прав |