Привеждане на формули в пренексен вид

ПРИВЕЖДАНЕ НА ФОРМУЛИ В ПРЕНЕКСЕН ВИД

Ще наричаме една формула пренексно представима, ако тя е еквивалентна на някоя пренексна формула със същото множество на свободните променливи (намирането на такава пренексна формула се нарича привеждане на дадената формула в пренексен вид). Благодарение на свойството а) от въпроса „Еквивалентни формули“ всяка пренексна формула е пренексно представима, а свойството в) от същия въпрос гарантира, че всяка формула, която е еквивалентна на пренексно представима формула със същото множество на свободните променливи, също е пренексно представима. Ще докажем следното важно твърдение:

Теорема за пренексна представимост. Всяка формула е пренексно представима.

Доказателството на тази теорема ще извършим чрез индукция, съобразена с дефиницията на понятието формула. Разбира се, атомарните формули, както и по-общо всички безкванторни формули, са пренексни формули и поради това са очевидно пренексно представими. При това положение е достатъчно да покажем, че пренексната представимост се запазва при образуване на отрицание, на конюнкция и на дизюнкция и при поставяне на квантор. Това ще направим, като формулираме и докажем съответни леми.

Лема за запазване на пренексната представимост при образуване на отрицание. Отрицанието на всяка пренексно представима формула е пак пренексно представима формула.

Доказателство. Благодарение на свойството д) от въпроса „Еквивалентни формули“ е достатъчно да докажем, че отрицанието на всяка пренексна формула е пренексно представима формула. Това можем да направим чрез индукция, съобразена с индуктивната дефиниция на понятието пренексна формула. Ако една формула е безкванторна, нейното отрицание е пак безкванторна формула и следователно е пренексно представима формула. Да предположим сега, че отрицанието на дадена пренексна формула φ е пренексно представима формула. Ще докажем, че са пренексно представими и формулите ¬ ∀η φ и ¬ ∃η φ , където η е коя да е свободна променлива на φ. Нека θ е такава пренексна формула, че ¬ φ ≡ θ и FVAR(¬ φ) = FVAR(θ) . Тогава свойствата ж) и д) от въпроса „Еквивалентни формули“ дават, че

¬ ∀η φ ≡ ∃η ¬ φ ≡ ∃η θ , откъдето по свойството в) от същия въпрос получаваме, че формулата ¬ ∀η φ е еквивалентна на формулата ∃η θ . Тъй като FVAR(θ) = FVAR(¬ φ) = FVAR(φ) променливата η е свободна променлива на θ, тъй че формулата ∃η θ е пренексна, а освен това FVAR(¬ ∀η φ) = FVAR(∀η φ) = FVAR(φ) \ {η} = FVAR(θ) \ {η} = FVAR(∃η θ) . Разглежданията за формулата ¬ ∃η φ са напълно аналогични. _□

Лема за запазване на пренексната представимост при поставяне на квантор. При поставяне на квантор пред пренексно представима формула винаги се получава пак пренексно представима формула.

Доказателство. Благодарение на свойството д) от въпроса „Еквивалентни формули“ е достатъчно да докажем, че при поставяне на квантор пред пренексна формула винаги се получава пренексно представима формула. Това се вижда много лесно. Ако кванторът е по свободна променлива на дадената пренексна формула, то получената формула е даже пренексна, а в противен случай получената формула е еквивалентна на дадената и има същото множество на свободните променливи. _□

Лема за запазване на пренексната представимост при образуване на конюнкция и на дизчнкция. Конюнкцията и дизюнкцията на кои да е две пренексно представими формули са пак пренексно представими формули.

Доказателство. Ще разгледаме случая на конюнкция, а случаят на дизюнкция е аналогичен. Благодарение на свойството г) от въпроса „Еквивалентни формули“ е достатъчно да докажем, че конюнкцията на кои да е две пренексни формули е пренексно представима.
Първо ще докажем това за конюнкцията на безкванторна формула с пренексна формула. Нека φ е произволна безкванторна формула. Ще покажем, че за всяка пренексна формула ψ конюнкцията φ & ψ е пренексно представима. Ще използваме индукция относно броя на свързаните променливи на ψ. Ако този брой е 0, то формулата ψ също е безкванторна и тогава формулата φ & ψ, бидейки безкванторна, е даже пренексна. Да предположим сега, че при даден избор на естественото число n конюнкцията на φ с всяка пренексна формула, имаща брой n на свързаните променливи, е пренексно представима. Нека ψ е пренексна формула, чиито свързани променливи са n+1 на брой. Ще покажем, че конюнкцията φ & ψ е пренексно представима. От забележка 2 във въпроса „Преименуване на свързана променлива на пренексна формула“ е ясно, че формулата ψ е еквивалентна на някоя пренексна формула със същия брой свързани променливи и същото множество на свободните променливи, на която най-левият квантор е по променлива, непринадлежаща на множеството FVAR(φ). Избираме някоя пренексна формула с изброените свойства. Тя има вида Κχ , където χ е пренексна формула с брой n на свързаните променливи, а Κ е квантор по някоя свободна променлива η на χ. Тъй като η не е свободна променлива на φ, свойствата а), г), й) и в) от въпроса „Еквивалентни формули“ позволяват да заключим, че

φ & ψ ≡ Κ(φ & χ) . Освен това FVAR(Κ(φ & χ)) = FVAR(φ & χ) \ {η} = (FVAR(φ) ∪ FVAR(χ)) \ {η} = (FVAR(φ) \ {η}) ∪ (FVAR(χ) \ {η}) = FVAR(φ) ∪ FVAR(Κχ) = FVAR(φ) ∪ FVAR(ψ) = FVAR(φ & ψ) . При това положение, за да установим пренексната представимост на конюнкцията φ & ψ , достатъчно е да покажем, че е пренексно представима формулата Κ(φ & χ) . Последното обаче следва от лемата за запазване на пренексната представимост при поставяне на квантор и от обстоятелството, че съгласно индуктивното предположение конюнкцията φ & χ е пренексно представима.
За да докажем, че конюнкцията на две произволни пренексни формули е пренексно представима, ще предположим, че е дадена произволна пренексна формула ψ, и ще покажем, че за всяка пренексна формулаφ конюнкцията φ & χ е прексно представима. Това ще направим чрез индукция относно броя на свързаните променливи във φ. Ако този брой е 0, то φ е безкванторна и имаме разгледания по-горе случай. Индуктивната стъпка пък е аналогична на индуктивната стъпка в горните разсъждения, като главната разлика е в използването на свойството к) от въпроса „Еквивалентни формули“ вместо свойството й). _□

Забележка. Доказателството на теоремата за пренексна представимост съдържа в неявен вид метод за привеждане на произволна формула в пренексен вид. В някои случаи обаче по този метод може да се получи по-сложна пренексна формула, отколкото се налага. Такова е положението например с привеждането в пренексен вид на формулата

∀X p(X) & ∀X q(X) , където p и q са едноместни предикатни символи. По свойството з) от въпроса „Еквивалентни формули“ тя е еквивалентна на формулата ∀X (p(X) & q(X)) , която очевидно е пренексна, а освен това и двете формули са с празно множество на свободните променливи. Привеждането на дадената формула в пренексен вид по метода, произтичащ от доказателството, би довел до формула от по-сложния вид ∀ξ ∀ξ' (p(ξ) & q(ξ')) , където ξ и ξ' са различни променливи.

Последно изменение: 7.09.2008 г.