Корисник:Огњензивановиц/Пренекс нормална форма

Формула предикатског рачуна је у пренекс нормалној форми (PNF) ако је написана као низ квантификатора и везаних променљивих, који се назива префикс, а затим следи део без квантификатора, који се зове матрица. Заједно са нормалним облицима у исказном рачуну (нпр. дисјунктивни нормални облик или коњунктивни нормални облик), он обезбеђује канонску нормалну форму корисну у аутоматском доказивању теорема.

Свака формула у класичној логици је логички еквивалентна формули у пренекс нормалном облику. На пример, ако су $\phi (y)$, $\psi (z)$, и $\rho (x)$ формуле без квантификатора са слободним променљивим приказаним тада је:

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

у пренекс нормалном облику са матрицом $\phi (y)\lor (\psi (z)\rightarrow \rho (x))$, док је

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

логички еквивалентан, али не у пренекс нормалном облику.

Конверзија у пренекс форму

Свака формула првог реда је логички еквивалентна (у класичној логици) некој формули у пренекс нормалном облику. Постоји неколико правила конверзије која се могу рекурзивно применити за претварање формуле у пренекс нормални облик. Правила зависе од тога који се логички оператори појављују у формули.

Коњункција и дисјункција

Правила за коњункцију и дисјункцију кажу да је:

$(\forall x\phi )\land \psi$ еквивалентно са $\forall x(\phi \land \psi )$ под (благим) додатним условом $\exists x\top$, или, еквивалентно, $\lnot \forall x\bot$ (што значи да постоји најмање један),

$(\forall x\phi )\lor \psi$ еквивалентно са $\forall x(\phi \lor \psi )$;

и

$(\exists x\phi )\land \psi$ еквивалентно са $\exists x(\phi \land \psi )$,

$(\exists x\phi )\lor \psi$ еквивалентно са $\exists x(\phi \lor \psi )$ под додатним условом $\exists x\top$.

Еквиваленције су важеће када се $x$ не појављује као слободна променљива од $\psi$; ако се $x$ појављује као слободан у $\psi$, може се преименовати везано $x$ у $(\exists x\phi )$ и добити еквивалент $(\exists x'\phi [x/x'])$.

На пример, у језику алгебарских прстенова,

$(\exists x(x^{2}=1))\land (0=y)$ је еквивалентно са $\exists x(x^{2}=1\land 0=y)$,

али

$(\exists x(x^{2}=1))\land (0=x)$ није еквивалентно са $\exists x(x^{2}=1\land 0=x)$

јер је формула са леве стране тачна у било ком прстену када је слободна променљива y једнака 0, док формула са десне стране нема слободних променљивих и нетачна је у било ком нетривијалном прстену. Што значи да ће $(\exists x(x^{2}=1))\land (0=x)$ прво бити написано као $(\exists x'(x'^{2}=1))\land (0=x)$ и онда пребачено у пренекс нормалну форму $\exists x'(x'^{2}=1\land 0=x)$.

Негација

Правила за негацију кажу да је:

$\lnot \exists x\phi$ еквивалентно са $\forall x\lnot \phi$

и

$\lnot \forall x\phi$ еквивалентно са $\exists x\lnot \phi$.

Импликација

Постоје четири правила за импликације: два која уклањају квантификаторе из узрока и два која уклањају квантификаторе из консеквента. Ова правила се могу извести преписивањем импликације $\phi \rightarrow \psi$ као $\lnot \phi \lor \psi$ и примењивањем горе наведених правила за дисјункцију и негацију. Као и код правила за дисјункцију, ова правила захтевају да се променљива квантификована у једној подформули не појављује слободно у другој подформули.

Правила за уклањање квантификатора из узрока су (обратите пажњу на промену квантификатора):

$(\forall x\phi )\rightarrow \psi$ је еквивалентно са $\exists x(\phi \rightarrow \psi )$ (под претпоставком да $\exists x\top$),

$(\exists x\phi )\rightarrow \psi$ је еквивалентно са $\forall x(\phi \rightarrow \psi )$.

Правила за уклањање квантификатора из консеквента су:

$\phi \rightarrow (\exists x\psi )$ је еквивалентно са $\exists x(\phi \rightarrow \psi )$ (под претпоставком да $\exists x\top$),

$\phi \rightarrow (\forall x\psi )$ је еквивалентно са $\forall x(\phi \rightarrow \psi )$.

На пример, када је опсег квантификације ненегативан природни број (тј. $n\in \mathbb {N}$), исказ

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

је логички еквивалентан исказу

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

Прва изјава каже да је за било који природан број n, ако је x мање од n, онда је x мање од нуле. Друга изјава каже да ако постоји неки природан број n такав да је x мање од n, онда је x мање од нуле. Обе изјаве су нетачне. Прва изјава не важи за n=2, јер је x=1 мање од n, али не мање од нуле. Друга изјава не важи за x=1, јер природан број n=2 задовољава x<n, али x=1 није мање од нуле.

Пример

Претпоставимо да су $\phi$, $\psi$, и $\rho$ формуле без квантификатора и ниједна од ових формула не дели ниједну слободну променљиву. Размотримо формулу

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

Рекурзивном применом правила почевши од најдубљих подформула, може се добити следећи низ логички еквивалентних формула:

$(\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 )$.

Ово није једина пренекс форма која је еквивалентна оригиналној формули. На пример, бавећи се консеквентом пре узрока у примеру изнад, пренекс форма

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

се може добити

$\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 )$.

Редослед два универзална квантификатора са истим опсегом не мења значење/истинитост исказа.

Употреба пренекс форми

Неки доказни рачуни ће се бавити само теоријом чије су формуле написане у пренекс нормалној форми. Концепт је од суштинског значаја за развој аритметичке хијерархије и аналитичке хијерархије.

Геделов доказ његове теореме комплетности за логику првог реда претпоставља да су све формуле преведене у пренекs нормалну форму.

Тарскијеви аксиоми за геометрију су логички систем чије се реченице све могу написати у универзално-егзистенцијалној форми, посебном случају пренекс нормалне форме код које је сваки универзални квантификатор претходи било ком егзистенцијалном квантификатору, тако да се све реченице могу преписати у облику $\forall u$ $\forall v$ $\ldots$ $\exists a$ $\exists b$ $\phi$ где је $\phi$ реченица која не садржи никакав квантификатор. Ова чињеница је омогућила Тарском да докаже да је еуклидска геометрија одлучива.

Референце

• 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.