Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Gödel’s Incompleteness Theorems — Arithmetic, Self-Reference, and the Limits of Formal Systems

Overview

In 1931, Kurt Gödel published Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I (“On Formally Undecidable Propositions of Principia Mathematica and Related Systems, I”). The result was devastating: any formal system capable of expressing elementary arithmetic is either inconsistent or incomplete — there are true statements expressible in the system that the system itself cannot prove. This shattered the Hilbert program, the early-20th-century project to secure mathematics by formalizing it in a complete, consistent, decidable axiomatic system. Hilbert had asked three questions: (1) Consistency: can the axioms of arithmetic be proved consistent using only finitistic methods? (2) Completeness: can every true arithmetical statement be proved? (3) Decidability (Entscheidungsproblem): is there an algorithm deciding theorem-hood?

Gödel’s first theorem answered (2) in the negative (for any sufficiently strong, consistent, effectively axiomatized system). His second answered (1) in the negative (such a system cannot prove its own consistency). Turing’s 1936 paper answered (3) in the negative, via the undecidability of the Halting Problem. The Church–Turing thesis, formulated jointly from these two papers, identifies the effectively computable functions with the recursive (λ-definable, Turing-machine-computable) ones.

Related: Logic, Proof Techniques, Turing Machines, Computability, Lambda Calculus

Formal Systems and the Hilbert Program

A formal system F consists of (i) a formal language (well-formed formulas), (ii) a set of axioms — formulas taken as given, and (iii) a set of inference rules — relations producing new formulas from old. A proof is a finite sequence of formulas each of which is either an axiom or follows from earlier formulas by a rule. F is effectively axiomatized if there is an algorithm that, given a finite sequence, decides whether it is a valid proof — i.e., the axioms and rules are recursive.

Hilbert’s vision, articulated in his 1900 and 1928 addresses, was to put all of mathematics on such a footing. The Principia Mathematica of Russell & Whitehead (1910–1913) was an attempt; Peano arithmetic PA was the proposed foundation for the natural numbers. The dream required the system to be: consistent (no φ ∧ ¬φ is provable), ω-consistent (a stronger condition: if ∃x φ(x) is provable, then some ¬φ(n) is not provable), complete (every closed formula or its negation is provable), and decidable (an algorithm decides theorem-hood). Gödel showed these cannot simultaneously hold for any system containing arithmetic.

Gödel Numbering — Arithmetization of Syntax

The key technical innovation is arithmetization of syntax: encode formulas and proofs as natural numbers, and use arithmetic itself to talk about syntactic properties. Gödel invented a coding scheme — primitive recursive functions that map each symbol, formula, and proof to a unique natural number, with the syntactic operations (substitution, modus ponens, etc.) becoming primitive recursive functions on these numbers. Concretely, a sequence of symbols s_1, …, s_n is encoded as 2^s_1 · 3^s_2 · 5^s_3 · ... · p_n^s_n (the product of the first n primes raised to the respective code powers); by the fundamental theorem of arithmetic, this is bijective.

The crucial fact is that the predicates “n is the code of a well-formed formula”, “the formula coded by m is an axiom”, “p is the code of a valid proof of the formula coded by q”, etc., are all primitive recursive — expressible purely arithmetically with bounded quantification. So Peano arithmetic can “talk about” its own syntax. In particular, there is a primitive recursive predicate Prf(p, q) meaning “p is the Gödel number of a proof of the formula with Gödel number q”. The predicate Prov(q) := ∃p. Prf(p, q) (“q is provable”) is recursively enumerable. These arithmetical predicates are definable inside PA — there is a formula Proof_PA(p, q) of PA such that for actual naturals n, m, PA ⊢ Proof_PA(n̄, m̄) iff n is really a PA-proof of the formula numbered m, and PA ⊢ ¬Proof_PA(n̄, m̄) otherwise.

The Diagonal Lemma

The diagonal lemma (also called the fixed-point lemma) is the technical heart of the incompleteness proof. It says:

For any formula φ(x) with one free variable x in the language of arithmetic, there is a sentence G such that PA ⊢ G ↔ φ(⌜G⌝).

Here ⌜G⌝ is the numeral (formal term S^0…0 with the right number of S’s) denoting the Gödel number of G. In words: for any property φ expressible in arithmetic, there is a sentence G that is provably equivalent (in PA) to “φ holds of (the code of) G itself”.

The proof is a careful diagonalization. Given φ(x), define a (primitive-recursive, hence PA-representable) function f that takes a formula A(y) with free variable y and returns the sentence A(⌜A⌝) — substituting A’s own code into itself. Let B(y) := φ(f(y)), where f is the internal PA representative. Let n be the Gödel number of B(y), and let G := B(n̄) = φ(f(n̄)). Now compute: f(n) is the Gödel number of B(n̄) = G itself, so f(n̄) = ⌜G⌝ numerally. Hence G = φ(f(n̄)) = φ(⌜G⌝), modulo the proof that PA can verify this reasoning internally. The lemma gives us the provable equivalence G ↔ φ(⌜G⌝).

The First Incompleteness Theorem

