Forma normal de Prenex

Formalismo de la lógica de primer orden

Una fórmula del cálculo de predicados está en forma normal del prenexo ^[1] ( PNF ) si se escribe como una cadena de cuantificadores y variables ligadas , llamada prefijo , seguida 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 automatizada de teoremas .

Cada fórmula de la lógica clásica es lógicamente equivalente a una fórmula en forma normal prenexa. 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 la forma normal prenex.

Conversión al formulario prenex

Cada 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 prenex. Las reglas dependen de qué conectivos lógicos aparecen en la fórmula.

Conjunción y disyunción

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

${\displaystyle (\forall x\phi )\land \psi }$es equivalente a bajo (leve) condición adicional , o, de manera equivalente, (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 }$equivale 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 cambiar el nombre del encuadernado 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 prenex y luego se pondrá en forma normal . ${\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 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 }$

Implicación

Hay cuatro reglas para la implicación : dos que eliminan cuantificadores del antecedente y dos que eliminan 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 (obsérvese 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 (a saber ), la declaración ${\displaystyle n\in \mathbb {N} }$

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

es lógicamente equivalente a la declaració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 última 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 ciertas. La primera afirmación es cierta porque si x es menor que cualquier número natural, debe ser menor que el número natural más pequeño (cero). La última afirmación es cierta porque n=0 hace que la implicación sea una tautología .

Tenga en cuenta que la colocación de corchetes implica el alcance de la cuantificación , lo cual es muy importante para el significado de la fórmula. Considere las siguientes dos 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 última 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 afirmación anterior no es válida para n=2 , porque x=1 es menor que n , pero no menor que cero. La última afirmación no es válida 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 no hay dos de estas fórmulas que compartan ninguna variable libre. Considere 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 de prenexo equivalente a la fórmula original. Por ejemplo, al tratar con el consecuente antes del antecedente en el ejemplo anterior, la forma prenexa

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

Puede ser obtenido:

${\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 declaración.

Lógica intuicionista

Las reglas para convertir una fórmula a la forma prenex hacen un uso intensivo de la lógica clásica. En lógica intuicionista , no es cierto que cada fórmula sea lógicamente equivalente a una fórmula prenexa. La conectiva 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 lógica intuicionista, no se puede definir mediante disyunción y negación.

La interpretación de BHK ilustra por qué algunas fórmulas no tienen una forma de prenexo 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 otro lado, produce un valor concreto único de y y una función que convierte cualquier prueba de en una prueba de . Si cada x que satisface se puede utilizar para construir un y que satisface , pero no se puede construir tal y sin conocer 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 la 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 una variable libre de en (1) y (3); x no aparece como una variable libre de (2) y (4)). ${\displaystyle \,\psi }$ ${\displaystyle \,\phi }$

Uso del formulario prenex

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

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

Los axiomas de Tarski para la geometría son un sistema lógico cuyas oraciones pueden escribirse en forma universal-existencial , un caso especial de la forma normal prenexo 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 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 }$

Ver 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. Prensa de la Universidad de Princeton. págs.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: hacia la verdad a través de la prueba. Medios de ciencia y negocios de Springer. págs.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. Prensa CRC. págs.109–. ISBN 978-0-412-80830-2.
• Hinman, Peter (2005), Fundamentos de la lógica matemática , AK Peters , ISBN 978-1-56881-262-5