Théorème de Complétude

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 Σ ⊢ φ).