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

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

За една формула ще казваме, че е пренексна (или че е в пренексен вид), ако тя може да се получи от някоя безкванторна формула чрез някакъв (евентуално нулев) брой прилагания на действието поставяне на квантор пред дадена формула относно свободна променлива на формулата. Това описание може да се оформи като индуктивна дефиниция, състояща се от следните две точки:
1. Всяка безкванторна формула е пренексна.
2. Всеки път, когато θ е пренексна формула, а ξ е нейна свободна променлива, формулите ∀ξθ и ∃ξθ също са пренексни.

Явното описание на класа на пренексните формули, произтичащо от тази дефиниция, е следното: пренексни формули – това са формулите от вида

Κ₁Κ₂...Κ_nφ, където φ е безкванторна формула, n е неотрицателно цяло число и Κ₁, Κ₂, …, Κ_n са квантори относно свободни променливи на φ, като при n>1 тези променливи са две по две различни. Лесно е да се убедим, че представянето на коя да е пренексна формула в този вид е единствено. Формулата φ в него ще наричаме безкванторна част на разглежданата пренексна формула.

Забележка 1. При възприетата тук дефиниция на понятието пренексна формула, ако пред една формула, дори и тя да е пренексна, поставим квантор относно променлива, която не е свободна променлива на формулата, то получената формула, еквивалентна на дадената, няма да е пренексна.

Ще докажем следното твърдение.

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

Доказателство. За нуждите на това доказателство ще съпоставим на всяка формула неотрицателно цяло число, което ще наричаме брой на кванторите в нея. Дефиницията е напълно естествена и има следния вид:
1. Ако φ е атомарна формула, то броят на кванторите във φ е 0.
2. Ако броят на кванторите в дадена формула φ е n, то броят на кванторите във формулата ¬φ също е n.
3. Ако броят на кванторите във φ е k, а броят на кванторите в ψ е l, то броят на кванторите във всяка от формулите φ&ψ и φ∨ψ е k+l.
4. Ако броят на кванторите във φ е n и ξ е променлива, то броят на кванторите във всяка от формулите ∀ξφ и ∃ξφ е n+1.

Разбира се, коректността на тази дефиниция произтича от еднозначния прочит на формулите. Чрез индукция, съобразена с дефиницията за формула, се показва, че една формула е безкванторна точно тогава, когато броят на кванторите й е 0, и че винаги, когато една субституция σ е приложима към дадена формула φ, съответната формула σφ има същия брой квантори както φ.

Да наречем временно една формула φ редуцируема, ако тя е еквивалентна на някоя формула със същите свободни променливи, но имаща вида Κχ, където Κ е квантор относно някоя променлива, а χ е формула с брой на кванторите, по-малък от този на φ. Ще покажем, че всяка формула с положителен брой на кванторите е редуцируема. За целта е достатъчно да докажем помощното твърдение, че всяка формула е безкванторна или е редуцируема, а това ще направим чрез индукция, съобразена с дефиницията за формула. За краткост да наречем (пак временно) една формула нормална, ако тя е безкванторна или е редуцируема. Атомарните формули са нормални, защото са безкванторни. Формулите от вида ∀ξφ и от вида ∃ξφ, където ξ е променлива, а φ е произволна формула, също са нормални, защото са очевидно редуцируеми. Поради това за провеждането на индукцията остава да се убедим, че нормалността се запазва при образуване на отрицание, на конюнкция и на дизюнкция. За целта ще използваме следните еквивалентности, където φ и θ са произволни формули, ξ е променлива, Κ е квантор относно някоя променлива, която не е свободна променлива на θ, а λ е знак за конюнкция или знак за дизюнкция:

(1) ¬∀ξφ ≡ ∃ξ¬φ, ¬∃ξφ ≡ ∀ξ¬φ,
(2) (Κφλθ) ≡ Κ(φλθ), (θλΚφ) ≡ Κ(θλφ).
Верността на еквивалентностите (1) беше отбелязана в текста „Еквивалентни формули“. Тъй като втората от еквивалентностите (2) следва съвсем лесно от първата от тях, ще се ограничим с доказателство на първата. Възможни са четири случая според вида на квантора Κ и на знака λ. Ще разгледаме подробно два от тях – онези, в които Κ е квантор за общност (другите два случая се разглеждат аналогично). Нека Κ е ∀ξ, където ξ е дадена променлива, която разбира се не е свободна променлива на θ. Тогава доказваната еквивалентност има вида

