Completeness and Incompleteness Theorems

The Completeness Theorem establishes the exact agreement between two notions: syntactic provability ($⊢$), what a deductive calculus can derive, and semantic consequence ($\models$), what holds in all interpretations. For first-order logic these coincide, so the logic is adequate to its semantics. The Incompleteness Theorems concern a different relationship — within a fixed sufficiently strong theory $T$, there exist sentences neither provable nor refutable, and the consistency statement $\mathrm{Con}(T)$ is among them. The surprising fact is that these two results, superficially in tension ("complete" vs. "incomplete"), are about completely different objects: completeness is a property of the logic; incompleteness is a property of theories formalized within that logic. Together they delimit the reach of formal axiomatic mathematics.

The Core Insight

Completeness says: the proof system loses no information about validity. Incompleteness says: no single recursive theory captures all truths of arithmetic, because a theory able to talk about its own syntax can construct a sentence asserting its own unprovability. The bridge between syntax and semantics in one direction (completeness) is precisely what lets us reflect a theory's proof relation into arithmetic, enabling the self-reference that drives incompleteness.

Formal Statement

Syntactic and Semantic Consequence

Fix a first-order language $\mathcal{L}$. Let $T$ be a set of $\mathcal{L}$-sentences and $\phi$ an $\mathcal{L}$-sentence.

• $T⊢\phi$ ("$\phi$ is provable from $T$") means there is a finite formal derivation of $\phi$ from $T$ using the axioms and rules of a sound, fixed deductive calculus (e.g. a Hilbert system or natural deduction).
• $T\models \phi$ ("$\phi$ is a semantic consequence") means every $\mathcal{L}$-structure $\mathcal{M}$ that satisfies all of $T$ also satisfies $\phi$:

Here $\mathcal{M}=(M,I)$ is a domain $M$ with interpretation $I$ of the symbols; $\mathcal{M}\models \phi$ is defined by Tarski's recursion on formula structure.

Gödel–Henkin Completeness Theorem

For any first-order theory $T$ and sentence $\phi$,

Equivalently (the Model Existence form): a theory $T$ is consistent iff it has a model.

Recursively Axiomatizable, Consistent, Complete Theory

A theory $T$ is:

• recursively axiomatizable if it has a set of axioms whose Gödel numbers form a recursive (decidable) set;
• consistent if $T⊬\perp$, i.e. for no $\phi$ do we have both $T⊢\phi$ and $T⊢\neg \phi$;
• (negation-)complete if for every sentence $\phi$, $T⊢\phi$ or $T⊢\neg \phi$;
• $\omega$-consistent if there is no formula $\psi (x)$ with $T⊢\exists x\psi (x)$ yet $T⊢\neg \psi (\underline{n})$ for every numeral $\underline{n}$.

Gödel's First Incompleteness Theorem

Let $T$ be a consistent, recursively axiomatizable theory that interprets a modest fragment of arithmetic (e.g. Robinson arithmetic $\mathsf{Q}$). Then $T$ is incomplete: there is a sentence $G_T$ such that

