TheoremProved

Gödel's completeness theorem

Statement

In first-order logic, a sentence $\varphi$ is derivable from a set of axioms $\Sigma$ (written $\Sigma\vdash\varphi$ ) if and only if $\varphi$ is true in every model of $\Sigma$ (written $\Sigma\models\varphi$ ): syntactic and semantic consequence coincide.

Why is it true?

Completeness says first-order proof systems lose nothing: anything that is true in every possible structure satisfying the axioms can actually be derived by a finite formal proof. It is the positive counterpart to the (later) incompleteness theorems, which concern what a fixed axiom system for arithmetic specifically can prove, not first-order provability in general.

Proof sketch

Show every consistent set of first-order sentences has a model (Henkin's construction): extend the language with new constants to witness every existential statement, extend the theory to a maximal consistent set using these witnesses, and build a term model directly from the resulting syntactic data. Completeness then follows: if $\Sigma\nvdash\varphi$ , then $\Sigma\cup\{\neg\varphi\}$ is consistent, hence has a model in which $\varphi$ fails, so $\Sigma\not\models\varphi$ .

Proved by

proved 1929Kurt Gödel

Topics that use this theorem

Predicate logic Gödel's incompleteness theorems

Related theorems

Gödel's first incompleteness theorem

Step-by-step proofs

No step-by-step proof yet for this theorem.

References

Kurt Gödel (1930). Die Vollständigkeit der Axiome des logischen Funktionenkalküls · DOI:10.1007/BF01696781
Herbert B. Enderton (2001). A Mathematical Introduction to Logic · DOI:10.1016/C2009-0-22107-6