Prenex forma normal

---

Una fórmula del cálculo de predicados está en forma normal ( PNF ) prenex ^[1] 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 cuantificador libres con las variables libres que se muestran a continuación,${\ Displaystyle \ phi (y)}$${\ Displaystyle \ psi (z)}$${\ Displaystyle \ rho (x)}$

está en forma normal prenex con matriz , mientras que${\displaystyle \phi (y)\lor (\psi (z)\rightarrow \rho (x))}$

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.

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 (\exists x\phi )}$${\displaystyle (\exists x'\phi [x/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 y luego se pondrá en forma normal prenex .${\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)}$

---