Pränexform

Eine Formel F in der Prädikatenlogik erster Stufe befindet sich in Pränexform, wenn alle Quantoren außen stehen. Enthält die Pränexform zusätzlich nur Konjunktion, Disjunktion und Negation (unmittelbar vor Atomen) als Junktoren, so wird sie auch als verneinungstechnische Normalform bezeichnet.

Eine Formel F der Prädikatenlogik befindet sich in Pränexform, wenn Sie von der Form

Q1y1Q2y2...QnykF

ist, mit

k\ge0 und
Q_1,...,Q_k\in \left\{ \forall, \exists \right\}.

In F darf kein Quantor vorkommen.

Q1y1Q2y2...Qnyk heißt Präfix, F ist die Matrix.

Siehe auch:

Beispiel: Bildung einer Pränexform

aus: \forall x P(x)\and \forall y Q(y) \and \forall z R(z,y)

wird: \forall x \forall y \forall z P(x)\and Q(y)\and R(z,y)

See also: Pränexform, Disjunktion, Formel, Junktor, Konjunktion, Matrix, Negation, Normalform, Prädikatenlogik, Präfix