Théorème de compacité

Cet article est une ébauche concernant la logique et les mathématiques.

Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.

En logique mathématique, un théorème de compacité énonce que si toute partie finie d'une théorie est satisfaisable alors la théorie elle-même est satisfaisable. Il existe des logiques où il y a un théorème de compacité comme le calcul propositionnel ou la logique du premier ordre (on parle de logiques compactes). Il existe aussi des logiques sans théorème de compacité. Commençons l'article par un exemple informel où il n'y a pas de théorème de compacité en considérant la théorie suivante :

un jour, il ne pleuvra pas ; il pleut ; demain il pleut ; après-demain il pleut ; dans 3 jours il pleut ; dans 4 jours il pleut ;…

La théorie n'est pas satisfaisable (toutes les phrases ne peuvent être vraies en même temps). Pourtant, toute partie finie est satisfaisable. En d'autres termes, la logique temporelle linéaire n'est pas compacte^[1].

Calcul propositionnel

En calcul propositionnel, une formule propositionnelle est dite satisfaisable si l'on peut donner ^{[à définir]} des valeurs de vérité aux atomes constituant la formule de façon que celle-ci soit vrai. Par exemple, la formule "p et non q" est satisfaisable en mettant p à vrai et q à faux. Une telle assignation s'appelle une valuation. Par exemple, "p à vrai et q à faux" est une valuation. Ainsi, une formule est satisfaisable s'il existe une valuation qui la satisfait. Plus généralement une théorie propositionnelle est satisfaisable s'il existe une valuation qui satisfait chacune des formules de cette théorie.

Théorème — Soit T un ensemble de formules de la logique propositionnelle. Si tout sous-ensemble fini de T est satisfaisable, alors T est aussi satisfaisable.

Démonstration dans le cas dénombrable

La démonstration^{[réf. nécessaire]} 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é.

Démonstration dans le cas général

Cette démonstration^{[réf. nécessaire]} 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 :

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 $\{B_{i}\}_{i\in I}$ une chaine, c'est-à-dire un sous-ensemble de H totalement ordonné. L'ensemble $B':=\bigcup _{i\in I}B_{i}$ défini comme l'union (croissante) des ensembles $B_{i}$ , est un majorant de la chaine. En effet, d'une part, H inclut chaque $B_{i}$ pour $i\in I$ , ainsi il est "plus grand" que chaque $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 $\{B_{i}\}_{i\in I}$ est totalement ordonné, inclus dans un certain $B_{i_{0}}$ avec $i_{0}\in I$ ; cela n'est pas possible car $B_{i_{0}}$ est finiment satisfaisable).

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

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

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

Autre démonstration utilisant le théorème de Tykhonov

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 $\Omega :=\{0,1\}^{P}$ , muni de la topologie produit, est compact. Pour toute formule F, on définit l'ensemble $[[F]]$ des valuations sur P qui satisfont F. Formellement,

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

.

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

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

.

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

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

.

Autrement dit, A est satisfaisable.

Applications

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^{[réf. nécessaire]}. 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].

Logique du premier ordre

Le théorème de compacité de la logique du premier ordre énonce que si toute partie finie d'une théorie du premier ordre est satisfaisable, c'est-à-dire, possède un modèle, alors la théorie elle-même est satisfaisable. C'est l'un des outils de base de la théorie des modèles, qui permet de montrer l'existence de nouvelles structures, modèles d'une théorie satisfaisable donnée. C'est une conséquence immédiate du théorème de complétude de Gödel (à condition de l'avoir démontré pour une théorie quelconque, non nécessairement dénombrable en particulier). Il peut également se démontrer directement, sans faire référence à la notion de démonstration.

