Prenex-normaalvorm

Een wiskundige formule uit de predicatenlogica is in de prenex-normaalvorm als ze geschreven is als een reeks kwantoren, gevolgd door een deel zonder kwantoren, de matrix genoemd. Deze normaalvorm schrijft dus voor hoe de kwantoren moeten worden geplaatst.

Iedere formule in de klassieke logica is logisch equivalent met een formule in prenex-normaalvorm. Bijvoorbeeld, als ${\displaystyle \phi (y),\ \psi (z)}$ en ${\displaystyle \rho (x)}$ kwantorloze formules zijn met vrije variabelen, dan is

${\displaystyle \forall x\ \exists y\ \exists z\ (\phi \lor (\psi \rightarrow \rho ))}$

in prenex-normaalvorm met matrix ${\displaystyle \phi \lor (\psi \rightarrow \rho )}$, terwijl

${\displaystyle \forall x\ ((\exists y\ \phi )\lor ((\forall z\ \psi )\rightarrow \rho ))}$

hiermee logisch equivalent is, maar niet in prenex-normaalvorm.