Forma normal de Prenex

Formalismo de la lógica de primer orden

Una fórmula del cálculo de predicados está en forma normal prenex ^[1] ( PNF ) si se escribe como una cadena de cuantificadores y variables ligadas , llamada prefijo , seguido de una parte libre de cuantificadores, llamada matriz . ^[2] Junto con las formas normales en lógica proposicional (por ejemplo, forma normal disyuntiva o forma normal conjuntiva ), proporciona una forma normal canónica útil en la demostración automática de teoremas .

Toda fórmula de lógica clásica es lógicamente equivalente a una fórmula en forma normal prenex. Por ejemplo, si , y son fórmulas sin cuantificadores con las variables libres que se muestran, entonces ${\displaystyle \phi (y)}$ ${\displaystyle \psi (z)}$ ${\displaystyle \rho (x)}$

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

está en forma normal prenex con matriz , mientras que ${\displaystyle \phi (y)\lor (\psi (z)\rightarrow \rho (x))}$

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

es lógicamente equivalente pero no en forma normal prenex.

Conversión a formato prenex

Toda fórmula de primer orden es lógicamente equivalente (en lógica clásica) a alguna fórmula en forma normal prenexa. ^[3] Existen varias reglas de conversión que se pueden aplicar de forma recursiva para convertir una fórmula a la forma normal prenexa. Las reglas dependen de qué conectivos lógicos aparecen en la fórmula.

Conjunción y disyunción

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

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

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

Las equivalencias son válidas cuando no aparece como variable libre de ; si aparece libre en , se puede renombrar el límite en y obtener el equivalente . ${\displaystyle x}$ ${\displaystyle \psi }$ ${\displaystyle x}$ ${\displaystyle \psi }$ ${\displaystyle x}$ ${\displaystyle (\exists x\phi )}$ ${\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, primero se reescribirá como y luego se colocará en forma normal prenex . ${\displaystyle (\exists x(x^{2}=1))\land (0=x)}$ ${\displaystyle (\exists x'(x'^{2}=1))\land (0=x)}$ ${\displaystyle \exists x'(x'^{2}=1\land 0=x)}$

Negación

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 }$

Implicación

Existen 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 como y aplicando las reglas de disyunción y negación anteriores. Al igual que con las reglas de disyunción, estas reglas requieren que la variable cuantificada en una subfórmula no aparezca libre en la otra subfórmula. ${\displaystyle \phi \rightarrow \psi }$ ${\displaystyle \lnot \phi \lor \psi }$

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

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

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

Las reglas para eliminar cuantificadores del consecuente son:

${\displaystyle \phi \rightarrow (\exists x\psi )}$es equivalente a (bajo el supuesto de que ), ${\displaystyle \exists x(\phi \rightarrow \psi )}$ ${\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, ), la afirmación ${\displaystyle n\in \mathbb {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 hace que la implicación sea una tautología .

Tenga en cuenta que la colocación de los corchetes implica el alcance de la cuantificación , lo cual es muy importante para el significado de la fórmula. Considere las dos afirmaciones siguientes:

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

y su declaración 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.

Ejemplo

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

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

Aplicando recursivamente las reglas comenzando en 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 ordenamiento de dos cuantificadores universales con el mismo alcance no cambia el significado/valor de verdad del enunciado.

Lógica intuicionista

Las reglas para convertir una fórmula a una forma prenexa hacen un uso intensivo de la lógica clásica. En la lógica intuicionista , no es cierto que toda fórmula sea lógicamente equivalente a una fórmula prenexa. El conectivo 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 lógica clásica; en la lógica intuicionista, no es definible mediante disyunción y negación.

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

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

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

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

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

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

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

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

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

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

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

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

Uso de la forma prenex

Algunos cálculos de demostración sólo se ocuparán de una teoría cuyas fórmulas estén escritas en forma normal prenex. El concepto es esencial para desarrollar la jerarquía aritmética y la jerarquía analítica .

La prueba del teorema de completitud de Gödel para la lógica de primer orden presupone que todas las fórmulas han sido reformuladas en la forma normal prenexa.

Los axiomas de Tarski para geometría son un sistema lógico cuyas oraciones pueden escribirse todas en forma universal-existencial , un caso especial de la forma normal prenex que tiene cada cuantificador universal precediendo a cualquier cuantificador existencial , de modo que todas las oraciones pueden reescribirse en la forma , donde es una oración que no contiene ningún cuantificador. Este hecho le permitió a Tarski demostrar que la geometría euclidiana es decidible . ${\displaystyle \forall u}$  ${\displaystyle \forall v}$  ${\displaystyle \ldots }$  ${\displaystyle \exists a}$  ${\displaystyle \exists b}$  ${\displaystyle \phi }$ ${\displaystyle \phi }$

Véase también

• Jerarquía aritmética
• Herbrandización
• Eskolemización

Notas

1. El término 'prenex' proviene del latín praenexus "atado o atado por delante", participio pasado de praenectere [1] (archivado el 27 de mayo de 2011 en [2])
2. Hinman, P. (2005), pág. 110
3. Hinman, P. (2005), pág. 111

Referencias

• Richard L. Epstein (18 de diciembre de 2011). Lógica matemática clásica: los fundamentos semánticos de la lógica. Princeton University Press. pp. 108–. ISBN 978-1-4008-4155-4.
• Peter B. Andrews (17 de abril de 2013). Introducción a la lógica matemática y la teoría de tipos: la verdad a través de la prueba. Springer Science & Business Media. pp. 111–. ISBN 978-94-015-9934-4.
• Elliott Mendelson (1 de junio de 1997). Introducción a la lógica matemática, cuarta edición. CRC Press. pp. 109–. ISBN 978-0-412-80830-2.
• Hinman, Peter (2005), Fundamentos de lógica matemática , AK Peters , ISBN 978-1-56881-262-5