Eine Relation zwischen formalen Theorien, die dann gilt, wenn jede Theorie aus der anderen durch Hinzufügen expliziter Definitionen für neue Symbole gewonnen werden kann, sodass die beiden Theorien ohne Änderung der Inhalte der Sätze in den ursprünglichen Vokabularen ineinander übersetzbar sind.

Prinzip

Zwei Theorien sind definitional äquivalent, wenn es explizite, wahrheitserhaltende Definitionen gibt, die jedes nichtlogische Symbol der einen Theorie in die Sprache der anderen übersetzen und die Axiome wechselseitig zu Konsequenzen unter diesen Definitionen machen.

Demonstration

Betrachte eine prädikatenlogische Theorie T mit einem binären Symbol R und eine alternative Darstellung T', die R durch ein Symbol S ersetzt und ein definierendes Axiom S(x,y) ↔ φ_R(x,y) angibt, wobei φ_R eine Formel in der Sprache von T ist. Wenn umgekehrt R in T' durch eine Formel φ_S definierbar ist, sind T und T' definitional äquivalent; ihre Theoreme über das gemeinsame Vokabular stimmen nach Entfaltung der Definitionen überein.

Fehlanwendung

Die bloße gegenseitige Interpretierbarkeit oder die Tatsache, dieselben Modelle zu haben, als hinreichend für definitionale Äquivalenz zu halten. Gegenseitige Interpretierbarkeit ist oft schwächer und liefert nicht notwendigerweise explizite Eliminationsdefinitionen; daraus Äquivalenz abzuleiten ist ein häufiger Fehler.

Konsequenz

Sind Theorien definitional äquivalent, kann man eine Darstellung in Beweisen, Modellkonstruktionen und Anwendungen, die nur das gemeinsame Vokabular betreffen, ohne Weiteres durch die andere ersetzen; beide Präsentationen gelten als rein notationale Varianten derselben Theorie.

Umkehrung

Das Umgekehrte sind Theorien, die dieselben Sätze in einer gegebenen Sprache beweisen (konservative Übereinstimmung), aber zwischen denen keine expliziten Definitionen existieren, um neue Symbole zu eliminieren; solche Theorien sind trotz Übereinstimmung nicht definitional äquivalent.

Abgrenzung

Gilt für formale Theorien, bei denen explizite definitionsregeln (Einführung abkürzender Symbole mit exakten Definitionsformeln) erlaubt sind. Ausgeschlossen sind schwächere Relationen wie bloße Interpretierbarkeit, einige Formen der Morita-Äquivalenz oder semantische Äquivalenz ohne explizite Definitionsklauseln; vorausgesetzt wird eine akzeptierte Auffassung zulässiger Definitionen in der Hintergrundlogik.

Semantische Spannung

Konkurriert mit Begriffen wie Bi-Interpretierbarkeit und kategorialer Äquivalenz: Bi-Interpretierbarkeit gestattet wechselseitige Übersetzungen bis auf Isomorphie, während definitorische Äquivalenz explizite eliminierbare Definitionen fordert. Der Konflikt betrifft die Frage, ob syntaktische Eliminierbarkeit oder semantische Übersetzbarkeit das richtige Kriterium für 'Identität' ist.

Synthese

Definitionale Äquivalenz ist die syntaktische Aussage, dass zwei Theorien bis auf Einführung und Eliminierung definierter Symbole dieselbe Theorie sind: Explizite Definitionen verwandeln das eine Vokabular in das andere und machen jede Theorie zu einer notationalen Variante der anderen.