Prenex forma normal - Prenex normal form

Una fórmula del cálculo de predicados está en forma normal prenex ( PNF ) si se escribe como una cadena de cuantificadores y variables ligadas , llamado prefijo , seguido de una parte libre de cuantificador, llamada matriz .

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

${\ Displaystyle \ forall x \ existe 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 ((\ existe y \ phi (y)) \ lor ((\ existe z \ psi (z)) \ rightarrow \ rho (x)))}$

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

Conversión a forma prenex

Cada fórmula de primer orden es lógicamente equivalente (en lógica clásica) a alguna fórmula en forma normal prenex. Hay 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 de conjunción y disyunción dicen que

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

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

y

${\ Displaystyle (\ existe x \ phi) \ land \ psi}$ es equivalente a , ${\ Displaystyle \ existe x (\ phi \ land \ psi)}$

${\ Displaystyle (\ existe x \ phi) \ lor \ psi}$ es equivalente a bajo condición adicional . ${\ Displaystyle \ existe x (\ phi \ lor \ psi)}$${\ Displaystyle \ existe x \ top}$

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

Por ejemplo, en el idioma de los anillos ,

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

pero

${\ Displaystyle (\ existe x (x ^ {2} = 1)) \ land (0 = x)}$ no es equivalente a ${\ Displaystyle \ existe 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. Así que primero se reescribirá como y luego se pondrá en forma normal prenex . ${\ Displaystyle (\ existe x (x ^ {2} = 1)) \ land (0 = x)}$${\ displaystyle (\ existe x '(x' ^ {2} = 1)) \ land (0 = x)}$${\ Displaystyle \ existe x '(x' ^ {2} = 1 \ land 0 = x)}$

Negación

Las reglas para la negación dicen que

${\ Displaystyle \ lno \ existe x \ phi}$ es equivalente a ${\ Displaystyle \ forall x \ lnot \ phi}$

y

${\ Displaystyle \ lno \ forall x \ phi}$ es equivalente a . ${\ Displaystyle \ existe 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 anteriores. Al igual que con las reglas para la 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 (observe el cambio de cuantificadores):

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

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

Las reglas para eliminar cuantificadores del consecuente son:

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

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

Ejemplo

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

${\ Displaystyle (\ phi \ lor \ existe 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 \ existe x \ psi) \ rightarrow \ forall z \ rho}$ .

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

${\ Displaystyle \ neg (\ existe 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 prenex

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

Puede ser obtenido:

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

${\ Displaystyle \ forall z ((\ existe 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)}$ .

Lógica intuicionista

Las reglas para convertir una fórmula a la 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 prenex. El conectivo de la 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 se puede definir utilizando la disyunción y la negación.

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

${\ Displaystyle (\ existe x \ phi) \ rightarrow \ existe 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 puede calcular el valor de y a partir del valor dado de x . Una prueba de ${\ Displaystyle \ phi (x)}$${\ Displaystyle \ psi (y)}$

${\ Displaystyle \ existe y (\ existe 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 en una prueba de . Si cada x satisfactorio se puede usar para construir un y satisfactorio pero no se puede construir tal y sin el conocimiento de tal x, entonces la fórmula (1) no será equivalente a la fórmula (2). ${\ Displaystyle \ existe x \ phi}$${\ Displaystyle \ psi (y)}$${\ Displaystyle \ phi}$${\ Displaystyle \ psi}$

Las reglas para convertir una fórmula en 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 \ existe x (\ phi \ rightarrow \ psi)}$

(4) implica , ${\ Displaystyle \ phi \ rightarrow (\ existe x \ psi)}$${\ Displaystyle \ existe x (\ phi \ rightarrow \ psi)}$

(5) implica , ${\ Displaystyle \ lno \ forall x \ phi}$${\ Displaystyle \ existe x \ lnot \ phi}$

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

Uso de formulario prenex

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

La demostración 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.

El axioma de Tarski para la geometría es un sistema lógico cuyas oraciones se pueden escribir todas en forma existencial universal , un caso especial de la forma normal prenex que tiene cada cuantificador universal precediendo a cualquier cuantificador existencial , de modo que todas las oraciones se pueden reescribir 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 \ existe a}$ ${\ Displaystyle \ existe b}$ ${\ Displaystyle \ phi}$${\ Displaystyle \ phi}$

Ver también

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

Notas

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: a la verdad a través de la prueba . Springer Science & Business Media. 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, P. (2005), Fundamentos de lógica matemática , AK Peters , ISBN   978-1-56881-262-5