Une transformation entre systèmes syntaxiques, ensembles de formules ou modèles qui préserve la conséquence logique : chaque fois qu’une formule découle d’un ensemble de prémisses dans la source (Γ ⊨ φ ou Γ ⊢ φ), les images de ces prémisses entraînent l’image de la conclusion dans la cible (mapped(Γ) ⊨ mapped(φ) ou mapped(Γ) ⊢ mapped(φ)).

Principe

La préservation des conséquences signifie que le mappage respecte la relation de conséquence d’intérêt (entaillement sémantique ou dérivabilité syntaxique). Elle exige typiquement que les preuves ou entaillements sémantiques dans la source puissent être traduits en preuves ou entaillements dans la cible, souvent par un mappage mécanique des règles et des formules.

Démonstration

Une traduction syntaxique qui mappe chaque règle d’inférence d’un système de preuve sur un schéma démontrable dans un autre système fournit un mappage préservant les conséquences ; par exemple, une inclusion d’un calcul de preuve dans un autre qui transforme les preuves sources en preuves cibles préserve la conséquence au sens syntaxique.

Mauvaise application

Supposer que la préservation des conséquences implique la préservation de la vérité pour des formules isolées, ou confondre la conservation de l’entaillement classique avec la préservation de relations de conséquence non monotones ou réfutables sans vérifier la notion de conséquence cible.

Conséquence

Les mappages préservant les conséquences permettent de transférer théorèmes, obligations de preuve et arguments de correction entre formalismes ; ils favorisent le raisonnement modulaire, la réutilisation des dérivations et l’établissement de résultats de conservativité ou d’inclusion entre systèmes.

Inversion

La notion réciproque est la réflexion des conséquences : si mapped(Γ) entraîne mapped(φ) implique Γ entraîne φ, alors le mappage réfléchit les conséquences et—si les deux propriétés tiennent—il instaure une équivalence de conséquence entre source et cible.

Limite

S’applique uniquement par rapport à la notion de conséquence spécifiée (sémantique vs syntaxique, monotone vs non monotone) ; il peut nécessiter d’ajuster le système de preuve cible ou d’enrichir les prémisses pour retrouver la complétude, et exclut les mappages qui préservent seulement la satisfiabilité ou la vérité de formules isolées mais pas l’entaillement entre ensembles.

Tension sémantique

Tension entre préservation des conséquences et contraintes proof‑théoriques : un mappage peut préserver l’entaillement tout en augmentant drastiquement la longueur ou la complexité des preuves, ou ne préserver l’entaillement qu’au prix d’un changement de sémantique de preuve (p. ex. classique vers constructif).

Synthèse

Un mappage préservant les conséquences est une traduction respectueuse de la structure qui transporte la conséquence logique d’une source vers une cible, permettant le transfert correct de la dérivabilité et de la théorématicité tout en exigeant une spécification claire de la notion de conséquence préservée.