Korisnik:Ognjenzivanovic/Preneks normalna forma

Formula predikatskog računa je u preneks normalnoj formi (PNF) ako je napisana kao niz kvantifikatora i vezanih promenljivih, koji se naziva prefiks, a zatim sledi deo bez kvantifikatora, koji se zove matrica. Zajedno sa normalnim oblicima u iskaznom računu (npr. disjunktivni normalni oblik ili konjunktivni normalni oblik), on obezbeđuje kanonsku normalnu formu korisnu u automatskom dokazivanju teorema.

Svaka formula u klasičnoj logici je logički ekvivalentna formuli u preneks normalnom obliku. Na primer, ako su $\phi (y)$, $\psi (z)$, i $\rho (x)$ formule bez kvantifikatora sa slobodnim promenljivim prikazanim tada je:

$\forall x\exists y\forall z(\phi (y)\lor (\psi (z)\rightarrow \rho (x)))$

u preneks normalnom obliku sa matricom $\phi (y)\lor (\psi (z)\rightarrow \rho (x))$, dok je

$\forall x((\exists y\phi (y))\lor ((\exists z\psi (z))\rightarrow \rho (x)))$

logički ekvivalentan, ali ne u preneks normalnom obliku.

Konverzija u preneks formu

Svaka formula prvog reda je logički ekvivalentna (u klasičnoj logici) nekoj formuli u preneks normalnom obliku. Postoji nekoliko pravila konverzije koja se mogu rekurzivno primeniti za pretvaranje formule u preneks normalni oblik. Pravila zavise od toga koji se logički operatori pojavljuju u formuli.

Konjunkcija i disjunkcija

Pravila za konjunkciju i disjunkciju kažu da je:

$(\forall x\phi )\land \psi$ ekvivalentno sa $\forall x(\phi \land \psi )$ pod (blagim) dodatnim uslovom $\exists x\top$, ili, ekvivalentno, $\lnot \forall x\bot$ (što znači da postoji najmanje jedan),

$(\forall x\phi )\lor \psi$ ekvivalentno sa $\forall x(\phi \lor \psi )$;

i

$(\exists x\phi )\land \psi$ ekvivalentno sa $\exists x(\phi \land \psi )$,

$(\exists x\phi )\lor \psi$ ekvivalentno sa $\exists x(\phi \lor \psi )$ pod dodatnim uslovom $\exists x\top$.

Ekvivalencije su važeće kada se $x$ ne pojavljuje kao slobodna promenljiva od $\psi$; ako se $x$ pojavljuje kao slobodan u $\psi$, može se preimenovati vezano $x$ u $(\exists x\phi )$ i dobiti ekvivalent $(\exists x'\phi [x/x'])$.

Na primer, u jeziku algebarskih prstenova,

$(\exists x(x^{2}=1))\land (0=y)$ je ekvivalentno sa $\exists x(x^{2}=1\land 0=y)$,

ali

$(\exists x(x^{2}=1))\land (0=x)$ nije ekvivalentno sa $\exists x(x^{2}=1\land 0=x)$

jer je formula sa leve strane tačna u bilo kom prstenu kada je slobodna promenljiva y jednaka 0, dok formula sa desne strane nema slobodnih promenljivih i netačna je u bilo kom netrivijalnom prstenu. Što znači da će $(\exists x(x^{2}=1))\land (0=x)$ prvo biti napisano kao $(\exists x'(x'^{2}=1))\land (0=x)$ i onda prebačeno u preneks normalnu formu $\exists x'(x'^{2}=1\land 0=x)$.

Negacija

Pravila za negaciju kažu da je:

$\lnot \exists x\phi$ ekvivalentno sa $\forall x\lnot \phi$

i

$\lnot \forall x\phi$ ekvivalentno sa $\exists x\lnot \phi$.

Implikacija

Postoje četiri pravila za implikacije: dva koja uklanjaju kvantifikatore iz uzroka i dva koja uklanjaju kvantifikatore iz konsekventa. Ova pravila se mogu izvesti prepisivanjem implikacije $\phi \rightarrow \psi$ kao $\lnot \phi \lor \psi$ i primenjivanjem gore navedenih pravila za disjunkciju i negaciju. Kao i kod pravila za disjunkciju, ova pravila zahtevaju da se promenljiva kvantifikovana u jednoj podformuli ne pojavljuje slobodno u drugoj podformuli.

Pravila za uklanjanje kvantifikatora iz uzroka su (obratite pažnju na promenu kvantifikatora):

$(\forall x\phi )\rightarrow \psi$ je ekvivalentno sa $\exists x(\phi \rightarrow \psi )$ (pod pretpostavkom da $\exists x\top$),

