ИНДУКТИВНО ДЕФИНИРАНО СЪПОСТАВЯНЕ НА ЕКВИВАЛЕНТНА БФОПО
За да докажем, че всяка безкванторна формула е еквивалентна на някоя БФОПО, ние доказахме индуктивно, че всяка безкванторна формула F и нейното отрицание са съответно еквивалентни на някои БФОПО G и G ′, които да означим сега с F+ и F-. Като проследим внимателно въпросното индуктивно доказателство, виждаме, че формулите F+ и F- могат да се определят индуктивно по следния начин, където точка 1 важи за всяка безкванторна формула F, а точки 2 и 3 - за всяко цяло число n, по-голямо от 1, и за произволни безкванторни формули F1, …, Fn :
0а. Ако F е атомарна формула, то F+ = F, F- = ¬ F .
0б. true+ = true, true- = fail, fail+ = fail, fail- = true.
1. ( ¬ F )+ = F-, ( ¬ F )- = F+.
2. (F1 & … & Fn)+ = F1+ & … & Fn+, (F1 & … & Fn)- = F1- ∨ … ∨ Fn-.
3. (F1 ∨ … ∨ Fn)+ = F1+ ∨ … ∨ Fn+, (F1 ∨ … ∨ Fn)- = F1- & … & Fn-.
Бихме могли, без да се занимаваме изобщо с гореспоменатото доказателство, да използваме тази индуктивна дефиниция, за да съпоставим на всяка безкванторна формула F две БФОПО F+ и F-, след което да докажем индуктивно, че за всяка безкванторна формула F са в сила еквивалентностите
F ≡ F+, ¬ F ≡ F-.
Също чрез индукция може да се докаже, че за всяка безкванторна формула F алгоритъмът чрез последователни еквивалентни замени, за който стана дума преди доказателството, дава резултат F+, ако го приложим към F, и резултат F-, ако го приложим към ¬ F .
Последно изменение: 10.06.2004 г.