Théorème de compacité
vignette|420x420px|Si toute partie finie d'une théorie est satisfaisable (schématisée à gauche), alors la théorie est satisfaisable (schématisée à droite). 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 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. En calcul propositionnel, une formule propositionnelle est dite satisfaisable si l'on peut assigner 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. 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 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.
