Theoria

A natural companion to the essay on Gentzen’s consistency proof, exploring how incompleteness shapes our understanding of mathematical truth and provability.

Contents

---

I. Introduction

In 1930, the mathematical world gathered in Königsberg for a conference on the epistemology of the exact sciences. The mood was optimistic—perhaps triumphalist. David Hilbert, the towering figure of early twentieth-century mathematics, had articulated a programme that promised to secure mathematics on unshakeable foundations: formalise all of mathematics within rigorous axiomatic systems, then prove—using only finitary, combinatorial methods—that these systems are consistent. Mathematics would thereby be rendered immune to paradox, its truths guaranteed by the very structure of formal proof itself.

On the final day of that conference, a young Austrian logician named Kurt Gödel rose to make a brief remark. What he announced—almost parenthetically—would fundamentally alter our understanding of mathematical knowledge. He had discovered that any sufficiently powerful formal system capable of expressing basic arithmetic must, if consistent, contain statements that cannot be proved within the system. Moreover, such a system cannot prove its own consistency.

These results, published the following year as “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme,”¹ constitute what we now call the First and Second Incompleteness Theorems. They represent not merely technical achievements in mathematical logic but profound philosophical discoveries about the nature of mathematical truth, the limits of formal reasoning, and the relationship between syntax and semantics.

I.1 The two theorems (informal statement)

First Incompleteness Theorem: Any consistent formal system F capable of expressing basic arithmetic contains a sentence G such that F ⊬ G. If F is additionally ω-consistent, then F ⊬ ¬G, so that G is undecidable in F. Hence (under ω-consistency) F is incomplete.

Second Incompleteness Theorem: Any consistent formal system F capable of expressing basic arithmetic cannot prove its own consistency—that is, F ⊬ Con(F).

The distinction between truth and provability emerges here with startling clarity. A sentence can be true in the intended model—hold in the standard interpretation of the formal language—yet remain forever beyond the reach of formal derivation within the system. This gap between semantic truth and syntactic proof lies at the heart of incompleteness and carries implications that reverberate through philosophy of mathematics, epistemology, and even philosophy of mind.

I.2 Connection to Gentzen’s consistency proof

In the companion essay to this one, we examined Gerhard Gentzen’s 1936 proof that Peano Arithmetic is consistent.² How can Gentzen have proved what Gödel showed to be unprovable? The answer illuminates the Second Incompleteness Theorem beautifully: Gentzen’s proof employs transfinite induction up to the ordinal ε₀—a principle that cannot itself be justified within PA. Gentzen did not circumvent Gödel’s result; he illustrated it. To prove the consistency of a formal system, one must ascend to a stronger system, initiating an infinite hierarchy of ever-more-powerful formal theories. This hierarchical structure—forced upon us by the Second Theorem—reveals that mathematical knowledge cannot be captured within any single formal framework but extends upward without bound.

II. Formal prerequisites

Before presenting Gödel’s constructions, we must establish the formal apparatus within which they operate.

II.1 First-order formal systems

A first-order formal system F consists of:

Language ℒ — A first-order language with logical symbols (¬, ∧, ∨, →, ↔, ∀, ∃, =), variables (x₀, x₁, x₂, …), and non-logical symbols (constants, function symbols, predicate symbols) specific to the theory. Axioms — A decidable set of sentences in ℒ designated as axioms. These include logical axioms (governing the behaviour of logical connectives and quantifiers) and non-logical axioms (specific to the mathematical theory being formalised). Rules of Inference — A finite set of syntactic rules permitting the derivation of new sentences from existing ones. Typically, these include modus ponens (from φ and φ → ψ, infer ψ) and generalisation (from φ, infer ∀x φ, under appropriate restrictions).

A proof in F is a finite sequence of sentences, each of which is either an axiom or follows from earlier sentences by a rule of inference. A sentence φ is provable in F (written F ⊢ φ or simply ⊢ φ when F is clear from context) if there exists a proof whose final sentence is φ.

II.2 Key definitions

Consistency — F is consistent if there is no sentence φ such that both F ⊢ φ and F ⊢ ¬φ. Completeness — F is complete if for every sentence φ in ℒ, either F ⊢ φ or F ⊢ ¬φ. Soundness — F is sound with respect to a model ℳ if every theorem of F is true in ℳ. ω-consistency — F is ω-consistent if there is no formula φ(x) such that F ⊢ ∃x ¬φ(x) while simultaneously F ⊢ φ(n̄) for every natural number n.

