Gödel's Completeness Theorem

Gödel’s completeness theorem is a fundamental result in mathematical logic establishing that the standard deductive calculi for classical first-order logic can prove every consequence that holds under all interpretations of their premises. It connects semantic truth with formal derivability: if a sentence is true in every model of a theory, it has a finite proof from that theory. Kurt Gödel established the result in his 1929 doctoral dissertation and published a revised proof in 1930. (www3.cs.stonybrook.edu)

Formal statement

Let $T$ be a set of first-order sentences and $\varphi$ a sentence in the same language. The notation $T\models\varphi$ means that every structure satisfying all sentences of $T$ also satisfies $\varphi$. The notation $T\vdash\varphi$ means that a formal proof of $\varphi$ exists from assumptions in $T$, using a specified deductive calculus. Completeness asserts

The converse is soundness, which ensures that derivations preserve truth. Together they yield

This is a correspondence between syntax, concerning symbolically defined derivations, and semantics, concerning interpretations and satisfaction. (math.umd.edu)

With no premises, the theorem says that every sentence possessing logical validity—truth in every structure—is provable using logical axioms alone. Allowing arbitrary, possibly infinite sets of premises gives the formulation commonly called strong completeness. An equivalent model-existence formulation states that every syntactically consistent first-order theory has a model. Consistency here means that no contradiction can be derived; it does not mean that the theory correctly describes a particular intended structure. (math.umd.edu)

Historical context and deductive systems

Gödel’s result extended the completeness investigations of propositional logic to predicate logic, where quantifiers range over individual objects. His original argument used a Hilbert-style calculus: logical axioms and rules of inference generate finite derivations. Other presentations employ natural deduction or sequent calculus. Completeness concerns a calculus together with its semantics; it is not a guarantee that any arbitrarily chosen collection of inference rules captures all valid arguments. (academic.oup.com)

Leon Henkin developed an influential alternative proof in his 1947 dissertation, published in 1949. Rather than directly transforming valid formulas into derivations, his approach constructs a model from a consistent set of sentences. This model-building perspective makes the relationship between proof theory and model theory particularly explicit. (www3.cs.stonybrook.edu)

The Henkin proof strategy

The proof first enlarges the language with fresh constants serving as witnesses for existential statements. For each appropriate formula $\psi(x)$, it introduces a sentence of the form

where $c$ is a new constant. The extensions are arranged so that consistency is preserved and existential formulas introduced during the construction also receive witnesses. The resulting theory is extended to a maximal consistent set, which contains either each sentence or its negation. (math.umd.edu)

A term model is then constructed. Its objects are closed terms, identified when the enlarged theory proves their equality. Provable equality thus defines an equivalence relation, and the domain consists of its equivalence classes. Function symbols act by forming terms, while relation symbols are interpreted according to membership of atomic sentences in the maximal consistent set. An induction on formula structure establishes the truth lemma: a sentence holds in this model exactly when it belongs to the set. Existential witnesses supply the crucial quantifier step. (pi.math.cornell.edu)

Finally, suppose $T\models\varphi$ but $T\not\vdash\varphi$. Then $T\cup\{\neg\varphi\}$ is consistent, so the construction provides a model satisfying $T$ but falsifying $\varphi$. This contradicts the assumed semantic consequence and proves completeness. (pi.math.cornell.edu)

Consequences for models

The compactness theorem follows because every formal proof uses only finitely many premises. If every finite subset of $T$ has a model, soundness excludes a contradiction derived from any finite subset. Consequently $T$ is consistent, and completeness supplies a model of the entire theory. Equivalently, any semantic consequence of $T$ already follows from some finite subset of $T$. (math.umd.edu)

For a language with a countable collection of symbols, the Henkin construction produces a model with an at most countable domain. This gives a model-existence form of the Löwenheim–Skolem theorem. It does not imply that all models are countable, or that the constructed model is the intended interpretation of the axioms. (pi.math.cornell.edu)

Completeness, incompleteness, and decidability

The theorem does not conflict with Gödel’s incompleteness theorems. Logical completeness concerns deriving everything true in all models of given premises. Completeness of a theory instead means that it decides every sentence by proving either that sentence or its negation. A consistent, effectively axiomatized theory sufficiently strong for arithmetic, such as first-order arithmetic based on the Peano axioms, can be incomplete despite using a complete logical calculus. An independent sentence and its negation then hold in different models of the theory. (pi.math.cornell.edu)

Nor does completeness provide a terminating algorithm for every logical question. With an effective presentation of the language and calculus, proofs can be enumerated, so a search eventually finds a proof of any valid sentence. For an invalid sentence, that search need not terminate. General first-order validity is undecidable. (courses.grainger.illinois.edu)

The semantic qualification also matters for second-order logic. Under full semantics, where relation variables range over all relations of the appropriate arity, no effective sound calculus proves every validity. Under Henkin semantics, those variables range over specified collections, and an appropriate completeness theorem becomes available. (ps.uni-saarland.de)