(∀ξφ&θ) ≡ ∀ξ(φ&θ) или вида (∀ξφ∨θ) ≡ ∀ξ(φ∨θ). Ще я докажем, като покажем, че при всеки избор на структура S и на оценка v в нея са в сила равенствата (∀ξφ&θ)^S,v = ∀ξ(φ&θ)^S,v, (∀ξφ∨θ)^S,v = ∀ξ(φ∨θ)^S,v. Нека S = (Σ,D,I) е произволна структура, а v е произволна оценка в S на променливите. Тогава (∀ξφ&θ)^S,v = min{∀ξφ^S,v,θ^S,v} = min{min{φ^S,v[ξ→d] | d∈D},θ^S,v},
∀ξ(φ&θ)^S,v = min{(φ&θ)^S,v[ξ→d] | d∈D} = min{min{φ^S,v[ξ→d],θ^S,v[ξ→d]} | d∈D},
(∀ξφ∨θ)^S,v = max{∀ξφ^S,v,θ^S,v} = max{min{φ^S,v[ξ→d] | d∈D},θ^S,v},
∀ξ(φ∨θ)^S,v = min{(φ∨θ)^S,v[ξ→d] | d∈D} = min{max{φ^S,v[ξ→d],θ^S,v[ξ→d]} | d∈D}. Благодарение на предположението, че ξ не е свободна променлива на формулата θ, оценката v[ξ→d] съвпада с оценката v върху множеството на свободните променливи на тази формула и поради това стойностите на θ в S при двете оценки са равни. По такъв начин нещата се сведоха до доказателство на равенствата min{min{φ^S,v[ξ→d] | d∈D},θ^S,v} = min{min{φ^S,v[ξ→d],θ^S,v} | d∈D},
max{min{φ^S,v[ξ→d] | d∈D},θ^S,v} = min{max{φ^S,v[ξ→d],θ^S,v} | d∈D}. Верността на тези равенства обаче следва от обстоятелството, че ако за всяко d от D е в сила неравенството φ^S,v[ξ→d] ≥ θ^S,v, то двете страни на първото от равенството са равни на θ^S,v, а двете страни на второто – на min{φ^S,v[ξ→d] | d∈D}, докато пък в противен случай двете страни на първото от равенствата са равни на 0, а двете страни на второто – на 1.

Лесно се проверява, че във всяка от еквивалентностите (1) и (2) при направените преди тях предположения двете страни на еквивалентността имат едни и същи свободни променливи.

За случая на отрицание да предположим, че φ е дадена нормална формула. Ще трябва да покажем, че и формулата ¬φ е нормална. Ако φ е безкванторна, то ¬φ е също безкванторна и значи е нормална. Да разгледаме случая, когато φ е редуцируема. Тогава φ ≡ Κχ, където Κ е квантор относно някоя променлива, χ е някоя формула, имаща по-малък брой квантори от φ, и формулата Κχ има същите свободни променливи както φ. Тогава, използвайки подходяща измежду еквивалентностите (1), получаваме, че

¬φ ≡ ¬Κχ ≡ Κ^~¬χ, където Κ^~ е другият вид квантор относно същата променлива както Κ, като при това са верни равенствата FVAR(Κ^~ ¬χ) = FVAR(¬Κχ) = FVAR(Κχ) = FVAR(φ) = FVAR(¬φ). Като вземем пред вид още, че броят на кванторите се запазва при образуване на отрицание, виждаме също, че броят на кванторите на ¬χ е по-малък от броя на кванторите на ¬φ. С това е показано, че и формулата ¬φ е редуцируема, а значи и нормална.

За случаите на конюнкция и на дизюнкция да предположим, че φ и ψ са нормални формули, а λ е знак за конюнкция или знак за дизюнкция. Ще покажем, че формулата φλψ също е нормална. Ако и двете формули φ и ψ са безкванторни, това е ясно, защото тогава и φλψ ще бъде безкванторна. Затова да разгледаме случая, когато някоя от тях е редуцируема. Нека например φ е редуцируема. Тогава φ ≡ Κχ, където Κ е квантор относно някоя променлива, χ е някоя формула, имаща по-малък брой квантори от φ, и свободните променливи на Κχ са същите както на φ. Ако променливата, относно която е кванторът Κ, не е свободна променлива на ψ, оттук, използвайки първата от еквивалентностите (2), получаваме, че

φλψ ≡ Κ(χλψ), като при това са налице равенствата FVAR(Κ(χλψ)) = FVAR(Κχλψ) = FVAR(Κχ)∪FVAR(ψ) = FVAR(φ)∪FVAR(ψ) = FVAR(φλψ). Тъй като броят на кванторите на формулата χλψ е по-малък от броя на кванторите на формулата φλψ, с това е показано, че и φλψ е редуцируема, а значи и нормална в случая, когато променливата, относно която е кванторът Κ, не е свободна променлива на ψ. Случаят, когато въпросната свързана променлива е свободна променлива на ψ, може да бъде сведен към него с помощта на лемата за преименуване на свързанa променливa (лемата е доказана в текста „Основни следствия от теоремата за стойността на резултат от прилагане на субституция към формула“). Например, нека Κ = ∀ξ, където ξ е свободна променлива на ψ. Да изберем някоя променлива ξ', която не е променлива нито на χ, нито на ψ (такава променлива ξ' съществува, защото променливите на коя да е формула са крайно много, а множеството на всички променливи е безкрайно). Тогава, по споменатата лема и забележката след нейното доказателство, формулата Κχ е еквивалентна на формулата ∀ξ'[ξ/ξ']χ, имаща същите свободни променливи както Κχ. Освен това ∀ξ'[ξ/ξ']χ има същия брой квантори както χ. Следователно ще имаме разгледаното преди малко положение, ако в качеството на ново Κ вземем ∀ξ', а в качеството на ново χ – формулата [ξ/ξ']χ.