Point de vue topologique

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 $e$ est un énoncé de ℒ, alors ou bien $T\vdash e$ ou bien $T\vdash \neg e$ .
Pour chaque énoncé $e$ définissons ${\mathcal {O}}_{e}=\{T\in {\text{𝒯}}\mid T\vdash e\}$ et munissons 𝒯 de la topologie dont une base d'ouverts est l'ensemble des ${\mathcal {O}}_{e}$ . Puisque ${\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 $\Omega \subset {\text{𝒯}}$ est donc ouvert si et seulement si il est réunion quelconque d'ensembles ${\mathcal {O}}_{e}$ .
On remarque par ailleurs que le complémentaire de l'ouvert élémentaire ${\mathcal {O}}_{e}$ est ${\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 ${\text{𝒯}}\smallsetminus {\mathcal {O}}_{e}$ comme base d'ouverts de la même topologie ou encore, ce qui revient au même, choisir les ${\mathcal {O}}_{e}$ comme base de fermés.

Théorème de compacité (version topologique) — 𝒯 est un espace topologique compact.

Démonstration

𝒯 est séparé : en effet si $T,T'\in {\text{𝒯}}$ et $T\neq T'$ il existe un énoncé $e$ tel que $T\vdash e$ et $T'\nvdash e$ (par exemple). Puisque $T'$ est complète il faut que $T'\vdash \neg e$ ; ainsi a-t-on $T\in {\mathcal {O}}_{e}$ et $T'\in {\mathcal {O}}_{\neg e}$ , ces deux ouverts étant disjoints.
Pour prouver la quasi-compacité il suffit de montrer que tout ultrafiltre sur 𝒯 est convergent. Soit donc 𝒰 un ultrafiltre sur 𝒯.

Chaque $T\in {\text{𝒯}}$ admet un modèle $M_{T}$ par définition. Posons alors ${\mathfrak {M}}=\prod \nolimits _{T\in {\text{𝒯}}}M_{T}{\big /}{\text{𝒰}}$ (ultraproduit des $M_{T}$ selon 𝒰) et $T_{0}=\mathrm {Th} ({\mathfrak {M}})$ , c'est-à-dire l'ensemble des énoncés $e$ tels que ${\mathfrak {M}}\models e$ .
Un voisinage élémentaire de $T_{0}$ est de la forme ${\mathcal {O}}_{e}$ pour un certain énoncé $e$ tel que $T_{0}\vdash e$ . On a donc ${\mathfrak {M}}\models e$ . D'après le théorème de Łoś $\{T\in {\text{𝒯}}\mid M_{T}\models e\}\in {\text{𝒰}}$ . Or $\{T\in {\text{𝒯}}\mid M_{T}\models e\}=\{T\in {\text{𝒯}}\mid T\vdash e\}={\mathcal {O}}_{e}$ , de sorte que ${\mathcal {O}}_{e}\in {\text{𝒰}}$ . Il en résulte que 𝒰 est convergent, vers $T_{0}$ .

Corollaire (théorème de compacité, version logique) — Soit ℰ un ensemble d'énoncés. Si toute partie finie de ℰ admet un modèle alors ℰ admet aussi un modèle.

Démonstration

Considérons la famille $({\mathcal {O}}_{e})_{e\in {\text{ℰ}}}$ ; on a déjà observé que ces ensembles sont fermés. Chaque intersection ${\mathcal {O}}_{e_{1}}\cap \ldots \cap {\mathcal {O}}_{e_{n}}$ (où $\{e_{1},\ldots ,e_{n}\}\subset {\text{ℰ}},\ n\geqslant 1$ ) est non vide puisque, par hypothèse, $\{e_{1},\ldots ,e_{n}\}$ possède un modèle.
D'après la propriété de Borel-Lebesgue (version ensembles fermés) appliquée au compact 𝒯, on a donc $\bigcap \nolimits _{e\in {\text{ℰ}}}\!{\mathcal {O}}_{e}\neq \varnothing$ . Si $T_{0}$ est élément de cette dernière intersection alors $\forall e\in {\text{ℰ}}\quad T_{0}\vdash e$ , et tout modèle de $T_{0}$ est aussi un modèle de ℰ.

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 ».

Application : principe de Robinson

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

$\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 $\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

$\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 $\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 $\varphi$ est vraie dans tous les corps de caractéristique supérieure ou égale à k.

Application : construction de modèles non standard

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.

Application : expressivité

Grâce au théorème de compacité, on peut démontrer qu'il n'existe pas de formule $\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é :

$\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].

Application : théorème de Löwenheim-Skolem

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.

Autres logiques

Logiques classiques

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

Logiques modales

Les logiques modales complètes selon une axiomatisation avec des formules de Sahlqvist sont fortement complètes : c'est-à-dire, $\varphi$ est conséquence sémantique de T si et seulement si $\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 $\varphi$ est valide si, et seulement si, $\varphi$ est démontrable.

Notes et références

↑ (en) Fred Krger et Stephan Merz, Temporal Logic and State Systems (Texts in Theoretical Computer Science. An EATCS Series), Berlin, Springer Publishing Company, Incorporated, 1^er janvier 2008, 433 p. (ISBN 978-3-540-67401-6 et 3-540-67401-2, lire en ligne).
↑ (en) Truss, John K., Foundations of Mathematical Analysis., Oxford, Oxford University Press, 1997, 349 p. (ISBN 0-19-853375-6), p. 330 point (v) ⇒ (vi)
↑ ^{a et b} (en) « Cours sur le théorème de compacité de M. Vardi ».
↑ Herbert B. Enderton, The Stanford Encyclopedia of Philosophy, Metaphysics Research Lab, Stanford University, 2015 (lire en ligne)
↑ Henrik Sahlqvist, Completeness and Correspondence in the First and Second Order Semantics for Modal Logic*, Elsevier, coll. « Proceedings of the Third Scandinavian Logic Symposium », 1^er janvier 1975 (lire en ligne), p. 110–143.
↑ (en) Rohit Parikh, The completeness of propositional dynamic logic, Springer Berlin Heidelberg, coll. « Lecture Notes in Computer Science », 4 septembre 1978 (ISBN 978-3-540-08921-6 et 9783540357575, lire en ligne), p. 403–415.

Articles connexes

[1] (en) Fred Krger et Stephan Merz, Temporal Logic and State Systems (Texts in Theoretical Computer Science. An EATCS Series), Berlin, Springer Publishing Company, Incorporated, 1^er janvier 2008, 433 p. (ISBN 978-3-540-67401-6 et 3-540-67401-2, lire en ligne).

[2] (en) Truss, John K., Foundations of Mathematical Analysis., Oxford, Oxford University Press, 1997, 349 p. (ISBN 0-19-853375-6), p. 330 point (v) ⇒ (vi)

[:0-3] {a et b} (en) « Cours sur le théorème de compacité de M. Vardi ».

[4] Herbert B. Enderton, The Stanford Encyclopedia of Philosophy, Metaphysics Research Lab, Stanford University, 2015 (lire en ligne)

[5] Henrik Sahlqvist, Completeness and Correspondence in the First and Second Order Semantics for Modal Logic*, Elsevier, coll. « Proceedings of the Third Scandinavian Logic Symposium », 1^er janvier 1975 (lire en ligne), p. 110–143.

[6] (en) Rohit Parikh, The completeness of propositional dynamic logic, Springer Berlin Heidelberg, coll. « Lecture Notes in Computer Science », 4 septembre 1978 (ISBN 978-3-540-08921-6 et 9783540357575, lire en ligne), p. 403–415.

[1]

[2]

[3]

[4]

[5]

[6]