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 $\varphi (y),\psi (z)$ en $\rho (x)$ kwantorloze formules zijn met vrije variabelen, dan is

$\mathrm{\forall }x\mathrm{\exists }y\mathrm{\exists }z(\varphi \vee (\psi \to \rho ))$

in prenex-normaalvorm met matrix $\varphi \vee (\psi \to \rho )$, terwijl

$\mathrm{\forall }x((\mathrm{\exists }y\varphi )\vee ((\mathrm{\forall }z\psi )\to \rho ))$

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

Conversie

Het is mogelijk een willekeurige formule $H$ naar een logisch equivalente formule in prenex-normaalvorm om te schrijven. Daarvoor moeten we er eerst voor zorgen dat elke variabele in $H$ slechts één keer in een kwantor voorkomt (gebonden wordt), en dat er geen variabelen zijn die zowel gebonden als vrij in $H$ voorkomen. Dit kunnen we altijd doen door gebonden variabelen te hernoemen. Daarna kunnen we stapsgewijs $H$ naar prenex-normaalvorm converteren door steeds subformules waarin een kwantor in een argument van een andere bewerking voorkomt volgens de volgende tabel om te schrijven:

Formule	Prenex-normaalvorm
$\mathrm{\neg }\mathrm{\forall }xF$	$\mathrm{\exists }x\mathrm{\neg }F$
$(\mathrm{\forall }xF)\wedge G$	$\mathrm{\forall }x(F\wedge G)$
$(\mathrm{\forall }xF)\vee G$	$\mathrm{\forall }x(F\vee G)$
$(\mathrm{\forall }xF)\to G$	$\mathrm{\exists }x(F\to G)$
$G\wedge (\mathrm{\forall }xF)$	$\mathrm{\forall }x(G\wedge F)$
$G\vee (\mathrm{\forall }xF)$	$\mathrm{\forall }x(G\vee F)$
$G\to (\mathrm{\forall }xF)$	$\mathrm{\forall }x(G\to F)$
$\mathrm{\neg }\mathrm{\exists }xF$	$\mathrm{\forall }x\mathrm{\neg }F$
$(\mathrm{\exists }xF)\wedge G$	$\mathrm{\exists }x(F\wedge G)$
$(\mathrm{\exists }xF)\vee G$	$\mathrm{\exists }x(F\vee G)$
$(\mathrm{\exists }xF)\to G$	$\mathrm{\forall }x(F\to G)$
$G\wedge (\mathrm{\exists }xF)$	$\mathrm{\exists }x(G\wedge F)$
$G\vee (\mathrm{\exists }xF)$	$\mathrm{\exists }x(G\vee F)$
$G\to (\mathrm{\exists }xF)$	$\mathrm{\exists }x(G\to F)$

Voorbeeld

Gegeven de formule $H=\mathrm{\exists }xP(x)\wedge \mathrm{\forall }x(\mathrm{\exists }yR(x,y)\to Q(x))$. We kunnen deze formule as volgt in prenex-normaalvorm omschrijven:

1. Herbenoemen van variabelen: $\mathrm{\exists }zP(z)\wedge \mathrm{\forall }x(\mathrm{\exists }yR(x,y)\to Q(x))$
2. $\mathrm{\exists }zP(z)\wedge \mathrm{\forall }x\mathrm{\forall }y(R(x,y)\to Q(x))$
3. $\mathrm{\exists }z\mathrm{\forall }x\mathrm{\forall }y(P(z)\wedge (R(x,y)\to Q(x)\left)\right)$