The notion of ω-consistency was introduced by Gödel in his 1931 paper. It is stronger than mere consistency and ensures a certain harmony between the system and the standard model.³

II.3 Peano Arithmetic (PA)

The canonical example of a “sufficiently strong” formal system is first-order Peano Arithmetic, denoted PA. Its language $ℒ_{PA}$ contains: a constant symbol 0, a unary function symbol S (successor), and binary function symbols + and · (addition and multiplication).⁴

The Axioms of PA:

Equality Axioms:
(1) ∀x (x = x)
(2) ∀x ∀y (x = y → y = x)
(3) ∀x ∀y ∀z (x = y ∧ y = z → x = z)
(4) Substitution axioms for each function and predicate symbol

Successor Axioms:
(5) ∀x (S(x) ≠ 0)
(6) ∀x ∀y (S(x) = S(y) → x = y)

Addition Axioms:
(7) ∀x (x + 0 = x)
(8) ∀x ∀y (x + S(y) = S(x + y))

Multiplication Axioms:
(9) ∀x (x · 0 = 0)
(10) ∀x ∀y (x · S(y) = x · y + x)

Induction Schema:
(11) [φ(0) ∧ ∀x (φ(x) → φ(S(x)))] → ∀x φ(x)

What enables self-reference in Gödel’s construction is that the theory is effectively axiomatised and can represent enough computable (primitive recursive) syntactic relations—Gödel coding, the proof predicate, and the diagonal “substitution” function. Full induction is not the key ingredient here; much weaker arithmetics (such as Robinson Arithmetic Q, which lacks induction entirely) already suffice for coding syntax and obtaining the basic incompleteness results.

II.4 Primitive recursive and general recursive functions

Gödel’s arithmetisation depends on the fact that certain syntactic operations—checking whether a string is a well-formed formula, substituting terms, verifying proofs—are computable and, more specifically, primitive recursive.

The class of primitive recursive functions is the smallest class of functions ℕᵏ → ℕ containing the basic functions and closed under composition and primitive recursion:⁵

Basic Functions:
(1) Zero function: Z(x) = 0
(2) Successor function: S(x) = x + 1
(3) Projection functions: Pᵢᵏ(x₁, …, xₖ) = xᵢ

Closure Operations:
(4) Composition
(5) Primitive Recursion

The broader class of general recursive functions (equivalently, Turing-computable functions) extends primitive recursive functions by allowing unbounded minimisation. The provability predicate “there exists a proof of φ” involves an existential quantifier over all possible proofs—potentially unbounded—and hence the provability predicate is only general recursive, not primitive recursive.⁶

Theorem (Representability): Every primitive recursive function is representable in PA. More generally, every general recursive function is representable in PA.⁷

This theorem—whose proof requires careful work with the axioms of PA—is essential to Gödel’s construction. It guarantees that PA can “see” its own syntactic operations when they are coded as arithmetic relations.

III. Gödel numbering and arithmetisation of syntax

Gödel’s stroke of genius was to realise that syntax—the structure of formal expressions and proofs—can itself be encoded as arithmetic. By assigning unique natural numbers to symbols, terms, formulas, and proofs, we can express metamathematical statements about PA within PA.

III.1 The coding scheme

We assign Gödel numbers to the basic symbols of $ℒ_{PA}$:⁸

Symbol	Gödel Number
0	1
S	3
+	5
·	7
=	9
¬	11
∧	13
∨	15
→	17
∀	19
∃	21
(	23
)	25
,	27
xᵢ	29 + 2i

III.2 Sequence coding via prime powers

To encode finite sequences of numbers, we use the fundamental theorem of arithmetic. The sequence ⟨a₁, a₂, …, aₙ⟩ is coded by:

⌜a₁, a₂, …, aₙ⌝ = p₁^(a₁+1) · p₂^(a₂+1) · … · pₙ^(aₙ+1)

where pᵢ denotes the i-th prime. Adding 1 to each exponent ensures we can distinguish, e.g., ⟨0, 2⟩ from ⟨2⟩. The empty sequence is coded by 1.

