Completeness Theorem

A metatheorem, classically for first-order logic, stating that if a formula is semantically entailed by a set of sentences then it is syntactically provable from those sentences; semantic consequence implies syntactic derivability (Σ ⊨ φ implies Σ ⊢ φ).