Avant d’énoncer le théorème, il est essentiel de définir deux concepts centraux en logique du premier ordre. Soit $T$ un ensemble d’axiomes (une théorie) et $\varphi$ une formule (un énoncé).
- Conséquence Syntactique (Démontrabilité) : On dit que $\varphi$ est une conséquence syntaxique de $T$, noté $T \vdash \varphi$, s’il existe une démonstration formelle de $\varphi$ à partir des axiomes de $T$ et des règles de déduction logiques (comme le modus ponens). C’est une notion purement mécanique qui ne s’occupe que de la manipulation de symboles.
- Conséquence Sémantique (Validité) : On dit que $\varphi$ est une conséquence sémantique de $T$, noté $T \models \varphi$, si $\varphi$ est vraie dans tous les modèles où les axiomes de $T$ sont vrais. Un modèle est une structure mathématique (un univers, des fonctions, des relations) qui donne un sens, une interprétation, aux symboles. C’est une notion de vérité.
Pour toute théorie $T$ du premier ordre et toute formule $\varphi$, les notions de conséquence syntaxique et de conséquence sémantique coïncident. $$ T \vdash \varphi \iff T \models \varphi $$
Autrement dit, une formule est démontrable à partir d’un ensemble d’axiomes si et seulement si elle est vraie dans tous les mondes où ces axiomes sont vrais.
Une théorie $T$ est consistante (on ne peut pas y démontrer de contradiction, i.e., $T \not\vdash \bot$) si et seulement si elle admet un modèle (il existe une structure où ses axiomes sont vrais).
Démonstration (Esquisse de la preuve de Henkin)
La démonstration se fait en deux parties.
Partie 1 : Correction (Soundness) : $T \vdash \varphi \implies T \models \varphi$
Cette implication est la plus simple. Elle consiste à vérifier que les axiomes logiques sont valides (vrais dans tout modèle) et que les règles d’inférence (comme le modus ponens) préservent la vérité. Ainsi, si on part d’axiomes de $T$ qui sont vrais dans un modèle $M$, chaque étape de la démonstration formelle de $\varphi$ produira une nouvelle formule qui est également vraie dans $M$. Par conséquent, la conclusion $\varphi$ doit être vraie dans $M$. Comme cela vaut pour n’importe quel modèle $M$ de $T$, on a bien $T \models \varphi$.
Partie 2 : Complétude (Completeness) : $T \models \varphi \implies T \vdash \varphi$
C’est la partie la plus difficile. On démontre sa contraposée : si $\varphi$ n’est pas démontrable à partir de $T$ ($T \not\vdash \varphi$), alors $\varphi$ n’est pas une conséquence sémantique de $T$ ($T \not\models \varphi$).
L’hypothèse $T \not\vdash \varphi$ est équivalente à dire que la théorie $T’ = T \cup \{\neg\varphi\}$ est consistante. Pour montrer que $T \not\models \varphi$, il nous suffit de trouver un modèle de $T’$, car un tel modèle rendrait $T$ vraie et $\varphi$ fausse. La preuve consiste donc à montrer que toute théorie consistante admet un modèle.
- Extension de Henkin : On commence par enrichir le langage de la théorie $T’$ en y ajoutant une infinité de nouvelles constantes, appelées « constantes de Henkin ». On étend ensuite la théorie $T’$ en ajoutant, pour chaque formule $\psi(x)$ du langage enrichi, un axiome de la forme $(\exists x \, \psi(x)) \implies \psi(c)$, où $c$ est une nouvelle constante de Henkin. Ces axiomes garantissent que si la théorie peut prouver l’existence d’un objet, elle nomme également un « témoin » pour cet objet. On montre que cette nouvelle théorie, notée $T^*$, est toujours consistante.
- Complétion de Lindenbaum : On étend la théorie consistante $T^*$ en une théorie $T^{**}$ qui est maximale et consistante. Cela signifie que pour toute formule $\alpha$ du langage enrichi, soit $T^{**} \vdash \alpha$, soit $T^{**} \vdash \neg\alpha$. On construit cette extension en énumérant toutes les formules et en ajoutant à chaque étape soit la formule, soit sa négation, de manière à préserver la consistance.
-
Construction du modèle canonique : À partir de la théorie complète $T^{**}$, on construit un modèle $M$ « sur mesure ».
- L’univers de $M$ est l’ensemble des termes clos (sans variable) du langage enrichi.
- L’interprétation des symboles est définie syntaxiquement : une relation $R(t_1, \dots, t_n)$ est déclarée « vraie » dans $M$ si et seulement si la formule $R(t_1, \dots, t_n)$ est un théorème de $T^{**}$ (i.e., $T^{**} \vdash R(t_1, \dots, t_n)$).
- Lemme de vérité : On montre alors par induction sur la structure des formules que pour n’importe quelle formule $\alpha$, $\alpha$ est vraie dans le modèle $M$ si et seulement si $\alpha$ est un théorème de $T^{**}$. L’étape cruciale de l’induction, celle concernant le quantificateur existentiel $\exists$, est assurée par les axiomes de Henkin que nous avons ajoutés.
Conclusion : Puisque $T^{**}$ contient tous les axiomes de $T’$, et que pour toute formule $\alpha$ de $T^{**}$, on a $T^{**} \vdash \alpha$, le lemme de vérité nous assure que toutes les formules de $T’$ sont vraies dans le modèle $M$. Ainsi, $M$ est un modèle de $T’ = T \cup \{\neg\varphi\}$. L’existence de ce modèle prouve que $\varphi$ n’est pas une conséquence sémantique de $T$.