Uit Wikipedia, de vrije encyclopedie
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
en
kwantorloze formules zijn met vrije variabelen, dan is
![{\displaystyle \forall x\ \exists y\ \exists z\ (\phi \lor (\psi \rightarrow \rho ))}](http://178.128.105.246/cars-https-wikimedia.org/api/rest_v1/media/math/render/svg/45064703ccdab960673bdc4e12ae3410ca716a26)
in prenex-normaalvorm met matrix
, terwijl
![{\displaystyle \forall x\ ((\exists y\ \phi )\lor ((\forall z\ \psi )\rightarrow \rho ))}](http://178.128.105.246/cars-https-wikimedia.org/api/rest_v1/media/math/render/svg/7e0e8dfa3dbb35e0149ae246faa7276f918faf08)
hiermee logisch equivalent is, maar niet in prenex-normaalvorm.
Het is mogelijk een willekeurige formule
naar een logisch equivalente formule in prenex-normaalvorm om te schrijven. Daarvoor moeten we er eerst voor zorgen dat elke variabele in
slechts één keer voorkomt, en dat er geen variabelen zijn die zowel gebonden als vrij in
voorkomen. Dit kunnen we altijd doen door gebonden variabelen te hernoemen. Daarna kunnen we stapsgewijs
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Gegeven de formule
. We kunnen deze formule as volgt in prenex-normaalvorm omschrijven:
- Herbenoemen van variabelen:
![{\displaystyle \exists zP(z)\land \forall x{\bigl (}\exists yR(x,y)\to Q(x){\bigr )}}](http://178.128.105.246/cars-https-wikimedia.org/api/rest_v1/media/math/render/svg/8f87318426e9268df350c60d4736bbab798c33b6)
![{\displaystyle \exists zP(z)\land \forall x\forall y{\bigl (}R(x,y)\to Q(x){\bigr )}}](http://178.128.105.246/cars-https-wikimedia.org/api/rest_v1/media/math/render/svg/5a91ddaa42a4a6c56163257fe0bf4b4784a96d88)
![{\displaystyle \exists z\forall x\forall y{\bigl (}P(z)\land {\bigl (}R(x,y)\to Q(x){\bigr )}{\bigr )}}](http://178.128.105.246/cars-https-wikimedia.org/api/rest_v1/media/math/render/svg/9a09e06bff16c68e959d01b294cb97d060f256c9)