Théorème de compacité

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

En logique mathématique, 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.

Le théorème de compacité du calcul propositionnel est le résultat analogue dans ce cadre plus restreint.


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 à ce 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.

La démonstration qui suit est donné dans le cas dénombrable, c'est-à-dire que l'on montre

Si tout sous-ensemble fini d’un ensemble infini dénombrable de propositions est satisfaisable, alors l’ensemble complet est aussi satisfisable.

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 A un ensemble infini dénombrable de propositions et P(n) une suite infinie dénombrable des propositions de A.

Soit p(n) une suite infinie dénombrable de propositions atomiques avec lesquelles les propositions de A sont construites.

Considérons l’arbre construit de la façon suivante.

Il y a un seul nœud initial, vide, de niveau 0.
S’il y a modèle dans lequel p(1) et P(1) sont tous les deux vrais, alors p(1) est un nœud de niveau 1 rattaché à l’unique nœud de niveau 0.
S’il y a un modèle dans lequel (non p(1)) et P(1) sont tous deux vrais, alors (non p(1)) est aussi un nœud de niveau 1 rattaché à l’unique nœud de niveau 0.
Quand un nœud y est rattaché à un autre x, alors x précède y. Cette relation est transitive : si un nœud x précède y et que y précède z, alors x précède z.
À un nœud de niveau n, on rattache p(n+1) au niveau n+1 s’il y a un modèle dans lequel p(n+1), tous ses prédécesseurs, et tous les P(i) pour i de 1 à n+1 sont vrais.
À un nœud de niveau n, 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 P(i) pour i de 1 à n+1 sont vrais.

On engendre de cette façon un arbre. Comme tout sous-ensemble fini de propositions de A est non contradictoire, cet 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 P(i) sont vrais. Cela termine cette preuve du théorème de compacité.

Articles connexes[modifier | modifier le code]