Una fórmula del cálculo de predicados está en prenex [1] forma normal ( PNF ) si se escribe como una cadena de cuantificadores y variables ligadas , llamado prefijo , seguido de una parte libre de cuantificador, llamada matriz . [2]
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 libres de cuantificadores con las variables libres que se muestran entonces
está en forma normal prenex con matriz , tiempo
es lógicamente equivalente pero no en 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. [3] 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
- es equivalente a bajo condición adicional (leve) , o equivalente, (lo que significa que existe al menos un individuo),
- es equivalente a ;
y
- es equivalente a ,
- es equivalente a bajo condición adicional .
Las equivalencias son válidas cuando no aparece como una variable libre de; Si parece libre en , se puede cambiar el nombre del límite en y obtener el equivalente .
Por ejemplo, en el idioma de los anillos ,
- es equivalente a ,
pero
- no es equivalente a
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. Entonces será reescrito primero como y luego poner en forma normal prenex .
Negación
Las reglas para la negación dicen que
- es equivalente a
y
- es equivalente a .
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 aplicar 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.
Las reglas para eliminar cuantificadores del antecedente son (observe el cambio de cuantificadores):
- es equivalente a (bajo el supuesto de que ),
- es equivalente a .
Las reglas para eliminar cuantificadores del consecuente son:
- es equivalente a (bajo el supuesto de que ),
- es equivalente a .
Ejemplo
Suponer que , , y son fórmulas sin cuantificadores y ninguna de estas fórmulas comparte ninguna variable libre. Considere la fórmula
- .
Aplicando recursivamente las reglas comenzando en las subfórmulas más internas, se puede obtener la siguiente secuencia de fórmulas lógicamente equivalentes:
- .
- ,
- ,
- ,
- ,
- ,
- ,
- .
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
Puede ser obtenido:
- ,
- ,
- .
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
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
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 satisfactoriase puede utilizar para construir una y satisfactoriapero 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).
Las reglas para convertir una fórmula a la forma prenex que fallan en la lógica intuicionista son:
- (1) implica ,
- (2) implica ,
- (3) implica ,
- (4) implica ,
- (5) implica ,
( x no aparece como una variable libre deen (1) y (3); x no aparece como una variable libre de en (2) y (4)).
Uso del 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.
Los axiomas de Tarski para la geometría son un sistema lógico cuyas oraciones pueden escribirse 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 pueden reescribirse en la forma , dónde es una oración que no contiene ningún cuantificador. Este hecho permitió a Tarski demostrar que la geometría euclidiana es decidible .
Ver tambié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). Una 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