Notation: We write ⌜φ⌝ for the Gödel number of expression φ, and n̄ for the numeral representing n in PA (i.e., S(S(⋯S(0)⋯)) with n applications of S).

III.3 Key primitive recursive predicates and functions

We define the primitive recursive predicates and functions that PA can represent:

Term(x) — “x is the Gödel number of a term”
Form(x) — “x is the Gödel number of a formula”
Sent(x) — “x is the Gödel number of a sentence”
Sub(x, y, z) — the Gödel number of φ[t/v]
Proof(x, y) — “x codes a proof of the formula coded by y”

The provability predicate is defined as:⁹

Prov(y) ≡ ∃x Proof(x, y)

This predicate—”there exists a proof of the formula coded by y”—is Σ₁: it has the form ∃x R(x, y) where R is primitive recursive.¹⁰

IV. The fixed-point lemma and the Gödel sentence

We now arrive at the technical heart of Gödel’s construction: the Diagonal Lemma, which enables the construction of self-referential sentences.

IV.1 The Diagonal Lemma (fixed-point theorem)

Theorem (Diagonal Lemma): For any formula φ(x) with one free variable x, there exists a sentence ψ such that:¹¹

PA ⊢ ψ ↔ φ(⌜ψ⌝̄)

In other words, ψ is provably equivalent to the statement “φ holds of my own Gödel number.” This is the formalisation of self-reference.

IV.2 Proof of the Diagonal Lemma

Define the diagonal function d: ℕ → ℕ by:

d(n) = Sub(n, ⌜x₀⌝, num(n))

where num(n) is the Gödel number of the numeral n̄. Intuitively, if n = ⌜θ(x₀)⌝ for some formula θ(x₀) with free variable x₀, then d(n) = ⌜θ(n̄)⌝—the Gödel number of θ applied to its own Gödel number.

Since Sub and num are primitive recursive, so is d. Let δ(x, y) be a formula representing d in PA. Now let φ(x) be any formula. Define:

θ(x₀) ≡ ∃y (δ(x₀, y) ∧ φ(y))

Let n = ⌜θ(x₀)⌝, and define ψ ≡ θ(n̄). The proof that PA ⊢ ψ ↔ φ(⌜ψ⌝̄) follows from the representability of d: since d(n) = ⌜ψ⌝, we have PA ⊢ δ(n̄, ⌜ψ⌝̄), and hence ψ ↔ ∃y (δ(n̄, y) ∧ φ(y)) ↔ φ(⌜ψ⌝̄). □

IV.3 Construction of the Gödel sentence

Apply the Diagonal Lemma to the formula ¬Prov(x). We obtain a sentence G such that:

PA ⊢ G ↔ ¬Prov(⌜G⌝̄)

Unpacking this: G is provably equivalent to the assertion “the formula with Gödel number ⌜G⌝ is not provable.” In other words, G says of itself that it is not provable.

This is the formalisation of the Liar Paradox—but with a crucial twist. The Liar sentence “This sentence is false” leads to paradox because truth is bivalent and we cannot consistently assign it a truth value. The Gödel sentence “This sentence is not provable” does not lead to paradox because provability and truth can diverge. G can be true (because it genuinely has no proof) without being provable. The incompleteness theorems reveal exactly this divergence.

V. The First Incompleteness Theorem

We now prove Gödel’s First Theorem in detail.

V.1 Formal statement

Theorem (First Incompleteness Theorem): Let PA be Peano Arithmetic and let G be the Gödel sentence constructed above (satisfying PA ⊢ G ↔ ¬Prov(⌜G⌝̄)). Then: (1) If PA is consistent, then PA ⊬ G. (2) If PA is ω-consistent, then PA ⊬ ¬G. Hence, under ω-consistency, G is undecidable in PA and PA is incomplete.

V.2 Proof

Let G be the Gödel sentence constructed above, satisfying PA ⊢ G ↔ ¬Prov(⌜G⌝̄).

Part 1: If PA is consistent, then PA ⊬ G.

