Parent: soundness-and-completeness
Completeness (Gödel, 1929 — forFOL)
Γ ⊨ φ ⟹ Γ ⊢ φ— anything true (in every model ofΓ) is provable. There are no gaps: the proof system is strong enough to reach every valid formula.
Proof — build a model out of syntax (semantics ← syntax)
The hard direction, and it crosses the syntax↔semantics gap the opposite way to soundness: instead of pushing truth down a proof, it manufactures a model from a consistent set of formulas. Work by contrapositive:
Γ ⊬ φ ⟹ Γ ⊭ φ— ifφis not provable, build a model ofΓwhereφis false (a countermodel), soφisn't valid.
The construction (Henkin / Lindenbaum):
Γ ⊬ φmeansΓ ∪ {¬φ}is consistent (syntactically — no proof of a contradiction).- Extend it to a maximal consistent set
Γ*(Lindenbaum: add formulas one by one, keeping consistency; add witnesses∃x.ψ → ψ[c/x]for the FOL case). Γ*is a model: read off truth from membership (φtrue⟺ φ ∈ Γ*); maximality + consistency make this a well-defined structure (a term model) satisfying all ofΓand¬φ. SoΓhas a model whereφfails →Γ ⊭ φ. ∎
The heart is the slogan "every consistent theory has a model" — a syntactic property (consistency) forces a semantic object (a model) into existence. That's completeness, and it's why the two sides coincide. The construction sketched here — Lindenbaum + Henkin + the truth lemma — is worked out in full in canonical-model.
What it buys
- Validity is semi-decidable: enumerate proofs; by completeness one appears iff
φis valid (the r.e. side of the Entscheidungsproblem). - Compactness falls out: if every finite subset of
Γis satisfiable,Γis consistent, hence (completeness) has a model — a workhorse of model theory. - Careful: this is completeness of the logic's proof system for validity — not the negation of Gödel incompleteness, which is about a theory failing to prove all arithmetic truths (see the caveat).
The canonical model that does all this work — the theory's own syntax turned into a structure — has its own note: canonical-model.