Lemme 4Théorème de complétude

Lemme de Lindenbaum ⋆

⋆ Axiome du choix

Le cas (ii) emploie le principe de maximalité de l'énoncé, forme de l'axiome du choix admise ici comme principe de la métathéorie : c'est le lemme de Zorn appliqué à un ensemble de parties ordonné par l'inclusion, que le nœud Lemme de Zorn démontrera équivalent, dans $\mathsf{ZF}$ , à l'axiome du choix. Le lemme de l'ultrafiltre (Lemme de l'ultrafiltre), strictement plus faible, suffirait. Le cas (i), qui couvre toutes les signatures finies ou dénombrables, n'emploie aucune forme du choix, et le point (iii), qui porte sur une théorie donnée, non plus.

Une théorie $T$ sur une signature $\mathcal L'$ est complète si, pour tout énoncé $\sigma$ de $\mathcal L'$ , on a $T \vdash \sigma$ ou $T \vdash \neg\sigma$ .

Énoncé

Soit $T$ une théorie cohérente sur une signature $\mathcal L'$ .

(i) Cas dénombrable. Si les énoncés de $\mathcal L'$ sont énumérés en une suite $\sigma_0, \sigma_1, \dots$ , la théorie $T$ est contenue dans une théorie cohérente $\widehat T$ sur $\mathcal L'$ qui contient, pour tout énoncé $\sigma$ , l'énoncé $\sigma$ ou l'énoncé $\neg\sigma$ ; $\widehat T$ est déterminée par l'énumération.

(ii) Cas général. La même conclusion vaut pour toute signature, si l'on admet le principe de maximalité suivant : si $\mathcal F$ est un ensemble non vide de parties d'un ensemble $E$ , et si la réunion de toute partie non vide de $\mathcal F$ formée d'éléments deux à deux comparables pour l'inclusion appartient à $\mathcal F$ , alors $\mathcal F$ a un élément maximal pour l'inclusion, c'est-à-dire strictement contenu dans aucun autre élément de $\mathcal F$ .

(iii) Une théorie cohérente $\widehat T$ qui contient, pour tout énoncé $\sigma$ , $\sigma$ ou $\neg\sigma$ est complète. De plus, pour tout énoncé $\sigma$ , $\widehat T \vdash \sigma$ si et seulement si $\sigma \in \widehat T$ , et exactement l'un des énoncés $\sigma$ et $\neg\sigma$ appartient à $\widehat T$ .

Démonstration

Observons d'abord que, si $T \vdash \sigma$ , la théorie $T \cup \{\sigma\}$ démontre les mêmes formules que $T$ : dans une démonstration formelle à partir de $T \cup \{\sigma\}$ , on remplace chaque emploi de l'hypothèse $\sigma$ par une démonstration de $\sigma$ à partir de $T$ . En particulier, $T \cup \{\sigma\}$ est cohérente si $T$ l'est.

(i) On définit par récurrence $T_0 = T$ , puis $T_{n+1} = T_n \cup \{\sigma_n\}$ si $T_n \vdash \sigma_n$ , et $T_{n+1} = T_n \cup \{\neg\sigma_n\}$ sinon. Si $T_n$ est cohérente, $T_{n+1}$ l'est aussi : dans le premier cas par l'observation qui précède, dans le second par le point (ii) de Cohérence.

Soit $\widehat T$ la réunion des $T_n$ . Si l'on avait $\widehat T \vdash \varphi$ et $\widehat T \vdash \neg\varphi$ , ces deux démonstrations n'emploieraient qu'un nombre fini d'éléments de $\widehat T$ , tous dans un même $T_n$ puisque les $T_n$ croissent, et $T_n$ serait incohérente. Enfin, tout énoncé est l'un des $\sigma_n$ , et $T_{n+1} \subset \widehat T$ contient $\sigma_n$ ou $\neg\sigma_n$ .

Les trois premières étapes, pour la signature formée de deux symboles de relation unaires

P

Q

et d'une constante

c

, la théorie

T = \{\forall x\, P\, x\}

et une énumération qui commence par

P\, c

Q\, c

\exists x\, \neg Q\, x

. À chaque étage, la branche rouge garde l'énoncé si la théorie déjà construite le démontre, et sa négation sinon (à droite, la raison :

T_0 \vdash P\,c

par l'axiome (2),

T_1 \nvdash Q\,c

parce qu'une structure à un élément où

Q

est vide est un modèle de

T_1

, et

T_2 \vdash \exists x\, \neg Q\, x

puisque

\neg Q\, c \in T_2

) ; la branche grise est écartée, et