1. Suppose PA ⊢ G [Assumption for reductio]
2. Then ∃n: Proof(n, ⌜G⌝) [There exists a proof]
3. PA ⊢ Proof(n̄, ⌜G⌝̄) [Representability]
4. PA ⊢ ∃x Proof(x, ⌜G⌝̄) [Existential generalisation]
5. PA ⊢ Prov(⌜G⌝̄) [Definition of Prov]
6. PA ⊢ G → ¬Prov(⌜G⌝̄) [Fixed-point equivalence]
7. PA ⊢ ¬Prov(⌜G⌝̄) [Modus ponens from 1, 6]
8. PA ⊢ Prov(⌜G⌝̄) ∧ ¬Prov(⌜G⌝̄) [Contradiction: 5, 7]
9. PA is inconsistent [From 8]
10. ∴ If PA is consistent, PA ⊬ G [Contraposition] □

Part 2: If PA is ω-consistent, then PA ⊬ ¬G.

1. Suppose PA ⊢ ¬G [Assumption for reductio]
2. PA ⊢ Prov(⌜G⌝̄) [Fixed-point equivalence]
3. PA ⊢ ∃x Proof(x, ⌜G⌝̄) [Definition of Prov]
4. By Part 1, PA ⊬ G [ω-consistency implies consistency]
5. In ℕ, no proof of G exists [From 4]
6. For all n ∈ ℕ: PA ⊢ ¬Proof(n̄, ⌜G⌝̄) [Representability]
7. PA ⊢ ∃x Proof(x, ⌜G⌝̄) and [From 3]
PA ⊢ ¬Proof(n̄, ⌜G⌝̄) for each n [From 6]
8. This violates ω-consistency [Definition]
9. ∴ If PA is ω-consistent, PA ⊬ ¬G [Contraposition] □

Corollary: If PA is ω-consistent, then G is undecidable in PA (neither provable nor refutable), and hence PA is incomplete.

On truth: If we additionally assume that PA is sound with respect to the standard model ℕ, then G is true in ℕ. For soundness implies consistency, so PA ⊬ G by Part 1, meaning no proof of G exists. Hence ¬Prov(⌜G⌝) holds in ℕ. Since G ↔ ¬Prov(⌜G⌝̄) is provable in PA and hence true in ℕ, G itself is true in ℕ.

VI. The Second Incompleteness Theorem

The First Theorem tells us that PA cannot prove all truths. The Second Theorem tells us something more devastating: PA cannot even prove the consistency claim that would justify confidence in its own theorems.

VI.1 The formal consistency statement

Define:

Con(PA) ≡ ¬Prov(⌜0 = 1⌝̄)

This says: “The formula 0 = 1 is not provable.” Meta-theoretically (in the intended interpretation over ℕ), PA is consistent if and only if ℕ ⊨ Con(PA). In nonstandard models, internal “proof” predicates can behave non-intuitively due to “proofs” of nonstandard length, so the equivalence between Con(PA) and “PA is consistent” is being stated in the usual meta-theoretic sense about the intended model.¹³

VI.2 Hilbert–Bernays–Löb derivability conditions

The proof of the Second Theorem requires that the provability predicate Prov(x) satisfies certain formal properties, known as the Hilbert–Bernays–Löb derivability conditions:¹⁴

D1. If PA ⊢ φ, then PA ⊢ Prov(⌜φ⌝̄)

D2. PA ⊢ Prov(⌜φ → ψ⌝̄) → (Prov(⌜φ⌝̄) → Prov(⌜ψ⌝̄))

D3. PA ⊢ Prov(⌜φ⌝̄) → Prov(⌜Prov(⌜φ⌝̄)⌝̄)

Interpretation: D1 says that PA “knows” what it proves: whenever PA actually proves φ, it also proves that it proves φ. D2 says that PA recognises the closure of provability under modus ponens. D3 says that provability is “provably self-aware”: if something is provable, then the fact of its provability is itself provable.

Important caveat: D1–D3 govern what happens when PA actually proves formulas. They do not allow one to infer Prov(⌜ψ⌝) merely from assuming ψ as a hypothesis in an object-level derivation. This distinction between “PA proves ψ” (a meta-level fact) and “ψ appears as a hypothesis” (an object-level assumption) is crucial for correct reasoning about the Second Theorem.

VI.3 Proof of the Second Theorem

Theorem (Second Incompleteness Theorem): If PA is consistent, then PA ⊬ Con(PA).

