title: Prenex-normaalvorm
text: 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 
   
  in prenex-normaalvorm met matrix , terwijl
   
  hiermee logisch equivalent is, maar niet in prenex-normaalvorm.
  
  Conversie 
  
  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:
  
  Voorbeeld 
  Gegeven de formule . We kunnen deze formule as volgt in prenex-normaalvorm omschrijven:
   Herbenoemen van variabelen: 
   
   
  
  Logica