Théorème de compacité

La démonstration qui suit est donnée dans le cas où T est dénombrable (elle s'étend au cas général en utilisant le lemme de Zorn, plutôt que le lemme de König, ou l'axiome du choix dépendant). Soit T un ensemble infini dénombrable de formules propositionnelles et φ(0), φ(1)… une énumération des formules de T.

Soit p(0), p(1)… une suite infinie dénombrable de variables propositionnelles avec lesquelles les formules de T sont construites.

Construisons un arbre de la façon suivante.

La racine de l'arbre est de niveau 0 et :

• s’il y a un modèle dans lequel p(1) et φ(1) sont tous les deux vrais, alors p(1) est un fils de la racine ;
• s’il y a un modèle dans lequel (non p(1)) et φ(1) sont tous deux vrais, alors (non p(1)) est (aussi) un fils de la racine.

Plus généralement, à un nœud de niveau n :

• on rattache un nœud étiqueté par p(n+1) s’il y a un modèle dans lequel p(n+1), tous ses prédécesseurs, et tous les φ(i) pour i de 1 à n+1 sont vrais.
• on rattache (non p(n+1)) au niveau n+1 s’il y a un modèle dans lequel (non p(n+1)), tous ses prédécesseurs, et tous les φ(i) pour i de 1 à n+1 sont vrais.

Comme tout sous-ensemble fini de propositions de T est satisfaisable, l'arbre peut être indéfiniment poursuivi, il est donc infini, il a un nombre infini de nœuds. Comme chaque nœud ne peut avoir que deux successeurs au plus, il est à branchement fini. D’après le lemme de König, il a donc une branche infinie. Cette branche définit un modèle dans lequel tous les φ(i) sont vrais. Cela termine cette preuve du théorème de compacité.

Cette démonstration traite du cas général, c'est-à-dire lorsqu'on ne suppose pas d'hypothèses particulières sur l'ensemble des variables propositionnelles (en particulier, l'ensemble des variables propositionnelles n'est pas forcément dénombrable). On utilise alors le lemme de Zorn qui permet de fabriquer une valuation qui satisfait l'ensemble de formules.

Soit A un ensemble de formules finiment satisfaisable, c'est-à-dire tel que toute partie finie de A soit satisfaisable. On définit H comme l'ensemble des ensembles de formules propositionnelles, finiment satisfaisables qui contiennent A. Formellement :

${\displaystyle H:=\{B\mid A\subseteq B{\text{ et }}B{\text{ est finiment satisfaisable}}\}}$