Proof Sketch: Using the Hilbert–Bernays–Löb derivability conditions for Prov(·), one can formalise the reasoning of Part 1 of the First Incompleteness Theorem inside PA. Specifically, one shows:

PA ⊢ Con(PA) → G

The verification that PA can internalise the meta-argument is technically demanding—it requires carefully checking that each step of the Part 1 proof can be carried out using only D1, D2, D3 and basic logical manipulations within PA. Hilbert and Bernays provided this verification in detail in Grundlagen der Mathematik.¹⁵

Given PA ⊢ Con(PA) → G: suppose PA ⊢ Con(PA). Then by modus ponens, PA ⊢ G. But by the First Incompleteness Theorem, if PA is consistent, then PA ⊬ G. Contradiction. Therefore, if PA is consistent, PA ⊬ Con(PA). □

VII. Connection to Gentzen’s consistency proof

In the companion essay, we examined Gentzen’s 1936 proof in detail. Let us now see how it illustrates the Second Incompleteness Theorem with precision.

VII.1 Gentzen’s result

Gentzen proved:¹⁶

PRA + TI(ε₀) ⊢ Con(PA)

where PRA is Primitive Recursive Arithmetic and TI(ε₀) denotes transfinite induction up to the ordinal ε₀ = ω^ω^ω^···.

VII.2 The critical point

The essential observation: TI(ε₀) is not provable in PA. Indeed, PA proves transfinite induction for each ordinal α < ε₀, but PA cannot prove transfinite induction for ε₀ itself. This follows from the Second Theorem—if PA could prove TI(ε₀), it could prove its own consistency, contradicting the theorem.

Thus Gentzen’s proof does not refute Gödel; it confirms him. The Second Theorem tells us consistency proofs must use methods beyond the system being analysed. Gentzen’s proof shows exactly what “beyond” looks like for PA: we must ascend to ε₀ in the ordinal hierarchy.

VII.3 The infinite hierarchy

This initiates an infinite regress—or, more optimistically, an infinite progression. The system PA + TI(ε₀) can prove Con(PA), but it cannot prove its own consistency. To prove that, we would need transfinite induction up to some ordinal α > ε₀. And so on, without end.¹⁷

VIII. Philosophical implications

VIII.1 Truth transcends provability

For PA, assuming consistency, the Gödel sentence G is unprovable in PA. If we further assume that PA is sound with respect to ℕ (or equivalently, Σ₁-sound), then G is true in ℕ. More generally, incompleteness yields unprovability; calling the sentence “true” requires specifying an intended model or adding a soundness assumption. This is not a defect of our particular formal system but a structural feature of any sufficiently strong consistent system when interpreted over its intended structure.

Gödel himself drew Platonist conclusions from this. In his 1951 Gibbs Lecture, he stated:

“Either mathematics is incompletable in this sense, that its evident axioms can never be comprised in a finite rule, that is to say, the human mind (even within the realm of pure mathematics) infinitely surpasses the powers of any finite machine, or else there exist absolutely unsolvable diophantine problems.”¹⁸

And more explicitly:

“The notion of mathematical truth cannot be reduced to formal provability… But, if it were true that there exist number-theoretic questions undecidable for the human mind, it would mean that the human mind is utterly irrational in asking questions it cannot answer, while asserting emphatically that only reason can answer them. This seems unlikely. So the Platonistic view seems to be the only one tenable.”¹⁹

VIII.2 The collapse of strict formalism

Hilbert’s programme envisioned mathematics as a purely formal game—manipulation of symbols according to syntactic rules, justified by finitary consistency proofs. Gödel’s theorems shatter this vision.

If mathematics were merely formal symbol manipulation, then mathematical truth would reduce to provability. But the First Theorem shows this reduction fails: there are truths (in the intended model) that no amount of rule-following will uncover. Moreover, the Second Theorem undermines the formalist’s justification strategy. The formalist wanted to secure confidence in mathematical reasoning by proving consistency formalistically. But the very systems we most want to justify are precisely those that cannot be self-justifying.

Gödel commented on this in his 1951 lecture:

“It is this theorem [the Second Incompleteness Theorem] which makes the incompletability of mathematics particularly evident. For, it makes it impossible that someone should set up a certain well-defined system of axioms and rules and consistently make the following assertion about it: All of these axioms and rules I perceive (with mathematical certitude) to be correct, and moreover I believe that they contain all of mathematics.”²⁰

