Théorème de compacité

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
image illustrant la logique image illustrant les mathématiques
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 satisfiable (toutes les phrases ne peuvent être en vraies en même temps). Pourtant, toute partie finie est satisfiable. En d'autres termes, la logique temporelle linéaire n'est pas compacte[1].

Calcul propositionnel[modifier | modifier le code]

En calcul propositionnel, une proposition est dite satisfaisable s'il existe une valuation qui affecte des valeurs de vérité aux atomes constituant la proposition de façon que celle-ci prenne la valeur vrai. 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[modifier | modifier le code]

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 propositions et φ(0), φ(1), ... une suite infinie dénombrable de formules de T.

Soit p(0), p(1), ... une suite infinie dénombrable de propositions atomiques avec lesquelles les propositions 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 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 y 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é.

Autre démonstration utilisant le théorème de Tyckonov[modifier | modifier le code]

Il existe une démonstration alternative utilisant le théorème de Tykhonov.

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 ssi 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[2].

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

Application ː principe de Robinson[modifier | modifier le code]

Ce principe[réf. nécessaire] dit 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 satisfiables (car si 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 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-standards[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 satisfiable. Donc, l'ensemble total est satisfiable. 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 contredit 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[2].

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 la signature est fini ou au plus le cardinal de la signature. La démonstration du théorème de Löwenheim-Skolem ascendant utilise ce fait.

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

Les logiques modales où interviennent un plus petit point fixe ne sont pas compactes ː logique temporelle linéaire, logique propositionnelle dynamique (propositional dynamic logic)[4] (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]

  1. Fred Krger et Stephan Merz, Temporal Logic and State Systems (Texts in Theoretical Computer Science. An EATCS Series), Springer Publishing Company, Incorporated, (ISBN 3540674012 et 9783540674016, lire en ligne)
  2. a et b (en) « Cours sur le théorème de compacité de M. Vardi »
  3. 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
  4. (en) Rohit Parikh, The completeness of propositional dynamic logic, Springer Berlin Heidelberg, coll. « Lecture Notes in Computer Science », (ISBN 9783540089216 et 9783540357575, lire en ligne), p. 403–415

Articles connexes[modifier | modifier le code]