On montre que l'ensemble H, ordonné par l'inclusion, est inductif. Soit ${\displaystyle \{B_{i}\}_{i\in I}}$ une chaine, c'est-à-dire un sous-ensemble de H totalement ordonné. L'ensemble ${\displaystyle B':=\bigcup _{i\in I}B_{i}}$ défini comme l'union (croissante) des ensembles ${\displaystyle B_{i}}$, est un majorant de la chaine. En effet, d'une part, H inclut chaque ${\displaystyle B_{i}}$ pour ${\displaystyle i\in I}$, ainsi il est "plus grand" que chaque ${\displaystyle B_{i}}$. D'autre part, il appartient à H car il contient A et est finiment satisfaisable (s'il ne l'était pas, il existerait un sous-ensemble fini insatisfaisable de formules inclus dans B', et donc, comme ${\displaystyle \{B_{i}\}_{i\in I}}$ est totalement ordonné, inclus dans un certain ${\displaystyle B_{i_{0}}}$avec ${\displaystyle i_{0}\in I}$ ; cela n'est pas possible car ${\displaystyle B_{i_{0}}}$est finiment satisfaisable).

D'après le lemme de Zorn, H possède un élément maximal que l'on note ${\displaystyle A_{0}}$. Cet ensemble possède la propriété d'être complet au sens où pour toute formule propositionnelle F, soit ${\displaystyle F\in A_{0}}$, soit ${\displaystyle \neg F\in A_{0}}$. En effet, par l'absurde, en supposant le contraire, on déduit par maximalité de ${\displaystyle A_{0}}$ que les ensembles ${\displaystyle A_{0}\cup \{F\}}$ et ${\displaystyle A_{0}\cup \{\neg F\}}$ ne sont pas finiment satisfaisables et qu'il existe des ensembles finis ${\displaystyle B_{1},B_{2}\subseteq A_{0}}$ tels que ${\displaystyle B_{1}\cup \{F\}}$ et ${\displaystyle B_{2}\cup \{\neg F\}}$ ne soient pas satisfaisables. Or ${\displaystyle B_{1}\cup B_{2}}$ est un sous-ensemble fini de ${\displaystyle A_{0}}$, donc satisfaisable. On déduit l'existence d'un valuation ${\displaystyle \nu }$ telle que ${\displaystyle \nu \vDash B_{1}\cup B_{2}}$ (en particulier, ${\displaystyle \nu \vDash B_{1}}$ et ${\displaystyle \nu \vDash B_{2}}$). Or, on a ${\displaystyle \nu \vDash F}$ ou ${\displaystyle \nu \vDash \neg F}$. Supposons par exemple que ${\displaystyle \nu \vDash F}$. Alors ${\displaystyle \nu \vDash B_{1},F}$ ce qui contredit le fait que ${\displaystyle B_{1}\cup F}$ ne soit pas satisfaisable.

On va maintenant construire une valuation ${\displaystyle \nu }$ qui satisfait ${\displaystyle A_{0}}$, et donc qui satisfait A, car A est inclus dans ${\displaystyle A_{0}}$. Comme ${\displaystyle A_{0}}$est complet, pour toute variable propositionnelle ${\displaystyle x}$, soit ${\displaystyle x\in A_{0}}$, ou alors ${\displaystyle \neg x\in A_{0}}$ (il faut noter que ces deux cas s'excluent mutuellement car ${\displaystyle A_{0}}$ est finiment satisfaisable). On pose alors ${\displaystyle \nu (x)=1}$ dans le premier cas et ${\displaystyle \nu (x)=0}$ dans le deuxième.

On montre à présent que ${\displaystyle \nu }$ satisfait ${\displaystyle A_{0}}$. Soit ${\displaystyle F\in A_{0}}$ et ${\displaystyle x_{1},\dots ,x_{n}}$ les variables propositionnelles apparaissant dans la formule F. On note ${\displaystyle \ell _{i}}$ le littéral associé à ${\displaystyle x_{i}}$ dans ${\displaystyle A_{0}}$, c'est-à-dire que l'on pose ${\displaystyle \ell _{i}=x_{i}}$ si ${\displaystyle x_{i}\in A_{0}}$ et ${\displaystyle \ell _{i}=\neg x_{i}}$ sinon. On pose alors ${\displaystyle B:=\{\ell _{1},\dots ,\ell _{n},F\}\subseteq A_{0}}$. ${\displaystyle B}$ est fini donc satisfaisable, il existe donc une valuation ${\displaystyle \nu '}$ qui satisfait B. Or nécessairement, pour tout ${\displaystyle i\leq n}$ on a ${\displaystyle \nu (x_{i})=\nu '(x_{i})}$ donc ${\displaystyle \nu (F)=\nu '(F)=1}$, ce qui conclut la démonstration.

Il existe une autre démonstration[2] utilisant le théorème de Tykhonov, qui a recours à l'axiome du choix.

Démonstration

Soit P l'ensemble des variables propositionnelles et A un ensemble de formules finiment satisfaisables sur P. D'après le théorème de Tykhonov, l'ensemble ${\displaystyle \Omega$ :=\{0,1\}^{P}} , muni de la topologie produit, est compact. Pour toute formule F, on définit l'ensemble ${\displaystyle [[F]]}$ des valuations sur P qui satisfont F. Formellement,

${\displaystyle [[F]]:=\{\nu \in \Omega ,\nu \vDash F\}}$.

Pour toute formule F, l'ensemble ${\displaystyle V_{F}}$ est un fermé de ${\displaystyle \Omega }$. Le fait que A soit finiment satisfaisable se traduit par : pour toute partie B finie de A,

${\displaystyle \bigcap _{F\in B}[[F]]\neq \emptyset }$.

Donc, d'après la propriété de Borel-Lebesgue (version contraposée traitant des complémentaires),

${\displaystyle \bigcap _{F\in A}[[F]]\neq \emptyset }$.

Autrement dit, A est satisfaisable.

Grâce au théorème de compacité de la logique propositionnelle, on peut démontrer que tout graphe est 3-coloriable si tout sous-graphe fini de celui-ci est 3-coloriable (théorème de De Bruijn-Erdős). Le théorème des quatre couleurs stipule que tout graphe planaire (fini) est 4-coloriable. Le théorème de compacité implique que tout graphe infini planaire est 4-coloriable. On peut aussi démontrer que le quart du plan est pavable avec un ensemble fini donné de tuiles de Wang si et seulement si tout carré fini est pavable avec ce même ensemble de tuiles. Le théorème de compacité permet aussi de démontrer que tout ordre partiel sur un ensemble infini peut s'étendre à un ordre total[3].

Étant donné un ensemble fini de type de tuiles de Wang, le plan est pavable si et seulement si tout carré fini est pavable.

Un graphe est 3-coloriable si et seulement si tout sous-graphe fini est 3-coloriable.

Si ℒ est un langage du premier ordre, considérons 𝒯 l'ensemble des théories complètes dans le langage ℒ, c'est-à-dire l'ensemble des théories T qui possèdent un modèle et qui sont maximales au sens suivant : si ${\displaystyle e}$ est un énoncé de ℒ, alors ou bien ${\displaystyle T\vdash e}$ ou bien ${\displaystyle T\vdash \neg e}$.
Pour chaque énoncé ${\displaystyle e}$ définissons ${\displaystyle {\mathcal {O}}_{e}=\{T\in {\text{𝒯}}\mid T\vdash e\}}$ et munissons 𝒯 de la topologie dont une base d'ouverts est l'ensemble des ${\displaystyle {\mathcal {O}}_{e}}$. Puisque ${\displaystyle {\mathcal {O}}_{e_{1}}\cap \ldots \cap {\mathcal {O}}_{e_{n}}={\mathcal {O}}_{e_{1}\land \ldots \land e_{n}}}$, cette base d'ouverts est stable par intersections finies ; un ensemble ${\displaystyle \Omega \subset {\text{𝒯}}}$ est donc ouvert si et seulement si il est réunion quelconque d'ensembles ${\displaystyle {\mathcal {O}}_{e}}$.
On remarque par ailleurs que le complémentaire de l'ouvert élémentaire ${\displaystyle {\mathcal {O}}_{e}}$ est ${\displaystyle {\text{𝒯}}\smallsetminus \{T\in {\text{𝒯}}\mid T\vdash e\}=\{T\in {\text{𝒯}}\mid T\vdash \neg e\}={\mathcal {O}}_{\neg e}}$ ; c'est un ouvert élémentaire. On peut donc aussi bien choisir les ensembles ${\displaystyle {\text{𝒯}}\smallsetminus {\mathcal {O}}_{e}}$ comme base d'ouverts de la même topologie ou encore, ce qui revient au même, choisir les ${\displaystyle {\mathcal {O}}_{e}}$ comme base de fermés.

Remarque. Les deux énoncés ci-desus sont en fait équivalents, la compacité de l'espace 𝒯 pouvant se démontrer à partir de la « version logique ».

Ce principe énonce que si une formule ${\displaystyle \varphi }$ est vraie dans tous les corps de caractéristique nulle alors il existe un entier k tel que la formule ${\displaystyle \varphi }$ est vraie dans tous les corps de caractéristique supérieure ou égale à k. En effet, considérons l'ensemble de formules suivants :

${\displaystyle \lnot \varphi }$, les axiomes de la théorie des corps, 1+1 ≠ 0, 1+1+1 ≠ 0, 1+1+1+1 ≠ 0, …

Il s'agit d'un ensemble de formules non satisfaisable (car si l'ensemble de formules avait un modèle, comme il doit satisfaire les formules 1+1 ≠ 0, 1+1+1 ≠ 0, 1+1+1+1 ≠ 0… il est de caractéristique nulle et donc satisferait ${\displaystyle \varphi }$). Ainsi par le théorème de compacité, il existe un sous-ensemble fini de formules non satisfaisable et l'on peut supposer sans perte de généralité que ce sous-ensemble fini est de la forme

${\displaystyle \lnot \varphi }$, les axiomes de la théorie des corps. 1+1 ≠ 0, 1+1+1 ≠ 0, …, 1+1+1+1 ≠ 0 (k-1 occurrences de 1 dans cette dernière formule)

Mais alors c'est exactement dire que ${\displaystyle \varphi }$ est conséquence sémantique de l'ensemble de formules

les axiomes de la théorie des corps. 1+1 ≠ 0, 1+1+1 ≠ 0, …, 1+1+1+1 ≠ 0

Ce qui se reformule en ${\displaystyle \varphi }$ est vraie dans tous les corps de caractéristique supérieure ou égale à k.

Considérons l'ensemble des formules vraies dans le graphe où les sommets sont les entiers où deux entiers n et n+1 sont reliés par une arête. Si on ajoute à cet ensemble des formules de la forme « il n'y a pas de chemin de a à b de longueur k », alors on obtient un ensemble dont tout sous-ensemble fini est satisfaisable. Donc, l'ensemble total est satisfaisable. Un modèle de cet ensemble s'appelle un modèle non standard.

Grâce au théorème de compacité, on peut démontrer qu'il n'existe pas de formule ${\displaystyle \varphi }$ du premier ordre qui exprime « il y a un nombre infini d'éléments ». En effet, par l'absurde, si tel était le cas, la théorie suivante contredirait le théorème de compacité :

${\displaystyle \lnot \varphi }$ ; il y a plus d'un élément ; il y a plus de deux éléments ; il y a plus de trois éléments ;…

De la même manière, la connexité d'un graphe, l'accessibilité dans un graphe ne sont pas exprimables en logique du premier ordre[3].

Le théorème de compacité peut se reformuler de manière plus précise : si toute partie finie d'une théorie du premier ordre est satisfaisable, alors la théorie possède un modèle dont le cardinal est au plus dénombrable si sa signature est finie ou au plus le cardinal de sa signature. La démonstration du théorème de Löwenheim-Skolem ascendant utilise ce fait.

La logique du second ordre n'est pas compacte[4].

Les logiques modales complètes selon une axiomatisation avec des formules de Sahlqvist sont fortement complètes : c'est-à-dire, ${\displaystyle \varphi }$ est conséquence sémantique de T si et seulement si ${\displaystyle \varphi }$ est démontrable depuis T. Elles sont donc compactes[5].

Les logiques modales où interviennent un plus petit point fixe ne sont pas compactes : logique temporelle linéaire, logique propositionnelle dynamique (propositional dynamic logic)[6] (l'argument est similaire à l'exemple donné dans l'introduction). En conséquence, elles ne peuvent avoir des axiomatisations fortement complètes : nous n'avons que ${\displaystyle \varphi }$ est valide si, et seulement si, ${\displaystyle \varphi }$ est démontrable.