VIII.3 Epistemological questions

How, then, do we access mathematical truths beyond formal proof? Several options present themselves:

Mathematical Intuition: We grasp the truth of the Gödel sentence not by deriving it formally but by understanding what it says. Recognising that PA is consistent and sound, we recognise that G is true in ℕ.

Axiom Extension: We can extend PA by adding new axioms—such as Con(PA) or transfinite induction principles—that capture truths inaccessible to the original system. This is the Gentzen strategy generalised.

Reflection Principles: We can add “reflection principles” asserting that everything provable is true. Such principles allow systems to recognise truths about their own theorems.²¹

VIII.4 Undecidability in mathematics

The Gödel sentence is a somewhat artificial construction—it was designed to be undecidable. But incompleteness extends to natural mathematical questions.

The Continuum Hypothesis (CH)—Cantor’s conjecture that there is no set whose cardinality lies strictly between that of the integers and the real numbers—was shown by Gödel (1940) to be consistent with ZFC set theory and by Cohen (1963) to be independent: neither CH nor its negation is provable in ZFC.²²

The Paris–Harrington theorem (1977) provides an example from “ordinary” combinatorics: a strengthening of the finite Ramsey theorem that is true in ℕ but unprovable in PA.²³

Goodstein’s theorem concerns sequences of natural numbers defined by a simple arithmetic procedure: every such sequence eventually reaches zero. This is provable using ordinals (specifically, induction up to ε₀) but not in PA.²⁴

VIII.5 The Lucas–Penrose argument

The philosopher John Lucas (1961) and physicist Roger Penrose (1989, 1994) argued that Gödel’s theorems demonstrate that human mathematical reasoning cannot be captured by any algorithm or formal system.²⁵ The argument has been extensively criticised—notably, that we cannot know our own consistency, and that the argument concerns idealised reasoners rather than finite, fallible humans.²⁶

Gödel himself was sympathetic to anti-mechanist conclusions but remained cautious:

“My theorems only show that the mechanization of mathematics, i.e., the elimination of the mind and of abstract entities, is impossible, if one wants to have a satisfactory foundation and target of mathematics. The mind, in its use, is not static, but constantly developing.”²⁷

VIII.6 The humility of reason

Perhaps the deepest philosophical lesson of incompleteness is a kind of intellectual humility. No formal system—however powerful, however carefully designed—can capture all mathematical truth or certify its own reliability. This is not scepticism. We have excellent reasons to believe PA is consistent; Gentzen’s proof provides one, and the coherence of our mathematical practice provides another. But our confidence cannot be formalised within the systems themselves.

Gödel expressed this beautifully:

“The formation of ever higher types… continues into the transfinite… There is nothing to prevent a being with an unlimited lifespan from discovering all the axioms one after another and thus eventually knowing them all. But no finite rule can replace this infinite process.”²⁸

Conclusion

Gödel’s Incompleteness Theorems stand among the greatest achievements of twentieth-century thought—not merely as technical results in mathematical logic but as profound revelations about the nature of mathematical knowledge.

The First Theorem shows that truth and provability diverge: in any sufficiently strong consistent formal system, there exist sentences unprovable in that system which are true in the intended model. The Second Theorem shows that consistency cannot be self-certified: the very systems we most want to trust cannot prove their own trustworthiness. Together, they demolish naive formalism and reveal the essential openness of mathematics.

Yet incompleteness is not cause for despair. Gentzen’s consistency proof exemplifies the constructive response: what cannot be proved within a system can be proved by ascending to a stronger one. The hierarchy of formal systems—each level justifying those below—mirrors the stratified nature of mathematical knowledge. We ascend from PA to PA + Con(PA), from arithmetic to set theory, from set theory to large cardinal axioms. Each step extends our reach while preserving rigour.

Mathematical truth, it seems, is inexhaustible. No single system contains it all; no finite procedure captures it. This is not a limitation to lament but a horizon to explore. As Gödel showed, the incompleteness of formal systems reflects the boundlessness of mathematical reality—a reality we approach asymptotically through ever-more-powerful methods, never completing the journey, always advancing.

