Théorème de complétude ⋆

(i) Soit $T$ une théorie cohérente sur $\mathcal L$, et $\mathcal L^+$, $H$ comme dans Extension par témoins. La théorie $T \cup H$ est cohérente sur $\mathcal L^+$. Le lemme de Lindenbaum la prolonge en une théorie cohérente $\widehat T$ sur $\mathcal L^+$ qui contient, pour tout énoncé, cet énoncé ou sa négation ; comme $\widehat T$ contient $H$, elle a la propriété des témoins.

Par le lemme de vérité, le modèle des termes clos $\mathcal M$ de $\widehat T$ satisfait tous les énoncés de $\widehat T$, en particulier ceux de $T$. C'est une structure pour $\mathcal L^+$ ; en oubliant l'interprétation des nouvelles constantes, on obtient une structure $\mathcal M_0$ pour $\mathcal L$, de même domaine.

La valeur d'un terme de $\mathcal L$ et la satisfaction d'une formule de $\mathcal L$ ne font intervenir que les interprétations des symboles de $\mathcal L$, comme on le voit par récurrence sur les termes, puis sur les formules ; $\mathcal M_0$ satisfait donc les mêmes énoncés de $\mathcal L$ que $\mathcal M$, et c'est un modèle de $T$.

(ii) Si $T \vdash \varphi$, alors $T \models \varphi$ par le théorème de correction. Réciproquement, si $T \nvdash \varphi$, la théorie $T \cup \{\neg\varphi\}$ est cohérente (Cohérence, (ii)), donc a un modèle par (i), qui est un modèle de $T$ ne satisfaisant pas $\varphi$ : ainsi $T \not\models \varphi$.

Les deux formes sont d'ailleurs équivalentes : on vient de déduire (ii) de (i), et, si (ii) est vrai, une théorie $T$ sans modèle vérifie $T \models \varphi \wedge \neg\varphi$ par vacuité, donc démontre $\varphi \wedge \neg\varphi$, puis $\varphi$ et $\neg\varphi$ par la règle des tautologies : elle est incohérente.