Forma normal prenexa

Una formula de la lógica de predicados tiene forma prenexa​ si está escrita como una cadena de cuantificadores seguidos por una parte sin cuantifcar (designada como matriz).

Toda fórmula es equivalente en lógica clásica a una fórmula en forma prenexa. Por ejemplo, si $\phi (y)$, $\psi (z)$, y $\rho (x)$ son fórmulas sin cuantificar con las variables libres mostradas, luego

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

Es en forma normal prenexa con la mtriz $\phi (y)\lor (\psi (z)\rightarrow \rho (x))$, mientras que

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

Es lógicamente equivalente pero no en forma prenexa.

Conversión a forma prenexa

Toda fórmula de primer orden es lógica equivalente (en lógica clasíca) a alguna fórmula en forma prenexa. Hay algunas reglas de conversión que pueden ser aplicadas recursivamente para convertir una fórmula a forma prenexa. Las reglas dependen de qué conectiva lógica (o conectivas) aparezcan en la fórmula.

Conjunción y disyunción

Las reglas para la conjunción y la disyunción dicen que

$(\forall x\phi )\land \psi$ $\forall x(\phi \land \psi )$,

$(\forall x\phi )\lor \psi$ es equivalente a $\forall x(\phi \lor \psi )$;

Y

$(\exists x\phi )\land \psi$ es equivalente a $\exists x(\phi \land \psi )$,

$(\exists x\phi )\lor \psi$ es equivalente a $\exists x(\phi \lor \psi )$.

Las equivalencias son válidas cuando x no aparece como variable libre de ψ; si x no aparece libre en ψ, debe ser reemplazada por otra variable libre.

For example, in the language of rings,

$(\exists x(x^{2}=1))\land (0=y)$ is equivalent to $\exists x(x^{2}=1\land 0=y)$,

but

$(\exists x(x^{2}=1))\land (0=x)$ is not equivalent to $\exists x(x^{2}=1\land 0=x)$

because the formula on the left is true in any ring when the free variable x is equal to 0, while the formula on the right has no free variables and is false in any nontrivial ring.

Negación

Las reglas para la negación dicen que

$\lnot \exists x\phi$ es equivalente a $\forall x\lnot \phi$

y

$\lnot \forall x\phi$ es equivalente a $\exists x\lnot \phi$.

Implicación

Hay cuatro reglas para la implicación: dos que remueven los cuantificadores del antecedente y dos que remueven los cuantificadores del consecuente. Estas reglas pueden ser derivadas reescribiendo la implicación $\phi \rightarrow \psi$ como $\lnot \phi \lor \psi$ y aplicando las reglas para la disyunción de arriba. Tal como las reglas de la disyunción, estas reglas requieren que la variable cuantificada en una subfórmula no aparezca libre en otra subfórmula.

Las reglas para remover cuantificadores del antecedente son:

$(\forall x\phi )\rightarrow \psi$ es equivalente a $\exists x(\phi \rightarrow \psi )$,

$(\exists x\phi )\rightarrow \psi$ es equivalente a $\forall x(\phi \rightarrow \psi )$.

Las reglas para remover cuantificadores del consecuente son:

$\phi \rightarrow (\exists x\psi )$ es equivalente a $\exists x(\phi \rightarrow \psi )$,

$\phi \rightarrow (\forall x\psi )$ es equivalente a $\forall x(\phi \rightarrow \psi )$.

Ejemplo

Supóngase que $\phi$, $\psi$, y $\rho$ son fórmulas sin cuantificar y no comparten variable libre alguna. Cnonsiderese la fórmula

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

Aplicando recursivamente las reglas empezando por las subfórmulas internas, la siguiente secuencia de fórmulas lógicamente equivalentes pueden obtenerse:

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

Esta no es la única forma prenexa equivalente a la fórmula original. Por ejemplo, abordando el consecuente antes que el anecedente en el ejemplo, la forma prenexa

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

Puede ser obtenida:

$\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 intuicionista

Las reglas para convertir una fórmula a una en forma prenexa hace engorroso el manejo de la lógica clásica. En lógica intuicionista no sucede que toda fórmula es lógicamente equivalente a una fórmula prenexa. La negación de una conectiva es un obstáculo, pero no es el único. La implicción también recibe un tratamiento en lógica intuicionista que en la lógica clásica; en lógica intuicionista, no es definible usando la negación y la disyunción.

Uso de la forma prenexa

Some proof calculi will only deal with a theory whose formulae are written in prenex normal form. The concept is essential for developing the arithmetical hierarchy and the analytical hierarchy.

Gödel's proof of his completeness theorem for first-order logic presupposes that all formulae have been recast in prenex normal form.

See also

• Herbrandization
• Skolemization
• Arithmetical hierarchy

References

• Hinman, P. (2005), Fundamentals of Mathematical Logic, A K Peters, ISBN 978-1-56881-262-5 .