The theorems invite a response of wonder rather than discouragement. They reveal mathematics as a living discipline, perpetually transcending its current bounds, propelled forward by the very limitations Gödel uncovered. Incompleteness is not the end of the Hilbert programme but its transformation: not a secure foundation once and for all, but an endless ascent into mathematical understanding.

---

For the constructive response to incompleteness—Gentzen’s remarkable proof that PA is consistent using transfinite induction—see the companion essay “Gentzen’s Consistency Proof for Peano Arithmetic: Ordinal Analysis and the Constructive Foundations of Mathematics.”

Selected references

Boolos, George, and Richard Jeffrey. Computability and Logic. 5th ed., with John Burgess. Cambridge: Cambridge University Press, 2007.

Franzén, Torkel. Gödel’s Theorem: An Incomplete Guide to Its Use and Abuse. Wellesley, MA: A K Peters, 2005.

Gödel, Kurt. “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I.” Monatshefte für Mathematik und Physik 38 (1931): 173–198.

Gödel, Kurt. “Some Basic Theorems on the Foundations of Mathematics and Their Implications” (Gibbs Lecture, 1951). In Solomon Feferman et al., eds., Kurt Gödel: Collected Works, vol. 3. Oxford: Oxford University Press, 1995.

Nagel, Ernest, and James R. Newman. Gödel’s Proof. Revised edition. New York: New York University Press, 2001.

Raatikainen, Panu. “Gödel’s Incompleteness Theorems.” Stanford Encyclopedia of Philosophy. https://plato.stanford.edu/entries/goedel-incompleteness/.

Smith, Peter. An Introduction to Gödel’s Theorems. 2nd ed. Cambridge: Cambridge University Press, 2013.

Smullyan, Raymond. Gödel’s Incompleteness Theorems. Oxford: Oxford University Press, 1992.

Wang, Hao. Reflections on Kurt Gödel. Cambridge, MA: MIT Press, 1987.