След като по този начин завършихме доказателството на помощното твърдение, можем да завършим и доказателството на теоремата за представимост в пренексен вид. Това можем да направим чрез индукция относно броя на кванторите в разглежданата формула. Да наречем една формула пренексно представима, ако тя е еквивалентна на някоя пренексна формула, имаща същите свободни променливи. Формулите, чийто брой на кванторите е 0, са безкванторни и следователно те самите са пренексни, поради което разбира се са пренексно представими. От друга страна, ако при дадено положително цяло число n всички формули с по-малко от n квантори са пренексно представими, то и формулите с брой n на кванторите ще бъдат пренексно представими благодарение на своята редуцируемост. Действително да разгледаме в такъв случай произволна формула φ с брой n на кванторите. Тя ще бъде еквивалентна на някоя формула от вида Κχ със същите свободни променливи, където Κ е квантор относно някоя променлива, а χ е формула с брой на кванторите, по-малък от n, и следователно е пренексно представима, т.е. χ е еквивалентна на някоя пренексна формула χ', имаща същите свободни променливи. При това положение формулата φ ще бъде еквивалентна на формулата Κχ' и тя ще има същите свободни променливи както φ. Ако променливата, относно която е кванторът Κ, е свободна променлива на формулата χ', то Κχ' ще бъде пренексна формула и пренексната представимост на χ ще бъде налице. Ако пък въпросният квантор е относно променлива, която не е свободна променлива на χ', то Κχ' ще бъде еквивалентна на χ' и ще има същите свободни променливи, а понеже това ще важи и за формулата φ, тя отново ще се окаже пренексно представима. _□

Забележка 2. Ако вместо част от еквивалентностите от вида (2) се използват подходящи други еквивалентности, то за някои формули могат да се намерят по-прости еквивалентни на тях пренексни формули със същите свободни променливи, отколкото ако се следва точно пътят от горното доказателство. Две такива еквивалентности са следните, където ξ може да бъде произволна променлива, а φ и ψ могат да бъдат произволни формули:

∀ξφ&∀ξψ ≡ ∀ξ(φ&ψ), ∃ξφ∨∃ξψ ≡ ∃ξ(φ∨ψ). Доказателството на тези еквивалентности не представлява затруднение. Например първата се свежда до това, че при всеки избор на структура S и на оценка v в нея е в сила лесно проверимото равенство min{min{φ^S,v[ξ→d] | d∈D},min{ψ^S,v[ξ→d] | d∈D}^S,v} = min{min{φ^S,v[ξ→d],ψ^S,v[ξ→d]} | d∈D}. С помощта на горните еквивалентности могат да се преработват и формули от по-общите видове ∀ξφ&∀ηψ и ∃ξψ∨∃ηψ, където ξ и η са произволни променливи, а φ и ψ – произволни формули; това може да се прави като при ξ ≠ η първо се извърши преименуване на едната или евентуално на двете свързани променливи.

Пример. Ще приведем в пренексен вид формулата ∀x p(x,y)&∀y q(x,y), където p и q са двуместни предикатни символи. Можем да си послужим със следната верига от еквивалентности:

∀x p(x,y)&∀y q(x,y) ≡ ∀z p(z,y)&∀z q(x,z) ≡ ∀z(p(z,y)&q(x,z)). Ако бихме следвали метода, произтичащ от доказателството на теоремата, би трябвало да си послужим примерно с веригата от еквивалентности ∀x p(x,y)&∀y q(x,y) ≡ ∀z p(z,y)&∀y q(x,y) ≡ ∀z(p(z,y)&∀y q(x,y)) ≡ ∀z(p(z,y)&∀u q(x,u)) ≡ ∀z∀u(p(z,y)&q(x,u)) и резултатът би съдържал един квантор повече от резултата, получен по другия начин.

Забележка 3. С помощта на еквивалентностите, посочени в забележка 2, могат да се докажат по друг начин еквивалентностите (2) в случая, когато Κ е квантор за общност. а λ е знак за конюнкция, и в случая, когато Κ е квантор за съществуване, а λ е знак за дизюнкция. Например, използвайки предположението, че ξ не е свободна променлива на θ, имаме

(∀ξφ&θ) ≡ (∀ξφ&∀ξθ) ≡ ∀ξ(φ&θ).

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

(1)	¬∀ξφ ≡ ∃ξ¬φ, ¬∃ξφ ≡ ∀ξ¬φ,
(2)	`(`Κφλθ`)` ≡ Κ`(`φλθ`)`, `(`θλΚφ`)` ≡ Κ`(`θλφ`)`.