En logique mathématique et métalogique, un système formel est dit complet par rapport à une propriété particulière si chaque formule possédant cette propriété peut être prouvée par une démonstration formelle à l'aide de ce système, c'est-à-dire par l'un de ses théorèmes ; autrement, le système est dit incomplet. Le terme « complet » est également utilisé sans qualification, avec des significations différentes selon le contexte, la plupart du temps se référant à la propriété de la validité sémantique. Intuitivement, dans ce sens particulier, un système est dit complet si toute formule vraie y est démontrable. Kurt Gödel, Leon Henkin et Emil Leon Poster ont tous publié des preuves de complétude. (Voir la thèse de Church-Turing.) La propriété réciproque de la complétude est appelée la correction, ou la cohérence : un système est correct par rapport à une propriété (principalement la validité sémantique) si chacun de ses théorèmes possède cette propriété. Un langage formel est expressivement complet s'il peut exprimer le but pour lequel il est destiné. Un ensemble de connecteurs logiques associés à un système formel est fonctionnellement complet si elle peut exprimer toutes les fonctions propositionnelles. La complétude sémantique est la réciproque de la correction des systèmes formels. Un système formel est dit correct pour une sémantique quand toute formule dérivable par les règles de ce système est vraie pour toutes les interprétations possibles dans la sémantique considérée. La propriété réciproque est appelée complétude (sémantique) du système formel, à savoir : si ⊨ φ, alors ⊢S φ. Par exemple, le théorème de complétude de Gödel établit la complétude sémantique pour la logique du premier ordre, mais il établit cette complétude également en un sens plus fort, décrit au paragraphe suivant. Un système formel S est fortement complet ou complet au sens fort, vis-à-vis d'une certaine sémantique, si pour tout ensemble de prémisses Γ (éventuellement infini), n'importe quelle formule φ qui se déduit sémantiquement de Γ (c'est-à-dire que tout modèle de Γ est modèle de φ) est dérivable à partir de formules de Γ dans le système formel considéré.