$(\exists x\phi )\rightarrow \psi$ je ekvivalentno sa $\forall x(\phi \rightarrow \psi )$.

Pravila za uklanjanje kvantifikatora iz konsekventa su:

$\phi \rightarrow (\exists x\psi )$ je ekvivalentno sa $\exists x(\phi \rightarrow \psi )$ (pod pretpostavkom da $\exists x\top$),

$\phi \rightarrow (\forall x\psi )$ je ekvivalentno sa $\forall x(\phi \rightarrow \psi )$.

Na primer, kada je opseg kvantifikacije nenegativan prirodni broj (tj. $n\in \mathbb {N}$), iskaz

$[\forall n\in \mathbb {N} (x<n)]\rightarrow (x<0)$

je logički ekvivalentan iskazu

$\exists n\in \mathbb {N} [(x<n)\rightarrow (x<0)]$

Prva izjava kaže da je za bilo koji prirodan broj n, ako je x manje od n, onda je x manje od nule. Druga izjava kaže da ako postoji neki prirodan broj n takav da je x manje od n, onda je x manje od nule. Obe izjave su netačne. Prva izjava ne važi za n=2, jer je x=1 manje od n, ali ne manje od nule. Druga izjava ne važi za x=1, jer prirodan broj n=2 zadovoljava x<n, ali x=1 nije manje od nule.

Primer

Pretpostavimo da su $\phi$, $\psi$, i $\rho$ formule bez kvantifikatora i nijedna od ovih formula ne deli nijednu slobodnu promenljivu. Razmotrimo formulu

$(\phi \lor \exists x\psi )\rightarrow \forall z\rho$.

Rekurzivnom primenom pravila počevši od najdubljih podformula, može se dobiti sledeći niz logički ekvivalentnih formula:

$(\phi \lor \exists x\psi )\rightarrow \forall z\rho$.

$(\exists x(\phi \lor \psi ))\rightarrow \forall z\rho$,

$\neg (\exists x(\phi \lor \psi ))\lor \forall z\rho$,

$(\forall x\neg (\phi \lor \psi ))\lor \forall z\rho$,

$\forall x(\neg (\phi \lor \psi )\lor \forall z\rho )$,

$\forall x((\phi \lor \psi )\rightarrow \forall z\rho )$,

$\forall x(\forall z((\phi \lor \psi )\rightarrow \rho ))$,

$\forall x\forall z((\phi \lor \psi )\rightarrow \rho )$.

Ovo nije jedina preneks forma koja je ekvivalentna originalnoj formuli. Na primer, baveći se konsekventom pre uzroka u primeru iznad, preneks forma

$\forall z\forall x((\phi \lor \psi )\rightarrow \rho )$

se može dobiti

$\forall z((\phi \lor \exists x\psi )\rightarrow \rho )$

$\forall z((\exists x(\phi \lor \psi ))\rightarrow \rho )$,

$\forall z(\forall x((\phi \lor \psi )\rightarrow \rho ))$,

$\forall z\forall x((\phi \lor \psi )\rightarrow \rho )$.

Redosled dva univerzalna kvantifikatora sa istim opsegom ne menja značenje/istinitost iskaza.

Upotreba preneks formi

Neki dokazni računi će se baviti samo teorijom čije su formule napisane u preneks normalnoj formi. Koncept je od suštinskog značaja za razvoj aritmetičke hijerarhije i analitičke hijerarhije.

Gedelov dokaz njegove teoreme kompletnosti za logiku prvog reda pretpostavlja da su sve formule prevedene u preneks normalnu formu.

Tarskijevi aksiomi za geometriju su logički sistem čije se rečenice sve mogu napisati u univerzalno-egzistencijalnoj formi, posebnom slučaju preneks normalne forme kod koje je svaki univerzalni kvantifikator prethodi bilo kom egzistencijalnom kvantifikatoru, tako da se sve rečenice mogu prepisati u obliku $\forall u$ $\forall v$ $\ldots$ $\exists a$ $\exists b$ $\phi$ gde je $\phi$ rečenica koja ne sadrži nikakav kvantifikator. Ova činjenica je omogućila Tarskom da dokaže da je euklidska geometrija odlučiva.

Reference

• Richard L. Epstein (18 December 2011). Classical Mathematical Logic: The Semantic Foundations of Logic. Princeton University Press. стр. 108–. ISBN 978-1-4008-4155-4. 
• Peter B. Andrews (17 April 2013). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Springer Science & Business Media. стр. 111–. ISBN 978-94-015-9934-4. 
• Elliott Mendelson (1 June 1997). Introduction to Mathematical Logic, Fourth Edition. CRC Press. стр. 109–. ISBN 978-0-412-80830-2.