# Forma prenexa

Una fórmula de la lògica de predicats té forma prenexa si està escrita com a cadena de quantificadors seguits per una part sense quantificar (anomenada matriu).
Tota fórmula és equivalent a una fórmula en forma prenexa. Per exemple, si $\phi (y)$, $\psi (z)$, i $\rho (x)$ són fórmules sense quantificar amb les variables lliures mostrades, llavors
    $\forall x\exists y\exists z(\phi (y)\lor (\psi (z)\rightarrow \rho (x)))$
és en forma normal prenexa amb la matriu $\phi (y)\lor (\psi (z)\rightarrow \rho (x))$, mentre que
    $\forall x((\exists y\phi (y))\lor ((\exists z\psi (z))\rightarrow \rho (x)))$
és lògicament equivalent, però no en forma prenexa.

## Conversió a forma prenexa

Tota fórmula de primer ordre és lògicament equivalent a alguna fórmula en forma prenexa. Hi ha algunes regles de conversió que es poden aplicar recursivament per tal de convertir una fórmula a forma prenexa. Les regles depenen de quina connectiva lògica (o connectives) i quin quantificador (o quantificadors) apareguin a la fórmula.

### Conjunció i disjunció

Les regles per a la conjunció i la disjunció diuen que
    $(\forall x\phi )\land \psi$ és equivalent a $\forall x(\phi \land \psi )$,
    $(\forall x\phi )\lor \psi$ és equivalent a $\forall x(\phi \lor \psi )$;
i
    $(\exists x\phi )\land \psi$ és equivalent a $\exists x(\phi \land \psi )$,
    $(\exists x\phi )\lor \psi$ és equivalent a $\exists x(\phi \lor \psi )$.
Les equivalències són vàlides quan x no apareix com a variable lliure de ψ; si x apareix lliure en ψ, ha de ser substituïda per una altra variable lliure.
Per exemple, en el llenguatge dels anells,
    $(\exists x(x^{2}=1))\land (0=y)$ és equivalent a $\exists x(x^{2}=1\land 0=y)$,
però
    $(\exists x(x^{2}=1))\land (0=x)$ no és equivalent a $\exists x(x^{2}=1\land 0=x)$
perquè la fórmula de l'esquerra és certa en qualsevol anell quan la variable lliure x és igual a 0, mentre 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
    $\lnot \exists x\phi$ és equivalent a $\forall x\lnot \phi$
i
    $\lnot \forall x\phi$ és equivalent a $\exists x\lnot \phi$.

### Implicació

Hi ha quatre regles per a la implicació: dues que eliminen els quantificadors de l'antecedent, i dues més que eliminen els quantificadors del conseqüent. Aquestes regles es poden derivar tot reescrivint la implicació $\phi \rightarrow \psi$ com a $\lnot \phi \lor \psi$ i aplicant després les regles per a la disjunció. De la mateixa manera que les regles de la disjunció, aquestes regles requereixen que la variable quantificada en una subfórmula no aparegui lliure en altra subfórmula.
Les regles per eliminar els quantificadors de l'antecedent són:
    $(\forall x\phi )\rightarrow \psi$ és equivalent a $\exists x(\phi \rightarrow \psi )$,
    $(\exists x\phi )\rightarrow \psi$ és equivalent a $\forall x(\phi \rightarrow \psi )$.
Les regles per eliminar els quantificadors del conseqüent són:
    $\phi \rightarrow (\exists x\psi )$ és equivalent a $\exists x(\phi \rightarrow \psi )$,
    $\phi \rightarrow (\forall x\psi )$ és equivalent a $\forall x(\phi \rightarrow \psi )$.

### Exemple

Suposem que $\phi$, $\psi$ i $\rho$ són fórmules sense quantificar, i que no comparteixen cap variable lliure. Considerem la fórmula
    $(\phi \lor \exists x\psi )\rightarrow \forall z\rho$.
Si apliquem recursivament les regles començant per les subfórmules internes, hom pot obtenir la següent seqüència de fórmules lògicament equivalents:
    $(\exists x(\phi \lor \psi ))\rightarrow \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 )$.
Aquesta no és l'única forma prenexa equivalent a la fórmula original. Per exemple, si transformem el conseqüent abans que l'antecedent, hom pot obtenir la forma prenexa
    $\forall z\forall x((\phi \lor \psi )\rightarrow \rho )$
amb els següents passos:
    $\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 )$.

### Lògica intuïcionista

Les regles per convertir una fórmula a una altra en forma prenexa fa feixuc el maneig de la lògica clàssica. En lògica intuïcionista no és sempre cert que tota fórmula sigui lògicament equivalent a una altra en forma prenexa. La negació d'una connectiva és un obstacle, però no pas l'únic. La implicació també rep un tractament diferent en lògica intuïcionista que en lògica clàssica; en lògica intuïcionista, no és definible mitjançant la negació i la disjunció.

## Ús de la forma prenexa

Alguns sistemes lògics només poden tractar amb una teoria que tingui les fórmules escrites en forma normal prenexa.
Aquest concepte és essencial per tal de desenvolupar la jerarquia aritmètica i la jerarquia analítica.
La demostració de Gödel del seu teorema de completesa per a la lògica de primer ordre pressuposa que totes les fórmules estan reescrites en forma normal prenexa.

## Vegeu també

* Forma normal de Skolem
* Jerarquía analítica

## Bibliografia

* Hinman, Peter G. Fundamentals of mathematical logic. Wellesley, Mass.: A.K. Peters, 2005. ISBN 978-1-56881-262-5.