Корисник:Ognjenzivanovic/Пренекс нормална форма

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

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

$\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(\varphi (y)\vee (\psi (z)\to \rho (x)))$

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

$\mathrm{\forall }x((\mathrm{\exists }y\varphi (y))\vee ((\mathrm{\exists }z\psi (z))\to \rho (x)))$

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

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

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

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

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

$(\mathrm{\forall }x\varphi )\wedge \psi$ еквивалентно са $\mathrm{\forall }x(\varphi \wedge \psi )$ под (благим) додатним условом $\mathrm{\exists }x\mathrm{\top }$, или, еквивалентно, $\mathrm{\neg }\mathrm{\forall }x\mathrm{\perp }$ (што значи да постоји најмање један),

$(\mathrm{\forall }x\varphi )\vee \psi$ еквивалентно са $\mathrm{\forall }x(\varphi \vee \psi )$;

и

$(\mathrm{\exists }x\varphi )\wedge \psi$ еквивалентно са $\mathrm{\exists }x(\varphi \wedge \psi )$,

$(\mathrm{\exists }x\varphi )\vee \psi$ еквивалентно са $\mathrm{\exists }x(\varphi \vee \psi )$ под додатним условом $\mathrm{\exists }x\mathrm{\top }$.

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

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

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

али

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

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

Негација

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

$\mathrm{\neg }\mathrm{\exists }x\varphi$ еквивалентно са $\mathrm{\forall }x\mathrm{\neg }\varphi$

и

$\mathrm{\neg }\mathrm{\forall }x\varphi$ еквивалентно са $\mathrm{\exists }x\mathrm{\neg }\varphi$.

Импликација

Постоје четири правила за импликације: два која уклањају квантификаторе из узрока и два која уклањају квантификаторе из консеквента. Ова правила се могу извести преписивањем импликације $\varphi \to \psi$ као $\mathrm{\neg }\varphi \vee \psi$ и примењивањем горе наведених правила за дисјункцију и негацију. Као и код правила за дисјункцију, ова правила захтевају да се променљива квантификована у једној подформули не појављује слободно у другој подформули.

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

$(\mathrm{\forall }x\varphi )\to \psi$ је еквивалентно са $\mathrm{\exists }x(\varphi \to \psi )$ (под претпоставком да $\mathrm{\exists }x\mathrm{\top }$),

$(\mathrm{\exists }x\varphi )\to \psi$ је еквивалентно са $\mathrm{\forall }x(\varphi \to \psi )$.

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

$\varphi \to (\mathrm{\exists }x\psi )$ је еквивалентно са $\mathrm{\exists }x(\varphi \to \psi )$ (под претпоставком да $\mathrm{\exists }x\mathrm{\top }$),

$\varphi \to (\mathrm{\forall }x\psi )$ је еквивалентно са $\mathrm{\forall }x(\varphi \to \psi )$.

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

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

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

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

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

Пример

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

$(\varphi \vee \mathrm{\exists }x\psi )\to \mathrm{\forall }z\rho$.

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

$(\varphi \vee \mathrm{\exists }x\psi )\to \mathrm{\forall }z\rho$.

$(\mathrm{\exists }x(\varphi \vee \psi ))\to \mathrm{\forall }z\rho$,

$\mathrm{\neg }(\mathrm{\exists }x(\varphi \vee \psi ))\vee \mathrm{\forall }z\rho$,

$(\mathrm{\forall }x\mathrm{\neg }(\varphi \vee \psi ))\vee \mathrm{\forall }z\rho$,

$\mathrm{\forall }x(\mathrm{\neg }(\varphi \vee \psi )\vee \mathrm{\forall }z\rho )$,

$\mathrm{\forall }x((\varphi \vee \psi )\to \mathrm{\forall }z\rho )$,

$\mathrm{\forall }x(\mathrm{\forall }z((\varphi \vee \psi )\to \rho ))$,

$\mathrm{\forall }x\mathrm{\forall }z((\varphi \vee \psi )\to \rho )$.

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

$\mathrm{\forall }z\mathrm{\forall }x((\varphi \vee \psi )\to \rho )$

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

$\mathrm{\forall }z((\varphi \vee \mathrm{\exists }x\psi )\to \rho )$

$\mathrm{\forall }z((\mathrm{\exists }x(\varphi \vee \psi ))\to \rho )$,

$\mathrm{\forall }z(\mathrm{\forall }x((\varphi \vee \psi )\to \rho ))$,

$\mathrm{\forall }z\mathrm{\forall }x((\varphi \vee \psi )\to \rho )$.

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

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

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

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

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

Референце

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