Un mappage entre langages, formules ou structures tel que, chaque fois qu’une formule est vraie dans une interprétation ou un modèle source, son image par le mappage est vraie dans l’interprétation ou le modèle cible correspondant (par rapport à la sémantique spécifiée).

Principe

La préservation de la vérité exige que le mappage commute avec la satisfaction : pour tout modèle source M et toute formule φ, si M ⊨ φ alors mapped(M) ⊨ mapped(φ). La direction est importante — la vérité n’a à être préservée que de la source vers la cible sauf si le mappage est en outre vérité‑réfléchissant.

Démonstration

Un homomorphisme de structures relationnelles qui envoie éléments et relations de sorte que les formules atomiques satisfaites dans la source le soient aussi dans la cible fournit un mappage préservant la vérité pour la satisfaction atomique ; la traduction standard des formules modales en formules du premier ordre est préservante de la vérité pour les modèles de Kripke pointés de la façon attendue.

Mauvaise application

Considérer à tort qu’un mappage préservant la vérité est inversible ou qu’il préserve l’entaillement et la démontrabilité dans les deux sens ; ou supposer la préservation des degrés de vérité dans des logiques non classiques sans vérifier la sémantique utilisée.

Conséquence

La préservation de la vérité permet de transférer modèles, contre‑exemples et résultats de satisfaisabilité de la source vers la cible, d’établir des plongements sémantiques sûrs et de réutiliser des constructions de modèles dans le cadre cible.

Inversion

La notion réciproque est la vérité‑réflexion : un mappage est vérité‑réfléchissant si la vérité de l’image implique la vérité de la préimage. Un mappage à la fois préservant et réfléchissant la vérité instaure une équivalence de vérité entre source et cible.

Limite

Dépend de la sémantique : la vérité doit être définie dans la source et la cible et le mappage doit être spécifié sur formules et modèles ; la propriété n’implique pas automatiquement la préservation de traits proof‑théoriques ou de relations d’entaillement sauf si ceux‑ci sont inclus dans la spécification.

Tension sémantique

Tension entre préservation de la vérité et préservation des conséquences : un mappage peut préserver la vérité de formules isolées sans préserver la conséquence logique entre ensembles de formules, et il peut préserver la vérité sous une sémantique mais échouer sous une autre (classique vs. à valeurs multiples, par exemple).

Synthèse

Un mappage préservant la vérité est un plongement sémantique garantissant que la vérité dans la source se reporte dans la cible ; il constitue une garantie sémantique dirigée qui facilite le transfert de modèles mais doit être complété par d’autres propriétés pour obtenir une équivalence plus forte.