Now apply the diagonal lemma to the formula ¬Prov(x), where Prov(x) := ∃p. Prf(p, x) says “x is provable in PA”. The lemma gives a sentence G such that:

PA ⊢ G ↔ ¬Prov(⌜G⌝)

Read this sentence: G is true iff G is not provable. This is the arithmetical Liar sentence — but unlike the natural-language Liar (“this sentence is false”), G is well-formed and unambiguously true-or-false.

The argument

  1. Suppose PA ⊢ G (G is provable). Then Prov(⌜G⌝) is true (a real proof exists) and PA can prove Prov(⌜G⌝) (we can compute the proof’s code and verify it). But G ↔ ¬Prov(⌜G⌝) is provable in PA, so PA also proves ¬G. Hence if PA is consistent, PA does not prove G.
  2. Suppose PA ⊢ ¬G. Then PA proves Prov(⌜G⌝) (since ¬G ↔ Prov(⌜G⌝)). But PA also proves ¬G and Prov(⌜G⌝). If PA is ω-consistent (a slightly stronger condition than consistency), then PA cannot prove ¬Prov(⌜G⌝) for every numeral, which is what would follow from PA ⊢ ¬Prov(⌜G⌝). Rosser (1936) strengthened the result to require only consistency, by constructing a Rosser sentence R such that R ↔ ∀p. Prf(p, ⌜R⌝) → ∃q<p. Prf(q, ⌜¬R⌝) — R says “for every proof of me, there’s a smaller proof of my negation.”
  3. Therefore, if PA is consistent (Rosser) or ω-consistent (Gödel), neither G nor ¬G is provable. PA is incomplete.

The result is robust: it applies to any effectively axiomatized, consistent theory T that contains enough arithmetic — Peano Arithmetic, Zermelo-Fraenkel set theory (ZFC), second-order arithmetic, etc. — for any “interesting” formal system. Even adding G as a new axiom doesn’t help: one can construct a new sentence G’ for the strengthened system, and the same diagonal argument applies.

Formal system T (consistent, contains arithmetic)
       │
       ▼
   Arithmetize syntax  →  formulas and proofs as natural numbers
       │
       ▼
   Diagonal lemma  →  sentence G_T with T ⊢ G_T ↔ ¬Prov_T(⌜G_T⌝)
       │
       ▼
   G_T is true but unprovable in T; ¬G_T is also unprovable
       │
       ▼
   T is incomplete

The Second Incompleteness Theorem

Gödel also showed that the consistency of PA — a sentence Con(PA) asserting “there is no proof of 0=1” — is one of these unprovable statements:

Second Incompleteness Theorem. If T is consistent and contains enough arithmetic, then T ⊬ Con(T).

The idea: G_T ↔ ¬Prov(⌜G_T⌝), and G_T is true (since if PA ⊢ G_T then PA is inconsistent). The sentence G_T essentially says “I am not provable in T.” But Con(T) — formally, “there is no T-proof of 0 = 1” — also implies “no formula is T-provable” in the sense used by Prov. In fact, the equivalence

Con(T) → G_T

is provable inside T (Gödel verified this — see Hilbert–Bernays 1934–39 for the precise conditions, since the proof requires formalizing the derivability conditions). Therefore, if T ⊢ Con(T), then T ⊢ G_T by modus ponens. But by the first theorem, T ⊬ G_T if T is consistent. Therefore T ⊬ Con(T).

This devastates the Hilbert program: the consistency of arithmetic cannot be established within arithmetic using finitary methods, because finitary methods are arithmetic. Gentzen (1936) gave a proof of PA’s consistency using transfinite induction up to ε_0 — but this uses resources stronger than PA itself, and so doesn’t contradict the second theorem. Modern relative consistency proofs (forcing in set theory, Cohen 1963) likewise use a stronger theory to prove the consistency of a weaker one.

The Liar’s Paradox Connection

The Liar paradox — “this sentence is false” — has been known since antiquity (Epimenides the Cretan: “all Cretans are liars”). In classical logic it generates a contradiction: if the sentence is true, it’s false; if false, it’s true. Tarski (1933) formalized this as: a sufficiently rich, consistent formal system cannot contain its own truth predicate.

Gödel’s contribution was to take the Liar and make it rigorous. The trick: replace “true” with “provable” (a syntactic property, not semantic), and use arithmetization to make the self-reference exact. The result is a sentence that is actually true (when PA is consistent, G is true — a theorem in a meta-theory, e.g., ZFC) but not provably so inside PA. So the system is consistent, the unprovable sentence is true, but the system can’t certify that truth.

Hofstadter’s Gödel, Escher, Bach (1979) makes the point that the Liar, Gödel’s sentence, and Escher’s Drawing Hands and Picture Gallery are all instances of strange loops — self-referential structures that fold a system back on itself, producing paradox when the system is naively interpreted as describing itself. The mathematical resolution is to keep the meta-level (where G is provably true) separate from the object-level (where G is unprovable); Hofstadter argues this stratification is the key to understanding consciousness and cognition.

Implications for Mathematics and Computing

For mathematics

