Pränexnormalform

Eine Formel ist in Pränexnormalform (PNF), wenn sie bereinigt ist und die Form hat:

wobei $Q_i\in \{\mathrm{\exists },\mathrm{\forall }\}$ Quantoren sind und $\psi$ (die Matrix) quantorenfrei ist.
Theorem: Jede FO-Formel ist äquivalent zu einer Formel in PNF.