Théorème 1Logique du premier ordre

Théorème de correction

Énoncé

Si $T \vdash \varphi$ , alors $T \models \varphi$ : tout ce qui est démontrable est vrai dans tous les modèles.

Démonstration

Montrons, par récurrence sur la longueur d'une démonstration formelle, que chacune de ses formules est satisfaite par tout modèle $\mathcal M$ de $T$ , sous toute valuation $s$ .

Les éléments de $T$ sont des énoncés satisfaits par $\mathcal M$ . Les axiomes logiques sont valides : (1) parce que, si $v$ attribue à chaque lettre la valeur de vérité sous $s$ de la formule qui la remplace, l'instance est satisfaite sous $s$ si et seulement si $\bar v$ vaut $1$ sur la tautologie, par récurrence sur celle-ci, les clauses de la satisfaction pour $\neg$ et $\to$ étant celles des tables de vérité ; (2) par le lemme de substitution ; (3) directement ; (4) par le lemme de coïncidence, puisque $x$ n'est pas libre dans $\alpha$ ; (5) directement.

Une généralisation d'une formule satisfaite sous toute valuation l'est aussi. Enfin, si $\alpha$ et $\alpha \to \beta$ sont satisfaites sous $s$ , alors $\beta$ l'est, par la définition de la satisfaction pour $\to$ .

□

Remarque

En particulier, une théorie qui a un modèle est cohérente : sinon elle démontrerait $\varphi$ et $\neg\varphi$ , qui seraient toutes deux vraies dans ce modèle. C'est la méthode la plus directe pour prouver la cohérence d'une théorie, et elle déplace la question vers la cohérence de la théorie où l'on construit le modèle. Il existe aussi des preuves syntaxiques de cohérence, comme celle de Gentzen (1936) pour l'arithmétique de Peano, qui raisonne sur les démonstrations elles-mêmes.

Repose sur

Modèles, conséquence Démonstrations formelles Substitution et lemme de substitution

Sert à

Théorème de complétude