Théorie complète

En logique mathématique, une théorie complète est une théorie qui est équivalente à un ensemble maximal cohérent de propositions ; ceci signifie qu'elle est cohérente et que toute extension propre ne l'est plus. Pour des théories logiques qui contiennent la logique propositionnelle classique, ceci équivaut à la condition que pour toute proposition φ du langage de la théorie, soit elle contient φ, soit elle contient sa négation ¬φ.

Comme le montrent les théorèmes d'incomplétude de Gödel, les théories du premier ordre qui sont récursivement axiomatisables et qui sont assez riches pour exprimer l'arithmétique ne peuvent pas être complètes.

L'usage du mot complet dans théorie complète est à différencier de celui utilisé lorsque l'on dit qu'une logique est complète, ce qui exprime que tous les énoncés sémantiquement valides sont des théorèmes prouvables (un énoncé est « sémantiquement valide » s'il est vrai dans tous les modèles de la théorie). Le théorème de complétude de Gödel utilise cette notion de complétude.

Les théories complètes sont fermées pour un certain nombre de propriétés qui modélisent le schéma T (en) :

pour un ensemble $S$ , on a $A\land B\in S$ si et seulement si $A\in S$ et $B\in S$ ;
pour un ensemble $S$ , on a $A\lor B\in S$ si et seulement si $A\in S$ ou $B\in S$ .

Les ensembles complets maximaux constituent un outil fondamental dans la théorie des modèles de la logique classique et de la logique modale. Leur existence dans un cas particulier est en général une conséquence immédiate du lemme de Zorn et est basée sur l'idée qu'une contradiction implique d'un nombre fini de prémisses.
En logique modale, la collection des ensembles cohérents maximaux étendant une théorie T (fermée pour la règle d'inférence de nécessitation) peut être munie d'une structure de modèle de sémantique de Kripke de T, appelé le modèle canonique.