Eine formale Schlussregel der Prädikatenlogik, die es erlaubt, eine universelle Formel ∀x φ(x) abzuleiten, wenn φ(x) unter der Bedingung bewiesen wurde, dass x beliebig ist und nicht von Annahmen über dieses einzelne Element abhängt.

Prinzip

Wenn eine Formel für ein beliebig gewähltes Element gilt — dessen Bezeichner in keinen ungeklärten Annahmen auftaucht — dann gilt sie für alle Elemente; die beliebige Instanz rechtfertigt die Einführung des Allquantors.

Demonstration

Angenommen, ohne Prämissen, die das Symbol a erwähnen, wurde P(a) ausschließlich aus Regeln bewiesen, die nichts Spezielles über a annehmen. Durch universelle Generalisierung kann man ∀x P(x) folgern. Beispiel: Aus einem Beweis, der a als beliebig behandelt und zeigt, dass a gerade ist, darf man nicht automatisch 'alle Zahlen sind gerade' schließen, sofern die Arbiträritätsbedingung fehlt.

Fehlanwendung

Die Regel anzuwenden, wenn das Zeigensymbol durch eine ungeklärte Annahme eingeführt oder von Prämissen abhängig ist (z. B. P(a) aus 'a = 0' ableiten und dann ∀x P(x) folgern) führt zu einer unzulässigen Verallgemeinerung.

Konsequenz

Korrekt angewendet erlaubt sie die Abstraktion von einem repräsentativen Fall zu einem allgemeinen Gesetz und ermöglicht die Bildung universeller Theoreme und Quantoreinführungen im Beweis.

Umkehrung

Die Umkehrung ist die universelle Instanziierung: Aus ∀x φ(x) folgt φ(t) für ein konkretes Term t. Generalisierung und Instanziierung verbinden die allgemeine und die spezielle Richtung der Quantifizierung.

Abgrenzung

Erfordert, dass die Variable (oder die Zeigerkonstante) nicht von ungeklärten Annahmen abhängt und nicht in Prämissen vorkommt, die sie einschränken. In bestimmten modalen, konstruktiven oder typisierten Systemen gelten zusätzliche Einschränkungen.

Semantische Spannung

Spannung zwischen der syntaktischen Regel zur Einführung von ∀ im Beweis und der semantischen Auffassung von 'für alle Elemente in einem Modell wahr' — eine syntaktische Verallgemeinerung kann durch Beweisregeln untersagt sein, auch wenn semantische Gültigkeit vorliegt.

Synthese

Universelle Generalisierung ist die Regel, die eine Herleitung über ein beliebiges, unabhängiges Repräsentantenelement in eine universelle Aussage überführt, unter Einhaltung von Frische- und Unabhängigkeitsbedingungen.