Un métathéorème, classiquement pour la logique du premier ordre, qui affirme que si une formule est sémantiquement impliquée par un ensemble d'énoncés alors elle est démontrable syntaxiquement à partir de ces énoncés ; la conséquence sémantique implique la dérivabilité syntaxique (Σ ⊨ φ implique Σ ⊢ φ).

Principe

Toutes les conséquences sémantiques sont capturables par le système de preuve : pour les logiques où il vaut, l'implication modèle-théorique coïncide avec la démontrabilité.

Démonstration

La preuve de complétude de Gödel pour la logique du premier ordre construit un ensemble maximaux consistant ou utilise une extension de Henkin pour étendre une théorie consistante et construire un modèle où toute formule sémantiquement suivie est vraie, montrant ainsi Σ ⊨ φ implique Σ ⊢ φ.

Mauvaise application

Confondre ce théorème avec les théorèmes d'incomplétude de Gödel concernant les théories arithmétiques, ou supposer la complétude pour des logiques du second ordre ou des logiques à sémantiques non standard sans vérification.

Conséquence

Équivaut les méthodes proof-théoriques et modèle-théoriques pour la logique considérée, permettant de déduire des corollaires comme le théorème de compacité et les propriétés de Löwenheim–Skolem.

Inversion

La correction fournit la direction inverse (la démontrabilité implique la validité sémantique) ; ensemble, correction et complétude établissent l'équivalence entre syntaxe et sémantique.

Limite

Vaut pour la logique classique du premier ordre avec la sémantique standard et des systèmes de preuve appropriés ; elle peut échouer pour les logiques d'ordre supérieur, certaines logiques modales sous certaines sémantiques, ou pour des systèmes dépourvus de règles de preuve adéquates.

Tension sémantique

Tension avec l'expressivité et la décidabilité : la complétude peut coexister avec la perte de décidabilité ou avec l'incapacité à capturer des notions intensionales ; souvent mise en regard des résultats d'incomplétude en arithmétique.

Synthèse

La complétude comble le trou laissé par la correction en assurant que les énoncés sémantiquement vrais (par rapport à la sémantique spécifiée) peuvent être atteints par une preuve syntaxique dans la logique ciblée, tandis que son applicabilité dépend de la structure et de la sémantique de la logique.