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».
son fórmulas sin cuantificar con las variables libres mostradas, luego está en forma normal prenexa, con la matriz
El término «prenexa» viene del latín praenexus, pasado participio de praenectere, que significa «atado» o «atado en el frente».
Hay algunas reglas de conversión que pueden ser aplicadas recursivamente para convertir una fórmula a forma prenexa.
Por ejemplo, en el lenguaje de los anillos, pero 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.
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: Las reglas para remover cuantificadores del consecuente son: Supóngase que
son fórmulas sin cuantificar y no comparten variable libre alguna.
Por ejemplo, abordando el consecuente antes que el antecedente en el ejemplo, la forma prenexa Puede ser obtenida: Las reglas para convertir una fórmula a una en forma prenexa hace engorroso el manejo de la lógica clásica.
Algunos sistemas lógicos solo pueden tratar con una teoría cuyas fórmulas estén escritas en forma normal prenexa.