Eine syntaktische Normalisierung von Aussagen der Prädikatenlogik erster Ordnung, bei der alle Quantoren nach vorne gezogen werden, sodass eine äquivalente Formel mit einem Quantorenpräfix und einer quantorenfreien Matrix entsteht.

Prinzip

Trenne die Bindungsstruktur (Quantoren) vom propositionalen Kern durch Umordnen und Umbenennen von Variablen, sodass alle Quantoren ein zusammenhängendes Präfix bilden und die gewünschte Erhaltungseigenschaft (Äquivalenz oder Erfüllbarkeit) erhalten bleibt.

Demonstration

Aus ∀x (P(x) → ∃y Q(y,x)) wird durch Umbenennung und Verschiebung der Quantoren ∀x ∃y (¬P(x) ∨ Q(y,x)), bzw. nach Skolemisation für Erfüllbarkeitsfragen ∀x (¬P(x) ∨ Q(f(x),x)). Dies zeigt das Hervorziehen der Quantoren und die quantorenfreie Matrix.

Fehlanwendung

Quantoren blind zu verschieben, ohne Variable-Capture, Änderungen der Gültigkeitsbereiche oder den Unterschied zwischen Äquivalenzerhalt und nur Erfüllbarkeitserhalt zu berücksichtigen. Beispielsweise kann das Entfernen von Abhängigkeiten bei der Skolemisation existenzielle Abhängigkeiten verfälschen.

Konsequenz

In Prenex-Form gebrachte Formeln erleichtern Vergleich, Resolution und viele metatheoretische Verfahren (z. B. die Klassifikation nach Quantorenpräfix), kosten aber die Verdeutlichung lokaler Bereiche und erfordern ggf. Skolemisation, wenn man Erfüllbarkeit erhalten will.

Umkehrung

Die Umkehrung besteht darin, die ursprünglichen Variablenbereiche wiederherzustellen und Quantoren in die Matrix zurückzuschieben, um lokale Abhängigkeiten sichtbar zu machen; die Prenex-Form nivelliert diese Information.

Abgrenzung

Gilt für die klassische Prädikatenlogik erster Ordnung und verwandte Logiken; erhält nicht zwangsläufig Wahrheit in nichtklassischen Logiken ohne Vorsicht, und Skolemisation entfernt Existenzquantoren nur im Sinne der Erfüllbarkeit, nicht zwingend der strengeren Äquivalenz.

Semantische Spannung

Spannung zwischen syntaktischer Einheitlichkeit (alle Quantoren vorn) und semantischer Lokalität (Quantoren, deren Bedeutung von benachbarten Junktoren abhängt) sowie zwischen Erhaltung von Äquivalenz und nur Erhalt der Erfüllbarkeit.

Synthese

Die Prenex-Normalform ist eine syntaktische Normierung, die Quantorenstruktur in ein Präfix extrahiert, um mechanisches Schließen und Klassifikation zu erleichtern, dabei aber lokale Gültigkeitsbereiche verdeckt; sie erfordert Aufmerksamkeit gegenüber Variablenabhängigkeiten und dem Ziel (Äquivalenz vs. Erfüllbarkeit).