Forma normal prenexa
En lógica de primer orden, una fórmula bien formada tiene forma normal prenexa si está escrita encabezada por una cadena de cuantificadores existenciales o universales, seguidos por una fórmula sin cuantificadores lógicos, designada como «matriz».

Toda fórmula es equivalente en lógica clásica a una fórmula en forma normal prenexa. Por ejemplo, si
, , y  son fórmulas sin cuantificar con las variables libres mostradas, luego

está en forma normal prenexa, con la matriz , mientras que

es lógicamente equivalente pero no en forma prenexa.

El término «prenexa» viene del latín praenexus, pasado participio de praenectere, que significa «atado» o «atado en el frente».

Cuando una fórmula en forma normal prenexa solo posee cuantificadores universales, se dice que está en forma normal de Skolem. Toda fórmula en forma normal prenexa es lógicamente equivalente a una en forma normal de Skolem, y la manera de llegar de una a otra se denomina skolemización.

Conversión a forma prenexa 

Toda fórmula de primer orden es lógicamente equivalente a alguna fórmula en forma prenexa. Hay algunas reglas de conversión que pueden ser aplicadas recursivamente para convertir una fórmula a forma prenexa. Las reglas dependen de qué conectiva lógica (o conectivas) y cuantificador (o cuantificadores) aparezcan en la fórmula.

Conjunción y disyunción 

Las reglas para la conjunción y la disyunción dicen que 
 es equivalente a ,
 es equivalente a ;
Y 
 es equivalente a ,
 es equivalente a .
Las equivalencias son válidas cuando x no aparece como variable libre de ψ; si x sí aparece libre en ψ, debe ser reemplazada por otra variable libre.

Por ejemplo, en el lenguaje de los anillos,
 es equivalente a ,
pero
 no es equivalente a 
porque la fórmula en 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.

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 remueven los cuantificadores del antecedente y dos que remueven los cuantificadores del consecuente. Estas reglas pueden ser derivadas reescribiendo la implicación
 como  y aplicando las reglas para la disyunción de arriba. Tal como las reglas de la disyunción, estas reglas requieren que la variable cuantificada en una subfórmula no aparezca libre en otra subfórmula.
 

Las reglas para remover cuantificadores del antecedente son:
 es equivalente a ,
 es equivalente a .

Las reglas para remover cuantificadores del consecuente son:
 es equivalente a ,
 es equivalente a .

Ejemplo 

Supóngase que , , y  son fórmulas sin cuantificar y no comparten variable libre alguna. Considérese la fórmula
.
Aplicando recursivamente las reglas empezando por las subfórmulas internas, la siguiente secuencia de fórmulas lógicamente equivalentes pueden obtenerse:
,
,
,
.

Esta no es la única forma prenexa equivalente a la fórmula original. Por ejemplo, abordando el consecuente antes que el antecedente en el ejemplo, la forma prenexa

Puede ser obtenida: 

,
,
.

Lógica intuicionista 

Las reglas para convertir una fórmula a una en forma prenexa hace engorroso el manejo de la lógica clásica. En lógica intuicionista no sucede que toda fórmula es lógicamente equivalente a una fórmula prenexa. La negación de una conectiva es un obstáculo, pero no es el único. La implicación también recibe un tratamiento en lógica intuicionista que en la lógica clásica; en lógica intuicionista, no es definible usando la negación y la disyunción.

Uso de la forma prenexa 

Algunos sistemas lógicos solo pueden tratar con 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 reescritas en formal normal prenexa.

Véase también 
 Herbrandization
 Forma normal de Skolem
 Jerarquía analítica

Referencias

Bibliografía 
 

Prenexa
Lógica matemática
En lógica de primer orden , una fórmula bien formada tiene forma normal prenexa si está escrita encabezada por una cadena de cuantificadores existenciales o universales , seguidos por una fórmula sin cuantificadores lógicos , designada como «matriz» . Toda fórmula es equivalente en lógica clásica a una fórmula en forma normal prenexa . Por ejemplo , si , y son fórmulas sin cuantificar con las variables libres mostradas , luego está en forma normal prenexa , con la matriz , mientras que es lógicamente equivalente pero no en forma prenexa . El término «prenexa» viene del latín praenexus , pasado participio de praenectere , que significa «atado» o «atado en el frente» . Cuando una fórmula en forma normal prenexa solo posee cuantificadores universales , se dice que está en forma normal de Skolem . Toda fórmula en forma normal prenexa es lógicamente equivalente a una en forma normal de Skolem , y la manera de llegar de una a otra se denomina skolemización . Conversión a forma prenexa Toda fórmula de primer orden es lógicamente equivalente a alguna fórmula en forma prenexa . Hay algunas reglas de conversión que pueden ser aplicadas recursivamente para convertir una fórmula a forma prenexa . Las reglas dependen de qué conectiva lógica ( o conectivas ) y cuantificador ( o cuantificadores ) aparezcan en la fórmula . Conjunción y disyunción Las reglas para la conjunción y la disyunción dicen que es equivalente a , es equivalente a ; Y es equivalente a , es equivalente a \ . Las equivalencias son válidas cuando x no aparece como variable libre de ψ ; si x sí aparece libre en ψ , debe ser reemplazada por otra variable libre . Por ejemplo , en el lenguaje de los anillos , es equivalente a , pero no es equivalente a porque la fórmula en la izquierda es verdadera en cualquier anillo cuando la variable libre x es igual a mientras que la fórmula de la derecha no tiene variables libres , y es falsa en cualquier anillo no-trivial . 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 remueven los cuantificadores del antecedente y dos que remueven los cuantificadores del consecuente . Estas reglas pueden ser derivadas reescribiendo la implicación como y aplicando las reglas para la disyunción de arriba . Tal como las reglas de la disyunción , estas reglas requieren que la variable cuantificada en una subfórmula no aparezca libre en otra subfórmula . Las reglas para remover cuantificadores del antecedente son : es equivalente a , es equivalente a \ . Las reglas para remover cuantificadores del consecuente son : es equivalente a , es equivalente a \ . Ejemplo Supóngase que , , y son fórmulas sin cuantificar y no comparten variable libre alguna . Considérese la fórmula . Aplicando recursivamente las reglas empezando por las subfórmulas internas , la siguiente secuencia de fórmulas lógicamente equivalentes pueden obtener se : . Esta no es la única forma prenexa equivalente a la fórmula original . Por ejemplo , abordando el consecuente antes que el antecedente en el ejemplo , la forma prenexa Puede ser obtenida : . Lógica intuicionista Las reglas para convertir una fórmula a una en forma prenexa hace engorroso el manejo de la lógica clásica . En lógica intuicionista no sucede que toda fórmula es lógicamente equivalente a una fórmula prenexa . La negación de una conectiva es un obstáculo , pero no es el único . La implicación también recibe un tratamiento en lógica intuicionista que en la lógica clásica ; en lógica intuicionista , no es definible usando la negación y la disyunción . Uso de la forma prenexa Algunos sistemas lógicos solo pueden tratar con 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 reescritas en formal normal prenexa . Vea se también Herbrandization Forma normal de Skolem Jerarquía analítica Referencias Bibliografía Prenexa Lógica matemática