1. Kurt Gödel, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I,” Monatshefte für Mathematik und Physik 38 (1931): 173–198. English translation in Jean van Heijenoort, ed., From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931 (Cambridge, MA: Harvard University Press, 1967), 596–616. ↩
2. Gerhard Gentzen, “Die Widerspruchsfreiheit der reinen Zahlentheorie,” Mathematische Annalen 112 (1936): 493–565. English translation: “The Consistency of Elementary Number Theory,” in M. E. Szabo, ed., The Collected Papers of Gerhard Gentzen (Amsterdam: North-Holland, 1969), 132–213. ↩
3. The notion of ω-consistency was introduced by Gödel in his 1931 paper. For a detailed discussion, see Peter Smith, An Introduction to Gödel’s Theorems, 2nd ed. (Cambridge: Cambridge University Press, 2013), 155–160. ↩
4. For a comprehensive treatment of Peano Arithmetic and its axiomatisation, see Richard Kaye, Models of Peano Arithmetic (Oxford: Oxford University Press, 1991), chapters 1–2. ↩
5. The theory of primitive recursive functions was developed by Gödel in his 1931 paper and systematised by Rózsa Péter in Recursive Functions (New York: Academic Press, 1967). ↩
6. See Stephen Cole Kleene, Introduction to Metamathematics (Amsterdam: North-Holland, 1952), chapters 9–11, for the definitive treatment of recursive function theory. ↩
7. The representability theorem is proved in detail in Elliott Mendelson, Introduction to Mathematical Logic, 6th ed. (Boca Raton: CRC Press, 2015), chapter 3. ↩
8. Gödel’s original coding used a somewhat different scheme. The presentation here follows the simplified version in Raymond Smullyan, Gödel’s Incompleteness Theorems (Oxford: Oxford University Press, 1992), 25–35. ↩
9. For the detailed construction of the proof predicate as primitive recursive, see George Boolos and Richard Jeffrey, Computability and Logic, 5th ed., with John Burgess (Cambridge: Cambridge University Press, 2007), chapter 15. ↩
10. The proof of representability for primitive recursive functions is given in full detail in Smith, An Introduction to Gödel’s Theorems, chapters 13–15. ↩
11. The Diagonal Lemma was implicit in Gödel’s 1931 paper and made explicit by Rudolf Carnap in Logical Syntax of Language (London: Kegan Paul, 1937). See also Smullyan, Gödel’s Incompleteness Theorems, 44–48. ↩
12. J. Barkley Rosser, “Extensions of Some Theorems of Gödel and Church,” Journal of Symbolic Logic 1 (1936): 87–91. ↩
13. The equivalence between Con(PA) and PA’s consistency holds in the standard model ℕ. In nonstandard models, the internal provability predicate may witness “proofs” of nonstandard length. For a careful treatment, see Smith, An Introduction to Gödel’s Theorems, chapter 25. ↩
14. The derivability conditions were formulated by David Hilbert and Paul Bernays in Grundlagen der Mathematik, vol. 2 (Berlin: Springer, 1939) and refined by Martin Hugo Löb in “Solution of a Problem of Leon Henkin,” Journal of Symbolic Logic 20 (1955): 115–118. ↩
15. For a thorough analysis of the impact of the Second Theorem on Hilbert’s programme and the detailed verification of the internalised argument, see Richard Zach, “Hilbert’s Program Then and Now,” in Dale Jacquette, ed., Philosophy of Logic (Amsterdam: North-Holland, 2007), 411–447. ↩
16. Gentzen, “Die Widerspruchsfreiheit der reinen Zahlentheorie.” For modern expositions, see Gaisi Takeuti, Proof Theory, 2nd ed. (Amsterdam: North-Holland, 1987), and Wolfram Pohlers, Proof Theory: The First Step into Impredicativity (Berlin: Springer, 2009). ↩
17. The ordinal analysis of formal systems and the resulting hierarchy is treated comprehensively in Michael Rathjen, “The Realm of Ordinal Analysis,” in S. Barry Cooper and John K. Truss, eds., Sets and Proofs (Cambridge: Cambridge University Press, 1999), 219–279. ↩
18. Kurt Gödel, “Some Basic Theorems on the Foundations of Mathematics and Their Implications” (Gibbs Lecture, 1951), in Solomon Feferman et al., eds., Kurt Gödel: Collected Works, vol. 3 (Oxford: Oxford University Press, 1995), 304–323, at 310. ↩
19. Gödel, “Some Basic Theorems,” 311–312. ↩
20. Gödel, “Some Basic Theorems,” 309. ↩
21. For reflection principles and their role in extending formal systems, see Solomon Feferman, “Transfinite Recursive Progressions of Axiomatic Theories,” Journal of Symbolic Logic 27 (1962): 259–316. ↩
22. Kurt Gödel, The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis with the Axioms of Set Theory (Princeton: Princeton University Press, 1940); Paul Cohen, “The Independence of the Continuum Hypothesis,” Proceedings of the National Academy of Sciences 50 (1963): 1143–1148, and 51 (1964): 105–110. ↩
23. Jeff Paris and Leo Harrington, “A Mathematical Incompleteness in Peano Arithmetic,” in Jon Barwise, ed., Handbook of Mathematical Logic (Amsterdam: North-Holland, 1977), 1133–1142. ↩
24. Reuben Louis Goodstein, “On the Restricted Ordinal Theorem,” Journal of Symbolic Logic 9 (1944): 33–41. The unprovability in PA was established by Laurence Kirby and Jeff Paris, “Accessible Independence Results for Peano Arithmetic,” Bulletin of the London Mathematical Society 14 (1982): 285–293. ↩
25. John Lucas, “Minds, Machines, and Gödel,” Philosophy 36 (1961): 112–127; Roger Penrose, The Emperor’s New Mind (Oxford: Oxford University Press, 1989); Roger Penrose, Shadows of the Mind (Oxford: Oxford University Press, 1994). ↩
26. For a detailed critique of the Lucas–Penrose argument, see Solomon Feferman, “Penrose’s Gödelian Argument,” Psyche 2 (1995): 21–32; and Stewart Shapiro, “Incompleteness, Mechanism, and Optimism,” Bulletin of Symbolic Logic 4 (1998): 273–302. ↩
27. From a letter to Hao Wang, quoted in Hao Wang, A Logical Journey: From Gödel to Philosophy (Cambridge, MA: MIT Press, 1996), 186. ↩
28. Kurt Gödel, “Russell’s Mathematical Logic” (1944), in Feferman et al., Kurt Gödel: Collected Works, vol. 2 (Oxford: Oxford University Press, 1990), 119–141, at 140–141. ↩