\widehat T

est la réunion des théories de la branche rouge.

(ii) Soit $E$ l'ensemble des énoncés de $\mathcal L'$ , et $\mathcal F$ l'ensemble des théories cohérentes sur $\mathcal L'$ qui contiennent $T$ ; il est non vide, puisque $T \in \mathcal F$ . Soit $\mathcal C$ une partie non vide de $\mathcal F$ formée de théories deux à deux comparables pour l'inclusion, et $U$ leur réunion, qui contient $T$ .

Une démonstration formelle d'une formule et de sa négation à partir de $U$ n'emploierait qu'un nombre fini d'énoncés, chacun dans un élément de $\mathcal C$ . Parmi ces éléments, en nombre fini et deux à deux comparables, l'un contient tous les autres, comme on le voit par récurrence sur leur nombre ; il serait incohérent. Donc $U \in \mathcal F$ .

Le principe de maximalité fournit un élément maximal $\widehat T$ de $\mathcal F$ .

Soit $\sigma$ un énoncé. Si $\widehat T \vdash \sigma$ , la théorie $\widehat T \cup \{\sigma\}$ est cohérente, par l'observation initiale, donc appartient à $\mathcal F$ et, par maximalité, est égale à $\widehat T$ : $\sigma \in \widehat T$ .

Sinon, $\widehat T \cup \{\neg\sigma\}$ est cohérente par Cohérence, (ii), et de même $\neg\sigma \in \widehat T$ .

(iii) Si $\sigma \in \widehat T$ ou $\neg\sigma \in \widehat T$ , alors $\widehat T \vdash \sigma$ ou $\widehat T \vdash \neg\sigma$ : $\widehat T$ est complète. Si $\widehat T \vdash \sigma$ sans que $\sigma$ appartienne à $\widehat T$ , alors $\neg\sigma \in \widehat T$ , donc $\widehat T \vdash \neg\sigma$ , et $\widehat T$ serait incohérente. La même raison interdit à $\sigma$ et à $\neg\sigma$ d'appartenir tous deux à $\widehat T$ .

□

Remarque

La récurrence de (i) n'est pas un algorithme : savoir si $T_n \vdash \sigma_n$ n'est pas décidable en général (Church, 1936). Elle n'en est pas moins une définition légitime, qui n'emploie que le tiers exclu de la métathéorie : à chaque étape, l'une des deux possibilités a lieu, et la règle dit laquelle retenir. L'erreur la plus répandue est de confondre cette dichotomie avec un choix ; il n'y a rien à choisir, puisque l'énumération fixe l'ordre et que la règle fixe la décision.

Remarque

Le principe de maximalité de (ii) est le lemme de Zorn pour l'inclusion, que le graphe des ordinaux démontrera à partir de l'axiome du choix (Lemme de Zorn). Sans énumération des énoncés, il n'y a pas d'ordre dans lequel les examiner, et la récurrence de (i) n'a plus de sens.

Remarque

Le lemme porte le nom de Lindenbaum, qui ne l'a pas publié : c'est Tarski qui le lui attribue, dès 1930. Les théories complètes et cohérentes d'une signature forment l'espace dont la topologie donne son nom au théorème de compacité.

Repose sur

Cohérence

Sert à

Le modèle des termes clos