Das Prinzip, dass man eine Teilformel durch eine andere Teilformel ersetzen darf, zu der sie logisch äquivalent ist (d. h. φ ↔ ψ), innerhalb einer größeren Formel, ohne den logischen Gesamtwert zu ändern, vorausgesetzt die kontextuellen Beschränkungen werden beachtet.

Prinzip

Wann immer zwei Formeln im gegebenen Kalkül beweisbar oder semantisch äquivalent sind, dürfen Vorkommen der einen einheitlich durch die andere in extensionellen Kontexten substituiert werden, wobei Wahrheit und Beweisbarkeit erhalten bleiben.

Demonstration

Wenn ¬¬p in der betrachteten Logik beweisbar äquivalent zu p ist, kann man in jeder größeren Formel eine Vorkommnis von ¬¬p durch p ersetzen (z. B. ¬¬p ∨ q in p ∨ q umwandeln), ohne die logische Konsequenz zu ändern.

Fehlanwendung

Das Ersetzen von Äquivalenten innerhalb intensionaler oder kontextabhängiger Operatoren (wie Glaube, Wissen, Modalität oder in Bereichen, die Bindungen verändern) wo Äquivalenz die Bedeutung nicht erhält, kann Argumente ungültig machen; ebenso ist das Substituieren von Formeln, die nur unter zusätzlichen Annahmen äquivalent sind, unsicher.

Konsequenz

Erleichtert Formelvereinfachung, Normalisierung und modulare Beweisführung durch erlaubte lokale Umformungen, die logische Eigenschaften bewahren, und ermöglicht die Übertragung von Hilfssätzen in Kontexten, in denen Extensionalität gilt.

Umkehrung

Die Umkehr besteht im Ersetzen nicht-äquivalenter Formeln oder im Durchführen von Umschreibungen in Kontexten, in denen Äquivalenz nicht die Austauschbarkeit garantiert; dies kann Wahrheitswerte und Ableitbarkeit verändern.

Abgrenzung

Anwendbar in extensionellen logischen Kontexten und in standardmäßigen Aussagen-/Prädikatenkalkülen; es versagt in intensionalen Logiken, vielen modalen Kontexten und an Stellen, wo Variablenfang oder Bereichsänderungen auftreten würden, sofern keine zusätzliche Rechtfertigung vorliegt.

Semantische Spannung

Es gibt eine Spannung zwischen syntaktischem Ersetzen (bloße Symbolmanipulation) und semantischer Äquivalenz: Zwei Formeln können extensionell äquivalent, dennoch aber in intensionalen Kontexten nicht austauschbar sein, was einen subtilen Wettstreit zwischen formaler Äquivalenz und kontextueller Bedeutung erzeugt.

Synthese

Substitution Gleichwertiger Ausdrücke: eine grundlegende Umschreibungsregel in extensionellen Logiken, die das Ersetzen beweisbar äquivalenter Teilformeln zur Vereinfachung oder Transformation von Formeln erlaubt, gültig nur dort, wo Extensionalität und Bindungsbedingungen Austauschbarkeit sicherstellen.