provided $T$ is $\omega$-consistent (Rosser's strengthening needs only consistency). Moreover, if $T$ is sound (true in $\mathbb{N}$), then $G_T$ is true but unprovable.

Gödel's Second Incompleteness Theorem

Let $T\supseteq \mathsf{PA}$ (Peano Arithmetic) be consistent and recursively axiomatizable. Let $\mathrm{Con}(T):=\neg {\mathrm{Prov}}_T(┌\perp ┐)$. Then

The formalization requires the provability predicate to satisfy the Hilbert–Bernays–Löb derivability conditions:

Why It Holds / Derivation

Completeness via Henkin's Construction

We prove the Model Existence Theorem [3]: every consistent $T$ has a model. Equation [2]'s nontrivial direction follows because if $T⊬\phi$ then $T\cup \{\neg \phi \}$ is consistent, hence has a model, which falsifies $\phi$, giving $T/\models \phi$.

1. Henkin expansion. Extend $\mathcal{L}$ to ${\mathcal{L}}^{\ast }$ by adding a fresh constant $c_{\psi }$ for each formula $\psi (x)$ with one free variable. Add Henkin axioms $\exists x\psi (x)\to \psi (c_{\psi })$ for each. The resulting theory $T^{\ast }$ is conservative and still consistent (each axiom can be added without contradiction by a finitary argument).

1. Maximal consistent extension. By Lindenbaum's lemma (Zorn / enumeration), extend $T^{\ast }$ to a maximal consistent theory $T^{\ast \ast }$: for every sentence $\sigma$, exactly one of $\sigma ,\neg \sigma$ lies in $T^{\ast \ast }$. $T^{\ast \ast }$ remains a Henkin theory.

1. Term model. Let the domain be the set of closed ${\mathcal{L}}^{\ast }$-terms modulo the equivalence $t\sim s⟺(t=s)\in T^{\ast \ast }$. Interpret function and relation symbols by membership in $T^{\ast \ast }$. Each equivalence class has a witnessing Henkin constant.

1. Truth Lemma. By induction on formula complexity, for every sentence $\sigma$:

1. Conclusion. Since $T\subseteq T^{\ast \ast }$, the term model ${\mathcal{M}}^{\ast \ast }$ satisfies $T$. Restricting the interpretation back to $\mathcal{L}$ gives a model of $T$. $■$

The argument uses the Axiom of Choice (via Lindenbaum) in general; for countable $\mathcal{L}$ only a weak fragment (König / Boolean prime ideal) is needed.

First Incompleteness via the Diagonal Lemma

1. Arithmetization of syntax. Assign Gödel numbers to symbols, formulas, and finite sequences. Key fact: the relation ${\mathrm{Proof}}_T(p,n)$ — "$p$ codes a $T$-proof of the formula with code $n$" — is primitive recursive, hence representable in $\mathsf{Q}$. Define ${\mathrm{Prov}}_T(n):=\exists p{\mathrm{Proof}}_T(p,n)$, a ${\Sigma }_1$ formula.

1. Diagonal Lemma. For any formula $\theta (x)$ there is a sentence $\sigma$ with

1. The Gödel sentence. Apply the diagonal lemma with $\theta (x):=\neg {\mathrm{Prov}}_T(x)$, obtaining $G_T$ with

1. Not provable. If $T⊢G_T$, then by D1 $T⊢{\mathrm{Prov}}_T(┌G_T┐)$, but $T⊢G_T\to \neg {\mathrm{Prov}}_T(┌G_T┐)$ from [9], so $T$ proves both ${\mathrm{Prov}}_T$ and $\neg {\mathrm{Prov}}_T$ — contradiction with consistency. Hence $T⊬G_T$.

1. Not refutable. If $T⊢\neg G_T$, then $T⊢{\mathrm{Prov}}_T(┌G_T┐)$, i.e. $T$ proves $\exists p{\mathrm{Proof}}_T(p,┌G_T┐)$. But since $T⊬G_T$, no number actually codes such a proof; $\omega$-consistency forbids proving the existential while refuting every instance. Hence $T⊬\neg G_T$.

1. Rosser's improvement. Replace ${\mathrm{Prov}}_T$ by Rosser's "provable with no shorter refutation" predicate; the parallel argument needs only plain consistency. $■$

Kurt Gödel | 1906–1978

Born in Brünn (now Brno), Gödel announced the Completeness Theorem in his 1929 doctoral dissertation at the University of Vienna and the Incompleteness Theorems at the September 1930 Königsberg conference, with the full paper Über formal unentscheidbare Sätze... appearing in 1931. A member of the Vienna Circle's periphery, he overturned Hilbert's program of finitary consistency proofs. Emigrating to Princeton's Institute for Advanced Study in 1940, he became Einstein's closest walking companion, later proving the consistency of the Continuum Hypothesis and Choice via the constructible universe $L$ (1938–40) and discovering rotating-universe solutions to general relativity (1949). His Platonism and methodical caution shaped the foundations of mathematical logic.

Building Intuition

Think of completeness as a dictionary that translates perfectly in both directions between the language of proofs and the language of meaning. If something is true under every possible interpretation, the calculus can always find a finite proof of it — no truth slips through the syntactic net. This is a remarkable finiteness result: validity, which is quantified over a proper class of structures, is certified by a finite object (a proof).

Incompleteness then exploits the very richness of arithmetic. Because numbers can encode anything finite — including formulas and proofs — a theory of arithmetic can describe its own proof system. The Gödel sentence is a careful self-referential sentence, "I am not provable here." If the theory proved it, the theory would prove a falsehood (it is provable), so a consistent theory cannot. But then the sentence is true. Truth has outrun proof — not because of a flaw in the theory, but because no consistent recursive theory can be both complete and capable of self-description. The Second Theorem sharpens this: a system cannot pull itself up by its own bootstraps to certify its own coherence.

Syntax–semantics correspondence (completeness) versus the truth–provability gap (incompleteness)

<svg viewBox="0 0 760 400" xmlns="http://www.w3.org/2000/svg">
<rect width="760" height="400" fill="#0a0e17"/>
<text x="380" y="30" fill="#e2e8f0" font-size="18" text-anchor="middle">Completeness vs. Incompleteness</text>

<!-- Completeness: two circles equal -->
<text x="190" y="70" fill="#e2e8f0" font-size="14" text-anchor="middle">Completeness (logic level)</text>
<circle cx="190" cy="150" r="60" stroke="#94a3b8" fill="none" stroke-width="2"/>
<text x="190" y="120" fill="#e2e8f0" font-size="13" text-anchor="middle">Provable</text>
<text x="190" y="140" fill="#94a3b8" font-size="12" text-anchor="middle">T ⊢ φ</text>
<text x="190" y="165" fill="#d4a853" font-size="20" text-anchor="middle">=</text>
<text x="190" y="190" fill="#94a3b8" font-size="12" text-anchor="middle">T ⊨ φ</text>
<text x="190" y="208" fill="#e2e8f0" font-size="13" text-anchor="middle">Valid</text>
<text x="190" y="240" fill="#d4a853" font-size="12" text-anchor="middle">perfect match</text>

<!-- Incompleteness: provable ⊂ true -->
<text x="560" y="70" fill="#e2e8f0" font-size="14" text-anchor="middle">Incompleteness (theory level)</text>
<circle cx="560" cy="160" r="90" stroke="#94a3b8" fill="none" stroke-width="2"/>
<text x="560" y="95" fill="#e2e8f0" font-size="13" text-anchor="middle">True in ℕ</text>
<circle cx="540" cy="175" r="50" stroke="#d4a853" fill="none" stroke-width="2.5"/>
<text x="540" y="180" fill="#d4a853" font-size="12" text-anchor="middle">Provable</text>
<text x="540" y="196" fill="#94a3b8" font-size="11" text-anchor="middle">in T</text>
<circle cx="600" cy="130" r="4" fill="#e2e8f0"/>
<text x="630" y="125" fill="#e2e8f0" font-size="12">G_T</text>
<text x="640" y="142" fill="#94a3b8" font-size="11">(true,</text>
<text x="640" y="156" fill="#94a3b8" font-size="11">unprovable)</text>

<line x1="300" y1="160" x2="450" y2="160" stroke="#94a3b8" stroke-width="1" stroke-dasharray="5 4"/>
<text x="375" y="150" fill="#94a3b8" font-size="11" text-anchor="middle">different objects</text>

<text x="380" y="380" fill="#94a3b8" font-size="12" text-anchor="middle">Left: the deductive calculus is adequate. Right: a fixed recursive theory leaves true sentences unproven.</text>
</svg>

Worked Examples

Compactness as a Corollary — Coloring an Infinite Graph

1. Introduce, for each $v\in V$ and color $i\in \{1,2,3\}$, a propositional variable $c_{v,i}$ ("$v$ has color $i$").
2. Form the theory $T$: (a) $c_{v,1}\vee c_{v,2}\vee c_{v,3}$ for each $v$; (b) $\neg (c_{v,i}\wedge c_{v,j})$ for $i\ne j$; (c) $\neg (c_{u,i}\wedge c_{w,i})$ for each edge $\{u,w\}\in E$ and each color $i$.
3. Any finite subset $T_0\subseteq T$ mentions finitely many vertices, forming a finite subgraph, which by hypothesis is 3-colorable — giving a model of $T_0$. So $T$ is finitely satisfiable.
4. By Compactness, $T$ has a model $\mathcal{M}$. Read off the coloring: assign $v$ the unique color $i$ with $\mathcal{M}\models c_{v,i}$.

The whole strength came from [3]: consistency (here, finite satisfiability) yields a model.

Computing the Gödel Number Growth and Why $G_T$ Is True

1. The 200th prime is $p_{200}=1223$. The number is bounded above by $p_{200}^{k\bar{a}}$ roughly, but the exact value is ${\prod }_{i=1}^{200}{p}_i^{a_i}$.
2. Order of magnitude (base-10 digits): ${\log }_{10}┌G_T┐={\sum }_i{a}_i{\log }_{10}{p}_i\approx k\bar{a}\cdot \overline{{\log }_{10}p}$. With $\overline{{\log }_{10}p}\approx {\log }_{10}(600)\approx 2.78$, we get $\approx 200\cdot 12\cdot 2.78\approx 6672$ digits.
3. Truth argument. $G_T$ asserts $\neg {\mathrm{Prov}}_T(┌G_T┐)$. We proved (Step 4 of the First Incompleteness proof) that $T⊬G_T$ when $T$ is consistent. Therefore no natural number $p$ actually codes a $T$-proof of $G_T$, so the statement "there is no proof of $G_T$" is true in $\mathbb{N}$.

The astronomical size is irrelevant to the logic — what matters is that $G_T$ is a perfectly definite arithmetic statement.

Common Misconceptions

A Complete but Non-arithmetic Theory Escapes Incompleteness

The hypotheses of the First Incompleteness Theorem are essential. The theory $\mathsf{Th}(\mathbb{R},+,\cdot ,<,0,1)$ — the real closed field axioms — is complete and decidable (Tarski, 1948). It does not contradict Gödel because it cannot define the integers as a subset, so it cannot arithmetize its own syntax. Likewise Presburger arithmetic (natural numbers with $+$ but no $\times$) is complete and decidable. Multiplication together with addition is exactly what enables the coding that triggers incompleteness.

Connections

The Completeness Theorem is the entry point to Model Theory: it guarantees models exist, underwriting the Compactness Theorem and the Löwenheim–Skolem Theorems, from which non-standard models of arithmetic and analysis (the foundation of Nonstandard Analysis) flow. The arithmetization of syntax connects incompleteness to Computability Theory: ${\mathrm{Prov}}_T$ being ${\Sigma }_1$ is the same phenomenon as recursively enumerable sets, and the unsolvability of the Halting Problem gives an alternative route to the First Incompleteness Theorem. The Second Theorem is the semantic content of the modal logic Provability Logic ($\mathsf{GL}$), via Solovay's completeness theorem, and underlies Löb's Theorem. Finally, Tarski's Undefinability of Truth is the close cousin obtained by diagonalizing the (undefinable) truth predicate rather than the (definable) provability predicate.

Real-World Applications

1. Automated theorem proving. Completeness guarantees that resolution-based provers (Prolog, SAT/SMT backends like Z3, Vampire) will eventually derive any valid first-order consequence — semantic correctness translates into a complete search procedure.
2. Program verification & limits thereof. Rice's theorem and incompleteness jointly explain why no algorithm can decide all nontrivial semantic properties of programs; verification tools (Coq, Isabelle, Lean) must rely on interactive proof and unprovable trusted cores.
3. Database theory. The compactness and completeness machinery underlies the semantics of first-order query languages and the decidability boundaries of conjunctive-query containment.
4. Cryptographic and security proofs. Formal proof assistants (used to verify TLS implementations, the seL4 microkernel) operate within a fixed theory; Gödelian limits mean the consistency of the trusted base is an article of faith, not internally provable.
5. Foundations of set theory. The Second Theorem implies $\mathsf{ZFC}$ cannot prove its own consistency, motivating the hierarchy of Large Cardinal Axioms, each strictly increasing consistency strength.
6. Reverse mathematics. Calibrating which theorems require which axioms (the subsystems ${\mathsf{RCA}}_0,{\mathsf{WKL}}_0,{\mathsf{ACA}}_0,\dots$) is built directly on Gödelian and completeness-style metamathematics.
7. Philosophy of mind (Lucas–Penrose argument). Claims that human mathematicians transcend any formal system invoke incompleteness; widely contested, but a concrete cultural application of the theorems.

Historical Development

• 1900 — Hilbert poses his second problem: prove the consistency of arithmetic, launching the finitist program.
• 1928 — Hilbert and Ackermann pose the Entscheidungsproblem and ask whether first-order logic is complete.
• 1929 — Gödel proves the Completeness Theorem in his Vienna dissertation, answering Hilbert–Ackermann affirmatively.
• 1930 (Sept., Königsberg) — Gödel announces the First Incompleteness Theorem; von Neumann immediately grasps and independently derives the Second.
• 1931 — Gödel publishes Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, establishing both Incompleteness Theorems.
• 1936 — Gentzen proves the consistency of $\mathsf{PA}$ by transfinite induction to ${\epsilon }_0$; Turing and Church independently settle the Entscheidungsproblem negatively, linking incompleteness to undecidability.
• 1936 — Rosser strengthens the First Theorem to require only consistency (not $\omega$-consistency).
• 1949 — Henkin gives the streamlined model-theoretic proof of completeness now standard.
• 1955 — Löb proves Löb's Theorem; the Hilbert–Bernays–Löb derivability conditions crystallize the Second Theorem's hypotheses, later subsumed by Solovay's 1976 arithmetical completeness of $\mathsf{GL}$.

Subtleties & Limits

Several deep issues persist around the incompleteness phenomenon. (1) Intensionality of the Second Theorem. $\mathrm{Con}(T)$ depends on how provability is formalized; Feferman (1960) exhibited a provability predicate (not satisfying D3) under which a $T$ "proves its own consistency" — clarifying that the Second Theorem requires the natural, derivability-condition-satisfying formalization. Pinning down the canonical notion remains philosophically contested. (2) Concrete mathematical independence. Beyond artificial Gödel sentences, the Paris–Harrington theorem (1977), the Hydra game (Kirby–Paris), and Goodstein's theorem give natural combinatorial statements independent of $\mathsf{PA}$; the program of finding ever more "mathematically ordinary" independent statements (e.g. in graph minor theory, Friedman's work on $\mathsf{ZFC}$-independence) is open-ended. (3) The ordinal analysis frontier. Determining the proof-theoretic ordinals of strong theories (notably full second-order arithmetic ${\Pi }_1^1\text{-}{\mathsf{CA}}_0$ and beyond) is among the hardest active problems in proof theory. (4) Absolute provability. Whether there is a sharp, theory-independent notion of "the mathematical truths humans can in principle know" — and whether it can be a recursive theory — connects incompleteness to open questions in the philosophy of mathematics.

See Also