Gödel’s theorems killed the Hilbert program as originally stated and reshaped philosophy of mathematics. Gödel himself was a platonist — he believed arithmetical statements have objective truth values independent of any formal system. The first incompleteness theorem, on this view, says our formal systems are approximations of mathematical truth, not its definition. Formalism has to be modified: a formal system is a tool, not the source of mathematical truth — some truths transcend any particular formal system. Intuitionism (Brouwer) is partly vindicated: the failure of classical completeness suggests the law of excluded middle A ∨ ¬A is suspect (and indeed every theorem in intuitionistic logic can be read via Curry–Howard as a constructive program). The results led to model theory (Skolem, Tarski, Robinson), forcing (Cohen), and large-cardinal axioms (Gödel, Cohen, Woodin) as ways to add new axioms whose consistency cannot be proved in ZFC but which can be shown relative to stronger principles.

For computing — the Church–Turing thesis and the Halting Problem

Gödel’s theorem is closely related to two foundational results of computability theory:

  1. Church–Turing thesis (1936): the intuitively computable functions are exactly the λ-definable, recursive, and Turing-computable functions. Gödel’s acceptance of this thesis — partly motivated by Turing’s analysis of “a computor” (a human following a mechanical procedure) — established the equivalence of his recursion-theoretic formulation with Turing’s machine model.

  2. Undecidability of the Halting Problem (Turing 1936): no algorithm decides, given a Turing machine M and input w, whether M halts on w. Turing’s proof is a direct diagonalization parallel to Gödel’s:

  Suppose H(M, w) decides halting.
  Define D(M) := if H(M, M) = "halts" then LOOP; else HALT.
  Run D(D): D(D) halts iff D(D) loops. Contradiction.

The structure mirrors Gödel: define a function that, applied to its own description, contradicts itself. The diagonal lemma is doing the same work as Turing’s diagonal construction; the Halting Problem is the “incompleteness theorem” of computability theory.

Many undecidable problems are equivalent to or harder than the Halting Problem: the Entscheidungsproblem (deciding theorem-hood in first-order logic), the word problem for groups, Hilbert’s tenth problem (Diophantine solvability — Matiyasevich 1970), the Post Correspondence Problem, and Rice’s theorem (any non-trivial property of recursively enumerable languages is undecidable). The Halting Problem and the incompleteness theorem are formally equivalent: the set of Gödel numbers of true arithmetical sentences is recursively enumerable but not recursive (Tarski); the set of PA-theorems is recursively enumerable but not complete; the set of (Turing) theorems is recursively enumerable but not decidable for membership.

What Gödel Does Not Say

A few common misconceptions deserve correction:

  • Truth is not impossible to know. G is true (in the standard model ℕ) but unprovable in PA — provable in ZFC and stronger systems. There is no absolute incompleteness, only relative.
  • Not all formal systems are flawed. Only those containing arithmetic, effectively axiomatized, and (ω-)consistent. Propositional logic is complete (Post 1921); first-order logic is complete (Gödel’s 1929 completeness theorem — different from the incompleteness theorems!); Presburger arithmetic (addition only) is complete and decidable (Presburger 1929).
  • Gödel does not imply human minds are non-mechanical. The Lucas–Penrose argument (1961, 1989) claims humans can “see” G is true and so exceed machines; this is a philosophical, not mathematical, conclusion and widely disputed.
  • Gödel does not say randomness helps. Chaitin’s incompleteness (algorithmic information theory) shows a sufficiently strong formal system cannot prove statements of the form “string X is algorithmically random” beyond a certain complexity bound — a strengthening of Gödel, not a separate phenomenon.

Interview Questions

Q: State Gödel’s first incompleteness theorem. A: Any effectively axiomatized, consistent (or ω-consistent for Gödel’s original statement; Rosser weakened to plain consistency) theory that contains enough arithmetic is incomplete — there is a sentence G in the language of the theory such that neither G nor ¬G is provable. The proof uses arithmetization of syntax and the diagonal lemma to construct a self-referential G equivalent to “G is not provable.”

Q: Why can’t PA prove its own consistency? A: Gödel’s second theorem: if T is consistent and contains arithmetic, T ⊬ Con(T). The reason is that G_T ↔ ¬Prov(⌜G_T⌝) is provable in T, and Con(T) → G_T is also provable in T (under the derivability conditions). So if T ⊢ Con(T), then T ⊢ G_T by modus ponens, contradicting the first theorem.

Q: What is the diagonal lemma? A: For any formula φ(x) of arithmetic with one free variable, there exists a sentence G such that PA ⊢ G ↔ φ(⌜G⌝). In words: G provably satisfies φ of its own Gödel number. The proof constructs G by substituting the code of a formula into itself, exploiting the primitive-recursive representability of substitution.

Q: How does Gödel relate to Turing’s Halting Problem? A: Both use diagonal self-reference. Turing constructs D such that D(M) does the opposite of what M does on its own description, then runs D(D) for a contradiction; Gödel constructs G that says “G is not provable,” then asks whether G is provable. Both prove a negative result about formal systems/algorithms. In fact, the set of true arithmetical sentences is recursively enumerable but undecidable — formally equivalent in difficulty to the Halting Problem.

References