ATLAS
Ouvrir dans l'atlas →ChapitreLogique du premier ordre
Théorème de complétude ⋆
Pour une signature finie ou dénombrable, la démonstration n'emploie aucune forme du choix : on énumère les énoncés au lieu de les choisir. Pour une signature quelconque, elle emploie un principe de maximalité, le lemme de Zorn pour l'inclusion, et le théorème équivaut, dans , au lemme de l'ultrafiltre (Lemme de l'ultrafiltre) (sous la forme « toute théorie cohérente a un modèle »).
Toute théorie cohérente a un modèle ; de façon équivalente, un énoncé vrai dans tous les modèles d'une théorie y est démontrable.
La démonstration est celle de Henkin. On ajoute au langage des constantes témoins, étage par étage, avec les axiomes sans perdre la cohérence ; on prolonge la théorie en une théorie cohérente qui contient chaque énoncé ou sa négation (lemme de Lindenbaum).
On construit le modèle dont les éléments sont les classes de termes clos pour l'égalité démontrable, et l'on vérifie, par récurrence sur les énoncés, qu'il satisfait exactement ceux de la théorie.
Ce théorème relie deux notions de natures différentes : l'une, syntaxique, porte sur des suites finies de symboles ; l'autre, sémantique, sur tous les modèles possibles, collection immense. Il ne dit pas que tout énoncé vrai est démontrable, ce que l'incomplétude contredit, mais que tout énoncé vrai dans tous les modèles de l'est.