Teorema de Completitud

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