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 :
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.
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é.