|
|
Ще покажем, че всяка безкванторна формула е еквивалентна на някоя БФОПО. За тази цел ще използваме известните ни еквивалентности
Преди да извършим съответни общи разсъждения, ще разгледаме един конкретен пример, а именно ще покажем как с помощта на някои измежду горните еквивалентности може да се намери една БФОПО, еквивалентна на формулата
Трите еквивалентни замени, извършени в горния пример, могат да се разглеждат като последователни стъпки от изпълнението на един алгоритъм, който е приложим към всяка безкванторна формула и би могъл да бъде описан в общ вид (отделно даваме неговото описание и доказателство, че той наистина преобразува всяка безкванторна формула в еквивалентна на нея БФОПО). Тук ние ще се ограничим само с едно доказателство на твърдението, че всяка безкванторна формула е еквивалентна на някоя БФОПО, без да се занимаваме с начин за нейното намиране. Доказателството обаче ще съдържа в неявен вид едно индуктивно дефинирано съпоставяне на такава еквивалентна БФОПО (фактически същата, която се получава чрез споменатия по-горе алгоритъм).
Ще си послужим с индукция, съобразена с дефиницията за безкванторна формула, като обаче ще доказваме твърдението, че всяка безкванторна формула и нейното отрицание са еквивалентни на някои БФОПО (добавката относно отрицанието я правим, защото е целесъобразна за провеждането на индукцията, макар че за формулировката на окончателния резултат тя всъщност е излишна, понеже и отрицанията на безкванторните формули също са безкванторни формули). За атомарните формули твърдението. че те и техните отрицания са еквивалентни на някои БФОПО, е в сила, защото те и техните отрицания са БФОПО, а пък всяка формула е еквивалентна на себе си. За формулата true също е вярно, че тя и нейното отрицание са еквивалентни на някои БФОПО - самата формула true е БФОПО, а нейното отрицание е еквивалентно на формулата fail, която също е с ограничено ползване на отрицание. Аналогично се проверява истинността на доказваното твърдение и за формулата fail. Да предположим сега, че дадена безкванторна формула F и нейното отрицание са съответно еквивалентни на формули G и G ′, които са с ограничено ползване на отрицание. Тогава формулата ¬ F и нейното отрицание са съответно еквивалентни на G ′ и
G (използваме еквивалентността за отрицание на отрицание). Остава да покажем, че ако дадени две или повече безкванторни формули имат свойството всяка от тях и нейното отрицание да са еквивалентни на някои БФОПО, то конюнкцията и дизюнкцията на дадените формули също имат това свойство. Нека дадените безкванторни формули са F1 , …, Fn , като те са еквивалентни съответно на БФОПО G1 , …, Gn , а отрицанията им - на БФОПО G1′, …, Gn ′. Тогава формулата F1 & … & Fn и нейното отрицание са еквивалентни съответно на БФОПО G1 & … & Gn и на БФОПО G1′ ∨ … ∨ Gn′ (използваме еквивалентността за отрицание на конюнкция). Аналогично се разсъждава за дизюнкцията на F1 , …, Fn .
Последно изменение: 10.06.2004 г.
|
|