Proof Theory
Gödel's Completeness Theorem: Provable Equals True in Every Model
Gödel's Completeness Theorem is the reason first-order logic works: it guarantees that anything true in every model of a set of axioms can actually be derived from those axioms in finitely many mechanical steps. Semantic truth and syntactic proof — two ideas that look wildly different — turn out to coincide exactly. Symbolically, for a first-order theory T and sentence φ, T ⊨ φ if and only if T ⊢ φ.
Proved by Kurt Gödel in his 1929 doctoral dissertation (published 1930), the theorem tells us that a finite, purely formal proof calculus is powerful enough to capture all logical consequences. Do not confuse it with his later, opposite-flavored Incompleteness Theorems (1931): completeness is about the logic itself being adequate; incompleteness is about specific theories like arithmetic being unable to decide every sentence in their own language.
- FieldMathematical logic / proof theory / model theory
- First provedKurt Gödel, 1929 dissertation (published 1930)
- StatementFor first-order logic: T ⊨ φ ⟺ T ⊢ φ
- Key hypothesisFirst-order logic with a sound, complete deductive calculus; countable or arbitrary signature
- Standard proof techniqueHenkin construction — build a model from a maximal consistent, witnessed theory
- Equivalent formEvery consistent first-order theory has a model (Model Existence Theorem)
Interactive visualization
Press play, or step through manually. The visualization is yours to drive — try it before reading on.
Watch the 60-second explainer
A condensed visual walkthrough — narrated, captioned, under a minute.
The precise statement: two arrows that always match
Fix a first-order language (signature) L. For a set of L-sentences T and an L-sentence φ, define two relations:
- Semantic (⊨): T ⊨ φ means every structure (model) 𝔐 that satisfies all sentences of T also satisfies φ. This is a statement about all possible worlds — potentially uncountably many.
- Syntactic (⊢): T ⊢ φ means there is a finite formal derivation of φ from T using a fixed proof calculus (axioms + rules like modus ponens and generalization).
Gödel's Completeness Theorem. For first-order logic, T ⊨ φ if and only if T ⊢ φ.
The 'only if' direction (⊨ ⟹ ⊢) is the deep content and is what 'completeness' names: every semantic consequence is provable. The reverse direction (⊢ ⟹ ⊨) is soundness and is comparatively easy. An equivalent, often more useful packaging is the Model Existence Theorem: a theory T is consistent (T ⊬ ⊥) if and only if T has a model.
The picture: closing the gap between worlds and words
Truth in every model is an infinitary, semantic condition — you would have to survey the entire proper class of structures, each possibly of enormous cardinality. Provability is finitary and combinatorial — a finite string of symbols you can in principle check by hand or by machine. There is no a priori reason these should agree.
The theorem says the gap is illusory for first-order logic. The mental image: the two relations ⊨ and ⊢ carve the space of sentences into 'consequences' and 'non-consequences', and completeness says the two cuts fall in exactly the same place.
The contrapositive is the workhorse view. If φ is not provable from T, then completeness manufactures a concrete counterexample: a model of T ∪ {¬φ}. So unprovability is witnessed by a model. This is why independence results in set theory (e.g. the Continuum Hypothesis) are proved by building models — Gödel's L for consistency, Cohen forcing for independence — rather than by hunting for a syntactic derivation.
The key idea of the proof: Henkin's construction of a model out of syntax
Leon Henkin (1949) gave the cleanest proof. It suffices to show the Model Existence form: every consistent T has a model. The move is startling — you build the model out of the syntax itself.
- Add witnesses. For each formula ∃x ψ(x), introduce a fresh constant c and the axiom ∃x ψ(x) → ψ(c). These Henkin constants promise that whatever is asserted to exist has a name. This stays consistent.
- Extend to maximal consistency. Using Lindenbaum's Lemma (a Zorn / König-type argument), extend the witnessed theory to a maximal consistent set T*. Now for every sentence σ, exactly one of σ, ¬σ is in T*.
- Read off the model. Take the term model whose domain is the closed terms (modulo the equivalence t ≈ s ⟺ (t = s) ∈ T*). Interpret each relation and function symbol exactly as T* dictates.
A truth lemma then proves by induction on formula complexity that 𝔐 ⊨ σ ⟺ σ ∈ T*. The existential step is exactly where the Henkin witnesses are needed. Since T ⊆ T*, this 𝔐 is a model of T. Gödel's original 1929 proof was different in detail but the same in spirit; Henkin's is what everyone teaches.
A worked special case: the Compactness Theorem falls right out
Completeness instantly yields Compactness: a set T of first-order sentences has a model iff every finite subset does. Why? A formal proof of ⊥ from T uses only finitely many premises. So if T is inconsistent, some finite T₀ ⊆ T is already inconsistent; contrapositively, if every finite subset is satisfiable (hence consistent, by soundness), then T is consistent, hence has a model by Model Existence.
A concrete payoff: let T be the theory of fields of characteristic 0, i.e. the field axioms plus the infinitely many sentences 1+1 ≠ 0, 1+1+1 ≠ 0, …. Any statement σ true in all characteristic-0 fields already follows from the field axioms together with finitely many of those inequalities — so σ holds in every field of sufficiently large prime characteristic p. This 'transfer' between characteristic 0 and large characteristic p (used all over algebraic geometry, e.g. Ax–Grothendieck) is a direct dividend of completeness via compactness.
Why the hypotheses matter: first-order is essential
The theorem is a delicate property of first-order logic. Change the logic and it breaks:
- Second-order logic (with standard/full semantics) has no completeness theorem. The natural numbers (ℕ, +, ×, 0, 1) are characterized up to isomorphism by a single second-order sentence (categoricity of second-order PA), yet the set of second-order validities is not even recursively enumerable — so no sound, effective proof calculus can derive all of them. If a completeness theorem held for full second-order logic, it would collide with the incompleteness of arithmetic.
- Infinitary logics like L_{ω₁,ω} (countable conjunctions) also generally lack completeness for their full semantics.
By contrast, first-order completeness is intimately tied to the downward Löwenheim–Skolem theorem: the Henkin model over a countable language is countable, so a consistent countable theory has a countable model. This is exactly why first-order logic cannot pin down the reals or ℕ up to isomorphism — Skolem's 'paradox' — the very expressive weakness that makes completeness (and compactness) possible.
Applications and significance: the foundation of model theory
Completeness is the license that makes model theory a subject. The dictionary 'consistent theory ⟷ existing model' lets logicians study algebra by building and comparing structures:
- Independence proofs. To show φ is not provable from T, exhibit a model of T ∪ {¬φ}. This is how the parallel postulate's independence, the independence of the Axiom of Choice and the Continuum Hypothesis (via Gödel's L and Cohen forcing), and countless algebraic non-implications are established.
- Nonstandard analysis. Compactness (hence completeness) produces models of the reals containing infinite and infinitesimal elements — Robinson's rigorous infinitesimals.
- Effectiveness. Because validities are the provable sentences and proofs are finite, the set of first-order validities is recursively enumerable (a semi-decision procedure exists), though by Church–Turing not decidable.
Philosophically, completeness vindicates the formal-axiomatic method for first-order reasoning: nothing that is genuinely a logical consequence escapes the proof system. It sets the exact stage against which the 1931 Incompleteness Theorems then measure what individual theories cannot do.
| Feature | Completeness Theorem (1929/30) | First Incompleteness Theorem (1931) |
|---|---|---|
| What it is about | The logic (first-order provability) itself | A specific theory (e.g. Peano Arithmetic) |
| Statement | T ⊨ φ ⟺ T ⊢ φ | There is a true sentence G with PA ⊬ G and PA ⊬ ¬G |
| Good or bad news? | Positive: the proof calculus captures all consequences | Negative: strong effective theories can't decide every sentence |
| Notion of 'complete' | The deductive system is complete | The theory PA is incomplete (not negation-complete) |
| Key mechanism | Henkin / model existence construction | Self-reference via arithmetized provability (diagonal lemma) |
Frequently asked questions
How is the Completeness Theorem different from the Incompleteness Theorems?
They are about different things and are not in tension. Completeness (1929/30) says the first-order proof calculus is adequate: every sentence true in all models of T is provable from T. Incompleteness (1931) says a specific consistent, effectively axiomatized theory strong enough for arithmetic (like PA) has sentences G with PA ⊬ G and PA ⊬ ¬G. One is about the logic being complete; the other is about a theory failing to be negation-complete.
What does 'complete' actually refer to here?
It refers to the deductive system, not to any particular theory. The proof calculus is complete because it can derive every semantic consequence: ⊨ implies ⊢. This is distinct from a theory T being 'complete' in the sense that for every sentence σ, T ⊢ σ or T ⊢ ¬σ (negation-completeness), which is the notion the Incompleteness Theorem shows PA lacks.
Why does the theorem fail for second-order logic?
Full (standard-semantics) second-order logic can categorically characterize structures like (ℕ, +, ×); its set of validities encodes arithmetic truth and is not recursively enumerable. No sound, effective proof system can enumerate all of those validities, so there is no completeness theorem. If second-order logic were complete, arithmetic truth would be recursively axiomatizable, contradicting incompleteness. (Second-order logic with Henkin semantics does regain completeness — but that is essentially many-sorted first-order logic.)
What is the role of the Henkin constants in the proof?
They guarantee that the model we build from the syntax has genuine witnesses for existential statements. When the truth lemma is proved by induction, the ∃x ψ(x) case requires that if ∃x ψ(x) is in the maximal consistent theory, some closed term names an element satisfying ψ. Adding a fresh constant c with the axiom ∃x ψ(x) → ψ(c) for every existential formula supplies exactly those names, so the term model's domain contains the needed witnesses.
How does completeness give the Compactness Theorem?
A formal derivation is finite, so it can invoke only finitely many premises. Hence if T proves a contradiction, some finite subset already does. Contrapositively, if every finite subset of T is satisfiable (so consistent, by soundness), then T is consistent, and by the Model Existence form of completeness T has a model. This is the standard route from completeness to compactness for first-order logic.
Does the theorem require the language to be countable?
No. Gödel's original result is stated for countable signatures, but the Henkin construction generalizes to signatures of arbitrary cardinality using Zorn's Lemma for the maximal-consistent extension. The resulting model then has cardinality at most that of the language. Countability is only needed if you want the sharper conclusion that a consistent countable theory has a countable model (downward Löwenheim–Skolem).