Prenex forma normal

---

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 vinculadas , denominada prefijo , seguida de una parte libre de cuantificadores, denominada matriz . ^[2]

Cada fórmula en lógica clásica es equivalente a una fórmula en forma normal prenex. Por ejemplo, si , y son fórmulas sin cuantificadores con las variables libres que se muestran, entonces${\ estilo de visualización \ phi (y)}$${\ estilo de visualización \ psi (z)}$${\ estilo de visualización \ rho (x)}$

está en forma prenex normal 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 recursivamente para convertir una fórmula a la forma normal prenex. Las reglas dependen de qué conectores lógicos aparecen en la fórmula.

Las equivalencias son válidas cuando no aparece como variable libre de ; si aparece libre en , se puede cambiar el nombre del límite 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. Entonces , 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)}$

---