En metalógica, la completitud o completud semántica es la propiedad metateórica que tienen los sistemas formales cuando todas las fórmulas lógicamente válidas (todas las verdades lógicas) del sistema son además teoremas del sistema.^[1]​ Es decir, cuando el conjunto de las verdades lógicas del sistema es un subconjunto del conjunto de teoremas. En otras palabras, si A es una fórmula cualquiera del lenguaje y S es el sistema formal bajo consideración, entonces se cumple que:

Si  ${\displaystyle \models _{\mathrm {S} }A}$  entonces  ${\displaystyle \vdash _{\mathrm {S} }A}$^[1]​

Por otra parte, la completitud sintáctica es la propiedad que tienen los sistemas formales cuando, para toda fórmula cerrada del lenguaje del sistema, o bien es un teorema o bien su negación lo es. Esto es, existe una prueba para cada fórmula cerrada o para su negación.

La lógica proposicional y la lógica de primer orden son ambas semánticamente completas, pero no sintácticamente completas. Por ejemplo, en la lógica proposicional, la fórmula p no es un teorema, y tampoco lo es su negación, de modo que eso basta para mostrar que no es sintácticamente completa. No obstante, como ninguna de esas dos fórmulas es una verdad lógica, no afectan a la completitud semántica del sistema.

El segundo teorema de incompletitud de Gödel demuestra que ningún sistema (definido recursivamente) con cierto poder expresivo puede ser a la vez consistente y sintácticamente completo.

Otra propiedad metateórica distinta es la completitud semántica fuerte, que dice: si en un sistema formal S, A es una fórmula bien formada cualquiera que es una consecuencia semántica de un conjunto ${\displaystyle \Gamma }$ de fórmulas, entonces existe una derivación de A a partir de ${\displaystyle \Gamma }$. En símbolos:

Si  ${\displaystyle \Gamma \models _{\mathrm {S} }A}$  entonces  ${\displaystyle \Gamma \vdash _{\mathrm {S} }A}$^[2]​

• Metalógica
• Teorema de completitud de Gödel
• Teoremas de incompletitud de Gödel