Eine mechanisch spezifizierte Abbildung von Formeln und Beweisen einer formalen Sprache oder eines Beweissystems auf Formeln und Beweise eines anderen, definiert durch Regeln über Syntax (Symbole, Junktoren, Termbildung) und mit dem Ziel, syntaktische Herleitbarkeit und verwandte beweistheoretische Eigenschaften zu bewahren.

Prinzip

Syntaktische Übersetzung wird durch strukturelle Rekursion über die Syntax und durch Abbildung von Inferenzregeln oder Beweiskonstukten aufgebaut, so dass Ableitungen in der Quelle Ableitungen im Ziel erzeugen; sie ist algorithmisch, oft kompositionell, und zielt darauf ab, Beweisbarkeit zu erhalten statt nur semantische Wahrheit.

Demonstration

Die Gödel‑Gentzen’sche Negationsübersetzung überführt klassische Beweise in intuitionistische Beweise durch eine rekursive syntaktische Transformation von Formeln und durch Regel‑Level‑Begründung, dass Quellableitungen Zielableitungen erzeugen, womit klassische Beweisbarkeit in konstruktive Beweisbarkeit für eine eingeschränkte Formelklasse eingebettet wird.

Fehlanwendung

Zu glauben, eine syntaktische Übersetzung erhalte automatisch die Semantik wie modelltheoretische Wahrheit, oder anzunehmen, sie bewahre Komplexität und Beweislänge; ebenso die fehlerhafte Anwendung einer Übersetzung, die für eine bestimmte deduktive Notion entworfen wurde, auf ein inkompatibles Zielbeweissystem ohne Anpassung.

Konsequenz

Eine korrekte syntaktische Übersetzung sichert die Korrektheit des Beweistransfers: wenn Γ ⊢_S φ, dann mapped(Γ) ⊢_T mapped(φ). Das unterstützt mechanisierten Beweistransfer, Metasätze über Konservativität und formale Einbettungen eines Kalküls in einen anderen.

Umkehrung

Semantische (modelltheoretische) Übersetzungen legen den Schwerpunkt auf Abbildung von Modellen und Wahrheitsbedingungen statt auf Beweise; ein rein semantisches Embedding liefert nicht notwendigerweise eine syntaktische Übersetzung, die Quellbeweise in Zielbeweise überführt.

Abgrenzung

Erfordert explizite formale Grammatiken und Beweissysteme für Quelle und Ziel sowie eine effektive Beschreibung der Übersetzung; schließt informelle Umschreibungen, nicht‑effektive Kodierungen oder Transformationen aus, die lediglich Erfüllbarkeit oder Einzelwahrheit erhalten, ohne Zielableitungen zu produzieren.

Semantische Spannung

Spannung zwischen syntaktischen Übersetzungen und semantischen Einbettungen: Eine syntaktisch treue Übersetzung kann semantisch undurchsichtig sein (Modellverhalten verändern), und umgekehrt kann ein semantisches Embedding keine praktikable syntaktische Übersetzung der Beweise induzieren.

Synthese

Eine syntaktische Übersetzung ist eine algorithmische, strukturwahrende Abbildung auf Formeln und Herleitungen, die Beweisbarkeit von einem formalen System in ein anderes trägt; sie ist das beweistheoretische Instrument für Einbettungen, Konservativitätsbeweise und automatisierte Beweismigration.