Eine Schlussregel, die es erlaubt, aus einer universal quantifizierten Aussage eine konkrete Instanz abzuleiten: aus ∀x P(x) darf man P(t) für jeden Term t folgern, der geeignet anstelle von x eingesetzt werden kann.

Prinzip

Eine allgemein über alle Elemente einer Domäne gemachte Aussage berechtigt zur Substitution eines beliebigen, aber sachgemäßen Terms für die gebundene Variable und liefert eine spezifische Instanz, wobei die Wahrheit erhalten bleibt, wenn die Substitution variablenfangfrei erfolgt.

Demonstration

Aus dem Axiom ∀n ∈ N, n + 0 = n kann man instanziieren und erhält 5 + 0 = 5, indem man die Ziffer 5 für die gebundene Variable n einsetzt.

Fehlanwendung

Das Instanziieren mit einem Term, der nicht zur Domäne gehört, oder das Einsetzen eines Terms, der Variablenfang verursacht (z. B. Ersetzen einer gebundenen Variablen durch einen Ausdruck mit quantifizierter Variable) macht die Folgerung ungültig.

Konsequenz

Ermöglicht das Ableiten konkreter Konsequenzen aus allgemeinen Gesetzen und unterstützt den Übergang von allgemeinen Prämissen zu speziellen Schlussfolgerungen in Beweisen und Rechnungen.

Umkehrung

Die Umkehr ist die universelle Generalisierung, die versucht, aus Instanzen ∀x P(x) zu folgern; im Gegensatz zur Instanziierung erfordert die Generalisierung Sorgfalt, um sicherzustellen, dass die Instanz beliebig war und keine zusätzlichen Annahmen gemacht wurden.

Abgrenzung

Gilt in der Prädikatenlogik erster Stufe und verwandten Logiken, in denen Domänen und Substitutionen wohl definiert sind; berechtigt nicht zur Instanziierung über verschiedene Sorten hinweg oder in Kontexten, die Bindungsstrukturen ändern, und verlangt, dass der einsetzende Term frei für die Variable ist.

Semantische Spannung

Es besteht Spannung mit existenziellen Regeln: universelle Instanziierung liefert einzelne Instanzen, schafft jedoch keine Existenzbehauptungen; Instanziierung mit existenzieller Einführung zu verwechseln ist ein häufiger semantischer Fehler.

Synthese

Universelle Instanziierung: eine grundlegende und sichere Regel in standardmäßigen Prädikatenlogiken, die spezifische Instanzen aus universellen Aussagen erzeugt, vorausgesetzt Substitutionen respektieren Domäne, Sorten und Variablenfangfreiheit.