Forma normal prenexa

En llògica de primer orde, una fòrmula ben formada té forma normal prenexa si està escrita encapçalada per una cadena de quantificadors existencials o universals, seguits per una fòrmula sense quantificadors llògics, designada com a «matriu».

Tota fòrmula és equivalent en llògica clàssica a una fòrmula en forma normal prenexa. Per eixemple, si $\varphi (y)$, $\psi (z)$, i $\rho (x)$ són fòrmules sense quantificar en les variables lliures mostrades, despuix

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

està en forma normal prenexa, en la matriu $\varphi (y)\vee (\psi (z)\to \rho (x))$, mentres que

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

és llògicament equivalent pero no en forma prenexa.

El terme «prenexa» ve del llatí praenexus, passat participi de praenectere, que significa «nugat» o «nugat en el front».

Quan una fòrmula en forma normal prenexa solament posseïx quantificadors universals, es diu que està en forma normal de Skolem. Tota fòrmula en forma normal prenexa és llògicament equivalent a una en forma normal de Skolem, i la manera d'aplegar d'una a una atra es denomina skolemisació.

Conversió a forma prenexa

Tota fòrmula de primer orde és llògicament equivalent a alguna fòrmula en forma prenexa. Hi ha algunes regles de conversió que poden ser aplicades recursivamente per a convertir una fòrmula a forma prenexa. Les regles depenen de quines conectiva llògica (o conectivas) i quantificador (o quantificadors) apareguen en la fòrmula.

Conjunció i disjunció

Les regles per a la conjunció i la disjunció diuen que

$(\mathrm{\forall }x\varphi )\wedge \psi$ és equivalent a $\mathrm{\forall }x(\varphi \wedge \psi )$,

$(\mathrm{\forall }x\varphi )\vee \psi$ és equivalent a $\mathrm{\forall }x(\varphi \vee \psi )$;

I

$(\mathrm{\exists }x\varphi )\wedge \psi$ és equivalent a $\mathrm{\exists }x(\varphi \wedge \psi )$,

$(\mathrm{\exists }x\varphi )\vee \psi$ és equivalent a $\mathrm{\exists }x(\varphi \vee \psi )$.

Les equivalència són vàlides quan x no apareix com a variable lliure de ψ; si x sí apareix lliure en ψ, deu ser reemplaçada per una atra variable lliure.

Per eixemple, en el llenguage dels anells,

$(\mathrm{\exists }x(x^2=1))\wedge (0=y)$ és equivalent a $\mathrm{\exists }x(x^2=1\wedge 0=y)$,

pero

$(\mathrm{\exists }x(x^2=1))\wedge (0=x)$ no és equivalent a $\mathrm{\exists }x(x^2=1\wedge 0=x)$

perque la fòrmula en l'esquerra és verdadera en qualsevol anell quan la variable lliure x és igual a 0, mentres que la fòrmula de la dreta no té variables lliures, i és falsa en qualsevol anell no-trivial.

Negació

Les regles per a la negació diuen que

$\mathrm{\neg }\mathrm{\exists }x\varphi$ és equivalent a $\mathrm{\forall }x\mathrm{\neg }\varphi$

i

$\mathrm{\neg }\mathrm{\forall }x\varphi$ és equivalent a $\mathrm{\exists }x\mathrm{\neg }\varphi$.

Implicació

Hi ha quatre regles per a l'implicació: dos que remouen els quantificadors de l'antecedent i dos que remouen els quantificadors del conseqüent. Estes regles poden ser derivades reescrivint l'implicació $\varphi \to \psi$ com $\mathrm{\neg }\varphi \vee \psi$ i aplicant les regles per a la disjunció de dalt. Tal com les regles de la disjunció, estes regles requerixen que la variable quantificada en una subfórmula no aparega lliure en una atra subfórmula.

Les regles per a remoure quantificadors de l'antecedent són:

$(\mathrm{\forall }x\varphi )\to \psi$ és equivalent a $\mathrm{\exists }x(\varphi \to \psi )$,

$(\mathrm{\exists }x\varphi )\to \psi$ és equivalent a $\mathrm{\forall }x(\varphi \to \psi )$.

Les regles per a remoure quantificadors del conseqüent són:

$\varphi \to (\mathrm{\exists }x\psi )$ és equivalent a $\mathrm{\exists }x(\varphi \to \psi )$,

$\varphi \to (\mathrm{\forall }x\psi )$ és equivalent a $\mathrm{\forall }x(\varphi \to \psi )$.

Eixemple

Suponga's que $\varphi$, $\psi$, i $\rho$ són fòrmules sense quantificar i no compartixen variable lliure alguna. Considere's la fòrmula

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

Aplicant recursivamente les regles escomençant per les subfórmulas internes, la següent seqüència de fòrmules llògicament equivalents poden obtindre's:

$(\mathrm{\exists }x(\varphi \vee \psi ))\to \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 )$.

Esta no és l'única forma prenexa equivalent a la fòrmula original. Per eixemple, abordant el conseqüent abans que l'antecedent en l'eixemple, la forma prenexa

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

Pot ser obtinguda:

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

Llògica intuicionista

Les regles per a convertir una fòrmula a una en forma prenexa fa engorroso el maneig de la llògica clàssica. En llògica intuicionista no succeïx que tota fòrmula és llògicament equivalent a una fòrmula prenexa. La negació d'una conectiva és un obstàcul, pero no és l'únic. L'implicació també rep un tractament en llògica intuicionista que en la llògica clàssica; en llògica intuicionista, no és definible usant la negació i la disjunció.

Us de la forma prenexa

Alguns sistemes llògics solament poden tractar en una teoria les fòrmules de la qual estiguen escrites en forma normal prenexa. El concepte és essencial per a desenrollar la jerarquia aritmètica i la jerarquia analítica. La prova de Gödel de la seua teorema de completitud per a la llògica de primer orde presupon que totes les fòrmules han segut reescrites en formal normal prenexa.

Vore també

• Herbrandization
• Forma normal de Skolem
• Jerarquia analítica