Forma normal de Prenex

Las reglas de conjunción y disyunción dicen que

${\displaystyle (\forall x\phi )\land \psi }$es equivalente a${\displaystyle \forall x(\phi \land \psi )}$bajo (leve) condición adicional${\displaystyle \exists x\top }$, o, equivalentemente,${\displaystyle \lnot \forall x\bot }$(lo que significa que existe al menos un individuo),

${\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 )}$bajo condición adicional${\displaystyle \exists x\top }$.

Las equivalencias son válidas cuando${\displaystyle x}$no aparece como una variable libre de${\displaystyle \psi }$; si${\displaystyle x}$parece libre en${\displaystyle \psi }$, se puede cambiar el nombre del límite${\displaystyle x}$en${\displaystyle (\exists x\phi )}$y obtener el equivalente${\displaystyle (\exists x'\phi [x/x'])}$.

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 de 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. Por lo tanto,${\displaystyle (\exists x(x^{2}=1))\land (0=x)}$será reescrito primero como${\displaystyle (\exists x'(x'^{2}=1))\land (0=x)}$y luego poner en forma normal de prenex${\displaystyle \exists x'(x'^{2}=1\land 0=x)}$.

Las reglas de 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 eliminan los cuantificadores del antecedente y dos que eliminan los cuantificadores del consecuente. Estas reglas se pueden derivar reescribiendo la implicación. ${\displaystyle \phi \rightarrow \psi }$como${\displaystyle \lnot \phi \lor \psi }$y aplicando las reglas de disyunción y negación mencionadas anteriormente. Al igual que con las reglas de disyunción, estas reglas requieren que la variable cuantificada en una subfórmula no aparezca como variable libre en la otra subfórmula.

Las reglas para eliminar los cuantificadores del antecedente son (nótese el cambio de cuantificadores):

${\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 eliminar los cuantificadores del consecuente son:

${\displaystyle \phi \rightarrow (\exists x\psi )}$es equivalente a${\displaystyle \exists x(\phi \rightarrow \psi )}$(bajo el supuesto de que${\displaystyle \exists x\top }$),

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

Por ejemplo, cuando el rango de cuantificación es el número natural no negativo (es decir,${\displaystyle n\in \mathbb {N} }$), la declaración

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

es lógicamente equivalente a la afirmación

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

La primera afirmación dice que si x es menor que cualquier número natural, entonces x es menor que cero. La segunda afirmación dice que existe algún número natural n tal que si x es menor que n , entonces x es menor que cero. Ambas afirmaciones son verdaderas. La primera afirmación es verdadera porque si x es menor que cualquier número natural, debe ser menor que el número natural más pequeño (cero). La segunda afirmación es verdadera porque n=0 convierte la implicación en una tautología .

Nótese que la colocación de los paréntesis implica el alcance de la cuantificación , lo cual es muy importante para el significado de la fórmula. Consideremos las dos siguientes afirmaciones:

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

y su enunciado lógicamente equivalente

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

La primera afirmación dice que para cualquier número natural n , si x es menor que n, entonces x es menor que cero. La segunda afirmación dice que si existe algún número natural n tal que x es menor que n , entonces x es menor que cero. Ambas afirmaciones son falsas. La primera afirmación no se cumple para n=2 , porque x=1 es menor que n , pero no menor que cero. La segunda afirmación no se cumple para x=1 , porque el número natural n=2 satisface x<n , pero x=1 no es menor que cero.

Supongamos que${\displaystyle \phi }$,${\displaystyle \psi }$, y${\displaystyle \rho }$son fórmulas sin cuantificadores y ninguna de estas fórmulas comparte ninguna variable libre. Considere la fórmula

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

Aplicando recursivamente las reglas comenzando por las subfórmulas más internas, se puede obtener la siguiente secuencia de fórmulas lógicamente equivalentes:

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

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

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

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

${\displaystyle \forall x(\neg (\phi \lor \psi )\lor \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, al tratar el consecuente antes del antecedente en el ejemplo anterior, la forma prenexa

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

se puede obtener:

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

El orden de los dos cuantificadores universales con el mismo alcance no cambia el significado/valor de verdad de la afirmación.

Las reglas para convertir una fórmula a la forma prenexa se basan en gran medida en la lógica clásica. En la lógica intuicionista , no toda fórmula es lógicamente equivalente a una fórmula prenexa. El conector de negación es un obstáculo, pero no el único. El operador de implicación también se trata de manera diferente en la lógica intuicionista que en la clásica; en la lógica intuicionista, no se puede definir mediante la disyunción y la negación.

La interpretación BHK ilustra por qué algunas fórmulas no tienen una forma prenexa intuicionistamente equivalente. En esta interpretación, una demostración de

${\displaystyle (\exists x\phi )\rightarrow \exists y\psi \qquad (1)}$

es una función que, dado un x concreto y una prueba de${\displaystyle \phi (x)}$, produce una y concreta y una prueba de${\displaystyle \psi (y)}$En este caso, es admisible que el valor de y se calcule a partir del valor dado de x . Una demostración de

${\displaystyle \exists y(\exists x\phi \rightarrow \psi ),\qquad (2)}$

Por otro lado, produce un único valor concreto de y y una función que convierte cualquier prueba de${\displaystyle \exists x\phi }$en una prueba de${\displaystyle \psi (y)}$. Si cada x satisface${\displaystyle \phi }$puede utilizarse para construir una y que satisfaga${\displaystyle \psi }$pero no se puede construir tal y sin conocimiento de tal x entonces la fórmula (1) no será equivalente a la fórmula (2).

Las reglas para convertir una fórmula a la forma prenexa que fallan en la lógica intuicionista son:

(1)${\displaystyle \forall x(\phi \lor \psi )}$implica${\displaystyle (\forall x\phi )\lor \psi }$,

(2)${\displaystyle \forall x(\phi \lor \psi )}$implica${\displaystyle \phi \lor (\forall x\psi )}$,

(3)${\displaystyle (\forall x\phi )\rightarrow \psi }$implica${\displaystyle \exists x(\phi \rightarrow \psi )}$,

(4)${\displaystyle \phi \rightarrow (\exists x\psi )}$implica${\displaystyle \exists x(\phi \rightarrow \psi )}$,

(5)${\displaystyle \lnot \forall x\phi }$implica${\displaystyle \exists x\lnot \phi }$,

( x no aparece como una variable libre de${\displaystyle \,\psi }$en (1) y (3); x no aparece como una variable libre de${\displaystyle \,\phi }$en (2) y (4)).