Brontekst bekijken van Prenex-normaalvorm

Een [[Vergelijking (wiskunde)|wiskundige formule]] uit de [[predicatenlogica]] is in de '''prenex-normaalvorm''' als ze geschreven is als een reeks [[Kwantor (logica)|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 <math>\phi(y),\ \psi(z)</math> en <math>\rho(x)</math> kwantorloze formules zijn met vrije variabelen, dan is 
: <math>\forall x \ \exists y \ \exists z \ (\phi \lor (\psi \rightarrow \rho))</math>
in prenex-normaalvorm met matrix <math>\phi \lor (\psi \rightarrow \rho)</math>, terwijl
: <math>\forall x \ ((\exists y \ \phi) \lor ((\forall z \ \psi ) \rightarrow \rho))</math>
hiermee logisch equivalent is, maar niet in prenex-normaalvorm.

== Conversie ==

Het is mogelijk een willekeurige formule <math>H</math> naar een logisch equivalente formule in prenex-normaalvorm om te schrijven. Daarvoor moeten we er eerst voor zorgen dat elke variabele in <math>H</math> slechts één keer in een kwantor voorkomt (gebonden wordt), en dat er geen variabelen zijn die zowel gebonden als vrij in <math>H</math> voorkomen. Dit kunnen we altijd doen door gebonden variabelen te hernoemen. Daarna kunnen we stapsgewijs <math>H</math> 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: 

{| class="wikitable centre"
! width="150px" | Formule 
! width="150px" | Prenex-normaalvorm
|-
| <math>\lnot \forall x F</math> 
| <math>\exists x \lnot F</math>
|-
| <math>(\forall x F) \land G </math> 
| <math> \forall x (F \land G)</math>
|-
| <math>(\forall x F) \lor G </math> 
| <math> \forall x (F \lor G)</math>
|-
| <math>(\forall x F)\rightarrow G </math> 
| <math> \exists x(F \rightarrow G)</math>
|-
| <math>G \land (\forall x F) </math> 
| <math> \forall x (G \land F)</math>
|-
| <math>G \lor (\forall x F) </math> 
| <math> \forall x (G \lor F)</math>
|-
| <math>G \rightarrow (\forall x F) </math> 
| <math> \forall x (G \rightarrow F)</math>
|-
| <math>\lnot \exists x F </math> 
| <math> \forall x \lnot F</math>
|-
| <math>(\exists x F) \land G </math> 
| <math> \exists x (F \land G)</math>
|-
| <math>(\exists x F) \lor G </math> 
| <math> \exists x (F \lor G)</math>
|-
| <math>(\exists x F)\rightarrow G </math> 
| <math> \forall x(F \rightarrow G)</math>
|-
| <math>G \land (\exists x F) </math> 
| <math> \exists x (G \land F)</math>
|-
| <math>G \lor (\exists x F) </math> 
| <math> \exists x (G \lor F)</math>
|-
| <math>G \rightarrow (\exists x F) </math> 
| <math> \exists x (G \rightarrow F)</math>
|-
|}

== Voorbeeld ==
Gegeven de formule <math>H=\exists x P(x) \land \forall x\bigl(\exists y R(x,y) \to Q(x)\bigr)</math>. We kunnen deze formule as volgt in prenex-normaalvorm omschrijven:
# Herbenoemen van variabelen: <math>\exists z P(z) \land \forall x\bigl(\exists y R(x,y) \to Q(x)\bigr)</math>
# <math>\exists z P(z) \land \forall x\forall y\bigl(R(x,y) \to Q(x)\bigr)</math>
# <math>\exists z\forall x\forall y \bigl( P(z) \land \bigl(R(x,y) \to Q(x)\bigr) \bigr)</math>

[[Categorie:Logica]]