Théorème de compacité

Il s'agit d'énoncer et de prouver le théorème de compacité du calcul des propositions. Ce théorème a un rôle très important pour la logique du premier ordre, notamment pour la preuve du théorème de complétude de Gödel. Sa preuve est basée sur le lemme de König, tout arbre infini à branchement fini a une branche infinie.

On dit qu'une proposition (c’est-à-dire une formule sans quantificateurs) est satisfiable s'il existe un modèle dans lequel la formule est vérifiée. Autrement dit, il est possible de donner des valeurs de vérité aux atomes constituant la proposition de façon à ce que celle-ci prenne la valeur vraie. On dit qu'un ensemble de formules est non contradictoire s'il existe un modèle où toutes les formules de cet ensemble sont simultanément satisfaites.

Le théorème de compacité s'énonce comme suit :

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

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.

A 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édecesseurs, et tous les P(i) pour i de 1 à n+1 sont vrais.

A 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édecesseurs, 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é.