Théorème de compacité
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
[modifier | modifier le code]En calcul propositionnel, une formule propositionnelle est dite satisfaisable si l'on peut assigner [à définir] des valeurs de vérité (vrai ou faux) 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. Le théorème de compacité s'énonce comme suit.
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
[modifier | modifier le code]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
[modifier | modifier le code]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 :
On montre que l'ensemble H, ordonné par l'inclusion, est inductif. Soit une chaine, c'est-à-dire un sous-ensemble de H totalement ordonné. L'ensemble défini comme l'union (croissante) des ensembles , est un majorant de la chaine. En effet, d'une part, H inclut chaque pour , ainsi il est "plus grand" que chaque . 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 est totalement ordonné, inclus dans un certain avec ; cela n'est pas possible car est finiment satisfaisable).
D'après le lemme de Zorn, H possède un élément maximal que l'on note . Cet ensemble possède la propriété d'être complet au sens où pour toute formule propositionnelle F, soit , soit . En effet, par l'absurde, en supposant le contraire, on déduit par maximalité de que les ensembles et ne sont pas finiment satisfaisables et qu'il existe des ensembles finis tels que et ne soient pas satisfaisables. Or est un sous-ensemble fini de , donc satisfaisable. On déduit l'existence d'un valuation telle que (en particulier, et ). Or, on a ou . Supposons par exemple que . Alors ce qui contredit le fait que ne soit pas satisfaisable.
On va maintenant construire une valuation qui satisfait , et donc qui satisfait A, car A est inclus dans . Comme est complet, pour toute variable propositionnelle , soit , ou alors (il faut noter que ces deux cas s'excluent mutuellement car est finiment satisfaisable). On pose alors dans le premier cas et dans le deuxième.
On montre à présent que satisfait . Soit et les variables propositionnelles apparaissant dans la formule F. On note le littéral associé à dans , c'est-à-dire que l'on pose si et sinon. On pose alors . est fini donc satisfaisable, il existe donc une valuation qui satisfait B. Or nécessairement, pour tout on a donc , ce qui conclut la démonstration.
Autre démonstration utilisant le théorème de Tykhonov
[modifier | modifier le code]Il existe une autre démonstration[2] utilisant le théorème de Tykhonov, qui a recours à l'axiome du choix.
Applications
[modifier | modifier le code]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
[modifier | modifier le code]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
[modifier | modifier le code]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 est un énoncé de ℒ, alors ou bien ou bien .
Pour chaque énoncé définissons et munissons 𝒯 de la topologie dont une base d'ouverts est l'ensemble des .
Puisque , cette base d'ouverts est stable par intersections finies ; un ensemble est donc ouvert si et seulement si il est réunion quelconque d'ensembles .
On remarque par ailleurs que le complémentaire de l'ouvert élémentaire est ; c'est un ouvert élémentaire. On peut donc aussi bien choisir les ensembles comme base d'ouverts de la même topologie ou encore, ce qui revient au même, choisir les comme base de fermés.
Théorème de compacité (version topologique) — 𝒯 est un espace topologique compact.
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.
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
[modifier | modifier le code]Ce principe[réf. nécessaire] énonce que si une formule est vraie dans tous les corps de caractéristique nulle alors il existe un entier k tel que la formule est vraie dans tous les corps de caractéristique supérieure ou égale à k. En effet, considérons l'ensemble de formules suivants :
, 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 ). 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
, 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 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 est vraie dans tous les corps de caractéristique supérieure ou égale à k.
Application : construction de modèles non standard
[modifier | modifier le code]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é
[modifier | modifier le code]Grâce au théorème de compacité, on peut démontrer qu'il n'existe pas de formule 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é :
; 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
[modifier | modifier le code]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
[modifier | modifier le code]Logiques classiques
[modifier | modifier le code]La logique du second ordre n'est pas compacte[4].
Logiques modales
[modifier | modifier le code]Les logiques modales complètes selon une axiomatisation avec des formules de Sahlqvist sont fortement complètes : c'est-à-dire, est conséquence sémantique de T si et seulement si 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 est valide si, et seulement si, est démontrable.
Notes et références
[modifier | modifier le code]- (en) Fred Krger et Stephan Merz, Temporal Logic and State Systems (Texts in Theoretical Computer Science. An EATCS Series), Berlin, Springer Publishing Company, Incorporated, , 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, , 349 p. (ISBN 0-19-853375-6), p. 330 point (v) ⇒ (vi)
- (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, (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 », (lire en ligne), p. 110–143.
- (en) Rohit Parikh, The completeness of propositional dynamic logic, Springer Berlin Heidelberg, coll. « Lecture Notes in Computer Science », (ISBN 978-3-540-08921-6 et 9783540357575, lire en ligne), p. 403–415.