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 :

Si toute partie finie d'une théorie est satisfaisable (schématisée à gauche), alors la théorie est satisfaisable (schématisée à droite).

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

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

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

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

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

Applications

modifier

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

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

Logique du premier ordre

modifier

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

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

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

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

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

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

Logiques classiques

modifier

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

Logiques modales

modifier

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
  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, , 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, , 349 p. (ISBN 0-19-853375-6), p. 330 point (v) ⇒ (vi)
  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, (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 », (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 », (ISBN 978-3-540-08921-6 et 9783540357575, lire en ligne), p. 403–415.

Articles connexes

modifier