Un métathéorème qui garantit que toute formule démontrable dans un système déductif formel donné est aussi sémantiquement valide dans la classe de modèles visée ; la dérivabilité syntaxique implique la vérité au sens des modèles.

Principe

Les preuves préservent la vérité : si une phrase est dérivable selon les règles de preuve du système, alors elle est vraie dans chaque modèle correspondant à la sémantique choisie.

Démonstration

En logique propositionnelle, on montre que si ⊢ φ (φ est démontrable), alors ⊨ φ (φ est vraie pour toute affectation de valeurs de vérité), en vérifiant que les axiomes sont valides et que les règles d'inférence préservent la validité.

Mauvaise application

Prétendre que le théorème vaut pour un système dont les règles permettent des étapes invalides (par exemple une règle qui dérive des formules arbitraires) ou confondre correction et complétude.

Conséquence

Confiance dans les preuves : une théorème démontré ne peut pas être sémantiquement faux par rapport à la sémantique visée, ce qui permet d'utiliser la recherche de preuves syntaxiques pour établir des vérités sémantiques.

Inversion

La complétude inverse la relation en affirmant que l'implication sémantique entraîne la démontrabilité syntaxique (là où la complétude est valide).

Limite

S'applique seulement relativement à un système de preuve et à une sémantique spécifiés ; la correction peut échouer si on change les règles, les axiomes ou les modèles visés ; elle n'affirme pas quelles vérités sont démontrables.

Tension sémantique

Tension avec la complétude et avec les notions informelles de vérité : la correction sécurise une direction (dérivation→validité) mais laisse ouverte la question de savoir si toutes les validités sont dérivables.

Synthèse

La correction est la garantie formelle que la machinerie déductive ne produit pas de faussetés sémantiques : elle relie dérivations syntaxiques et validité sémantique pour un système et une interprétation donnés, tandis que la dépendance aux règles et modèles délimite son champ.