Un metateorema, clásicamente para la lógica de primer orden, que afirma que si una fórmula es consecuencia semántica de un conjunto de frases entonces es demostrable sintácticamente a partir de ese conjunto; la consecuencia semántica implica la derivabilidad sintáctica (Σ ⊨ φ ⇒ Σ ⊢ φ).

Principio

Todas las consecuencias semánticas son capturables por el sistema de prueba: en las lógicas donde se cumple, la consecuencia modelo-teórica coincide con la demostrabilidad.

Demostración

La prueba de completitud de Gödel para la lógica de primer orden construye un conjunto maximamente consistente o emplea la Henkinización para extender una teoría consistente y construir un modelo en el que toda fórmula semánticamente seguida sea verdadera, mostrando así Σ ⊨ φ ⇒ Σ ⊢ φ.

Aplicación incorrecta

Confundir este teorema con los teoremas de incompletitud de Gödel sobre teorías aritméticas, o suponer que la completitud vale para lógicas de orden superior o para lógicas con semánticas no estándar sin verificación.

Consecuencia

Pone en equivalencia los métodos teoría-de-pruebas y teoría-de-modelos para la lógica considerada, permitiendo derivar corolarios como el teorema de compacidad y propiedades de Löwenheim–Skolem.

Inversión

La corrección da la dirección inversa (la demostrabilidad implica validez semántica); juntas, corrección y completitud establecen la equivalencia entre sintaxis y semántica.

Límite

Se cumple para la lógica clásica de primer orden con semántica estándar y sistemas de prueba adecuados; puede fallar para lógicas de orden superior, ciertas semánticas modales o sistemas sin reglas de prueba apropiadas.

Tensión semántica

Tensión con expresividad y decidibilidad: la completitud puede coexistir con la pérdida de decidibilidad o con la incapacidad para captar nociones intensionales; a menudo se contrasta con resultados de incompletitud en aritmética.

Síntesis

La completitud cierra la brecha dejada por la corrección al asegurar que las afirmaciones semánticamente verdaderas (respecto de la semántica especificada) pueden alcanzarse mediante pruebas sintácticas en la lógica objetivo, aunque su aplicabilidad depende de la estructura y semántica de la lógica.