Un mappage mécaniquement spécifié des formules et des preuves d’un langage formel ou système de preuves vers les formules et preuves d’un autre, défini par règles sur la syntaxe (symboles, connecteurs, formation de termes) et destiné à préserver la dérivabilité syntaxique et les propriétés proof‑théoriques associées.

Principe

La traduction syntaxique se construit par récursion structurelle sur la syntaxe et par le mappage de règles d’inférence ou de constructions de preuve de sorte que les dérivations sources produisent des dérivations cibles ; elle est algorithmique, souvent compositionnelle, et vise à préserver la démontrabilité plutôt que la seule vérité sémantique.

Démonstration

La traduction négative de Gödel–Gentzen mappe des preuves classiques en preuves intuitionnistes par une transformation récursive syntaxique des formules et en fournissant une justification au niveau des règles montrant que les dérivations sources produisent des dérivations cibles, réalisant ainsi une inclusion de la démontrabilité classique dans la démontrabilité constructive pour une classe restreinte de formules.

Mauvaise application

Supposer qu’une traduction syntaxique préserve automatiquement la sémantique telle que la vérité modèle‑théorique, ou qu’elle préserve la complexité et la longueur des preuves ; ou encore appliquer une traduction syntaxique conçue pour une notion déductive à un système de preuve cible incompatible sans ajustement.

Conséquence

Une traduction syntaxique correcte donne la correction du transfert de preuve : si Γ ⊢_S φ alors mapped(Γ) ⊢_T mapped(φ). Cela facilite le transport mécanisé de preuves, des méta‑résultats de conservativité et des inclusions formelles d’un calcul dans un autre.

Inversion

Les traductions sémantiques (modèle‑théoriques) se concentrent sur la cartographie des modèles et des conditions de vérité plutôt que sur les preuves ; un plongement purement sémantique ne fournit pas nécessairement une traduction syntaxique qui convertisse les preuves sources en preuves cibles.

Limite

Exige des grammaires formelles et des systèmes de preuve explicites pour la source et la cible et une description effective de la traduction ; elle exclut le paraphrase informel, les encodages non effectifs ou les transformations ne préservant que la satisfiabilité ou la vérité individuelle sans produire des dérivations cibles.

Tension sémantique

Tension entre traductions syntaxiques et plongements sémantiques : une traduction fidèle syntaxiquement peut être sémantiquement opaque (modifier le comportement des modèles), et réciproquement un plongement sémantique peut ne pas induire une traduction syntaxique praticable des preuves.

Synthèse

Une traduction syntaxique est un mappage algorithmique et préservant la structure sur formules et dérivations qui transporte la démontrabilité d’un système formel à un autre ; c’est l’instrument proof‑théorique pour l’inclusion, les preuves de conservativité et la migration automatique de preuves.