Forma normal prenexa

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

${\displaystyle (\forall x\phi )\land \psi }$ es equivalente a ${\displaystyle \forall x(\phi \land \psi )}$,

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

Y

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

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

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

Por ejemplo, en el lenguaje de los anillos,

${\displaystyle (\exists x(x^{2}=1))\land (0=y)}$ es equivalente a ${\displaystyle \exists x(x^{2}=1\land 0=y)}$,

pero

${\displaystyle (\exists x(x^{2}=1))\land (0=x)}$ no es equivalente a ${\displaystyle \exists x(x^{2}=1\land 0=x)}$

porque la fórmula en la izquierda es verdadera en cualquier anillo cuando la variable libre x es igual a 0, mientras que la fórmula de la derecha no tiene variables libres, y es falsa en cualquier anillo no-trivial.

Las reglas para la negación dicen que

${\displaystyle \lnot \exists x\phi }$ es equivalente a ${\displaystyle \forall x\lnot \phi }$

y

${\displaystyle \lnot \forall x\phi }$ es equivalente a ${\displaystyle \exists x\lnot \phi }$.

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 ${\displaystyle \phi \rightarrow \psi }$ como ${\displaystyle \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:

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

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

Las reglas para remover cuantificadores del consecuente son:

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

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

Supóngase que ${\displaystyle \phi }$, ${\displaystyle \psi }$, y ${\displaystyle \rho }$ son fórmulas sin cuantificar y no comparten variable libre alguna. Considérese la fórmula

${\displaystyle (\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:

${\displaystyle (\exists x(\phi \lor \psi ))\rightarrow \forall z\rho }$,

${\displaystyle \forall x((\phi \lor \psi )\rightarrow \forall z\rho )}$,

${\displaystyle \forall x(\forall z((\phi \lor \psi )\rightarrow \rho )))}$,

${\displaystyle \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 antecedente en el ejemplo, la forma prenexa

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

Puede ser obtenida:

${\displaystyle \forall z((\phi \lor \exists x\psi )\rightarrow \rho )}$

${\displaystyle \forall z((\exists x(\phi \lor \psi ))\rightarrow \rho )}$,

${\displaystyle \forall z(\forall x((\phi \lor \psi )\rightarrow \rho ))}$,

${\displaystyle \forall z\forall x((\phi \lor \psi )\rightarrow \rho )}$.

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 implicació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.

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