A topic in the Open Knowledge Graph — a free, open map of 15,290 topics and the order to learn them in.
Gödel's completeness theorem states that for first-order logic, semantic consequence and syntactic derivability coincide: Γ ⊨ φ if and only if Γ ⊢ φ. This is a fundamental metatheorem establishing the adequacy of formal proof systems for first-order logic. The completeness proof typically constructs a model from a maximal consistent set of formulas using the Lindenbaum-Henkin construction, leveraging the compactness theorem. Completeness shows that no valid first-order formula escapes any complete proof system—the expressive power of syntax matches semantics.
Begin with the contrapositive (if Γ is consistent, it has a model) and understand the Henkin construction. Work through a simplified completeness proof for propositional logic first. Discuss how completeness relates to the Löwenheim-Skolem theorem and compactness. Distinguish from the syntactic approach (Hilbert systems) vs. semantic approach (models).
You already know that a proof system for first-order logic is sound if every formula it can derive is actually valid — every proof leads somewhere true. Soundness is the easy direction and is established by checking that each inference rule preserves truth. Gödel's Completeness Theorem proves the converse: every valid formula *can* be derived. The formal statement is Γ ⊨ φ if and only if Γ ⊢ φ — semantic entailment and syntactic derivability coincide perfectly. This is a profound alignment between two very different ways of asking "must φ be true?"
The key challenge in proving completeness is the construction direction: given a consistent set of formulas Γ, we must produce a model that satisfies all of them. The Henkin construction is the standard approach. First, extend Γ to a maximal consistent set Γ* by a Lindenbaum-style argument: enumerate all formulas, adding each one that keeps the set consistent. Then, for every existential statement ∃x φ(x) in Γ*, introduce a fresh Henkin constant c and add φ(c) to the set. This gives every existence claim a witness. The resulting theory has the witness property: every existential claim is backed by a named element. Finally, the term model — whose universe is the set of all closed terms, with equality interpreted by provable equality — satisfies every sentence in Γ*. The model is built entirely from syntax, making it countable regardless of the complexity of Γ.
A critical distinction prevents over-applying completeness. Gödel's Incompleteness Theorems show that the theory of arithmetic (PA) has true sentences that are not provable from its axioms. But completeness says all *valid* formulas are provable — valid means true in *all* models, not just the standard one. Arithmetic has non-standard models with elements that behave strangely, and completeness holds for the whole first-order language. The incompleteness theorems say something different: some true arithmetic sentences are not provable from PA, meaning they are not universally valid — they fail in some non-standard model. First-order logic is complete as a *logic*; arithmetic is incomplete as a *theory*. These are different claims about different objects.
Completeness also implies the Compactness Theorem as an immediate corollary: if every finite subset of Γ is consistent (has a model), then Γ itself is consistent. The proof is one line — proofs are finite objects, so any derivation of a contradiction from Γ uses only finitely many formulas, which form a finite inconsistent subset. This means completeness, compactness, and the Löwenheim-Skolem theorems are all tightly linked: together, they characterize exactly what first-order logic can and cannot express, and they do so by showing that syntax and semantics, at the first-order level, are perfectly matched.