Gödel's incompleteness theorems

Theorem

Gödel's incompleteness theorems

T-130Home MU-403Threads logic

Statement

Let \(T\) be a formal theory in the language of arithmetic (or any language interpreting it) such that (i) \(T\) is recursively axiomatised — the set of axioms of \(T\) is decidable by an algorithm — and (ii) \(T\) is consistent, and (iii) \(T\) proves Robinson arithmetic \(Q\) (in particular \(T\) proves the basic recursive facts about \(+\), \(\times\), and \(\lt\) needed to represent every recursive function). Write \(\mathrm{Con}(T)\) for the arithmetised statement "\(T\) is consistent", a specific sentence of arithmetic built from a fixed Gödel coding of proofs. Then: First Incompleteness Theorem. There is a sentence \(G_T\) in the language of \(T\) such that \(T \nvdash G_T\) and \(T \nvdash \neg G_T\); moreover if \(T\) is \(\omega\)-consistent then \(G_T\) is true in the standard model \(\mathbb{N}\). Second Incompleteness Theorem. If \(T\) additionally satisfies the Hilbert–Bernays–Löb derivability conditions (so that its provability predicate behaves provably like a provability predicate), then \(T \nvdash \mathrm{Con}(T)\), unless \(T\) is inconsistent.

Why it matters

This pair of theorems, proved by Gödel in 1931, ended Hilbert's programme of finding a single finitary, mechanically checkable axiom system from which every arithmetical truth could be derived and whose own consistency could be verified by elementary means. No such system exists once it is strong enough to talk about its own syntax: strength and completeness cannot coexist, and strength and self-verifying consistency cannot coexist either.

The theorems are not a curiosity about arithmetic alone. Because Robinson arithmetic \(Q\) is interpretable in an enormous range of theories — set theory, most of algebra and analysis formalised axiomatically, theories of computation — the incompleteness phenomenon infects essentially every sufficiently expressive formal system used in mathematics, and underlies deep results in computability theory (the halting problem), theoretical computer science (undecidability of program verification), and the philosophy of mind and formal epistemology.

Hypotheses

Recursive axiomatisability.Counterexample: let \(T^*\) = the (non-recursively-enumerable) theory of all true arithmetical sentences, "true arithmetic". \(T^*\) is complete by definition — every sentence or its negation is a theorem — because there is no algorithm generating exactly its axioms, so the proof of \(G_T\) (which needs to enumerate proofs mechanically) cannot even get started. Consistency.An inconsistent theory proves every sentence, including \(G_T\), \(\neg G_T\), and \(\mathrm{Con}(T)\) itself; the theorems are vacuous/false-hypothesis for inconsistent \(T\), which is why both theorems carry "unless \(T\) is inconsistent" as an explicit escape clause. Interprets \(Q\) (sufficient arithmetical strength).Counterexample: Presburger arithmetic (the theory of \(\langle \mathbb{N}, + \rangle\) without multiplication) is recursively axiomatised, consistent, and complete — every sentence in its language is decided — because it cannot represent multiplication and hence cannot carry out the self-referential coding Gödel's proof needs. Derivability conditions (for the Second Theorem specifically).The First Theorem needs only a representability lemma, but the Second needs the provability predicate \(\mathrm{Prov}_T(x)\) to satisfy D1 \(T \vdash \varphi \Rightarrow T \vdash \mathrm{Prov}_T(\ulcorner\varphi\urcorner)\), D2 \(T \vdash \mathrm{Prov}_T(\ulcorner\varphi\to\psi\urcorner) \to (\mathrm{Prov}_T(\ulcorner\varphi\urcorner)\to \mathrm{Prov}_T(\ulcorner\psi\urcorner))\), D3 \(T \vdash \mathrm{Prov}_T(\ulcorner\varphi\urcorner) \to \mathrm{Prov}_T(\ulcorner \mathrm{Prov}_T(\ulcorner\varphi\urcorner)\urcorner)\). Rosser-style constructions can sometimes weaken what is needed for the first theorem alone, but dropping D3 breaks the second theorem's proof: there exist "provability-like" predicates satisfying only D1–D2 for which self-consistency IS provable (Rosser provability variants), showing D3 is not decorative.

Proof

\text{Fix a Gödel numbering } \ulcorner \varphi \urcorner \in \mathbb{N} \text{ of formulas/proofs of } T.

Standard primitive-recursive coding of finite syntactic objects as natural numbers (e.g. via prime-power codes); the coding and decoding maps, and the "is a well-formed proof" predicate, are primitive recursive. A

\mathrm{Prf}_T(p,x) :\Leftrightarrow p \text{ codes a } T\text{-proof of the formula coded by } x

\(\mathrm{Prf}_T\) is a primitive recursive relation because checking each line of a proof against the (decidable, by hypothesis i) axiom/rule list is itself primitive recursive. A

\text{(Representability Lemma) Every recursive relation } R \subseteq \mathbb{N}^k \text{ is represented in } T \text{ by a formula } \rho_R(x_1,\dots,x_k):\newline n_1,\dots,n_k \in R \Rightarrow T \vdash \rho_R(\bar n_1,\dots,\bar n_k), \quad n_1,\dots,n_k \notin R \Rightarrow T \vdash \neg\rho_R(\bar n_1,\dots,\bar n_k)

This is the key technical import: because \(T \vdash Q\) and \(Q\) already represents every recursive function/relation (a theorem proved by induction on the Kleene normal-form / primitive-recursion generating clauses of recursive functions), \(T\) inherits representability of \(\mathrm{Prf}_T\) in particular. Cited as a lemma rather than reproved here — its proof is a routine but lengthy induction over the class of recursive functions. C

\mathrm{Prov}_T(x) :\equiv \exists p\, \rho_{\mathrm{Prf}_T}(p,x)

Definition of the provability predicate, obtained by existentially quantifying out the proof-witness from the representing formula of step 3. A

\text{(Diagonal / Fixed-Point Lemma) For any formula } \psi(x) \text{ with one free variable there is a sentence } \delta \text{ with } T \vdash \delta \leftrightarrow \psi(\ulcorner \delta \urcorner).

Proved by the diagonal construction: let \(\mathrm{diag}(n)\) be the (primitive recursive, hence representable by step 3) function substituting the numeral \(\bar n\) for the free variable in the formula coded by \(n\); set \(\delta := \psi(\ulcorner \mathrm{diag}(y)\urcorner)[y:=\ulcorner \psi(\mathrm{diag}(y))\urcorner]\) — formally, apply \(\psi\) to the Gödel number of "apply diag to oneself". Unwinding the representability of diag gives the biconditional. This is the general form of the liar-paradox device made rigorous. B

\text{Apply step 5 to } \psi(x) :\equiv \neg \mathrm{Prov}_T(x), \text{ obtaining } G_T \text{ with } T \vdash G_T \leftrightarrow \neg\mathrm{Prov}_T(\ulcorner G_T \urcorner).

\(G_T\) is the Gödel sentence: it is (provably in \(T\)) equivalent to the arithmetised assertion of its own unprovability. B

\text{Suppose } T \vdash G_T. \text{ Then } T \vdash \mathrm{Prov}_T(\ulcorner G_T\urcorner) \text{ (by step 1's representability of the actual proof) and } T \vdash \neg \mathrm{Prov}_T(\ulcorner G_T\urcorner) \text{ (by step 6). Contradiction with consistency (hypothesis).}

If \(T\) really proves \(G_T\), some numeral \(\bar p\) codes that proof, so \(\rho_{\mathrm{Prf}_T}(\bar p,\ulcorner G_T\urcorner)\) is a true numerical fact hence \(T\)-provable by step 3, giving \(T \vdash \mathrm{Prov}_T(\ulcorner G_T\urcorner)\); combined with \(T \vdash G_T\) and step 6 this yields \(T \vdash \neg\mathrm{Prov}_T(\ulcorner G_T\urcorner)\) too, so \(T\) is inconsistent — contradicting hypothesis (ii). Hence \(T \nvdash G_T\). B

\text{Suppose } T \vdash \neg G_T. \text{ By step 6, } T \vdash \mathrm{Prov}_T(\ulcorner G_T \urcorner). \text{ Under } \omega\text{-consistency this forces } T \vdash G_T, \text{ contradicting step 7.}

\(\omega\)-consistency (no formula \(\varphi(x)\) with \(T \vdash \neg\varphi(\bar n)\) for every \(n\) yet \(T \vdash \exists x\,\varphi(x)\)) is used precisely here: from \(T \vdash \mathrm{Prov}_T(\ulcorner G_T\urcorner)\), i.e. \(T\vdash \exists p\,\rho_{\mathrm{Prf}_T}(p,\ulcorner G_T\urcorner)\), together with the fact (step 7) that no numeral actually codes a proof of \(G_T\), hence \(T \vdash \neg \rho_{\mathrm{Prf}_T}(\bar n, \ulcorner G_T\urcorner)\) for every \(n\) — an \(\omega\)-inconsistency unless we can extract an actual witness, which by representability gives \(T \vdash G_T\). (Rosser's 1936 refinement replaces \(\mathrm{Prov}_T\) by a trick predicate comparing proof-of-\(\varphi\) against proof-of-\(\neg\varphi\) codes, and gets \(T \nvdash \neg G_T\) from mere consistency, removing the need for \(\omega\)-consistency; we record this as the standard strengthening without re-deriving it in full.) C

\text{Conclusion of Theorem 1: } T \nvdash G_T \text{ and } T \nvdash \neg G_T \text{ (the latter under } \omega\text{-consistency, or unconditionally via Rosser).}

Combines steps 7 and 8/Rosser-remark. Since \(G_T\) is equivalent (step 6) to its own unprovability and it is indeed unprovable (step 7), \(G_T\) is true in \(\mathbb{N}\) — this gives the "moreover" clause of the statement. A

\text{Formalise steps 1–9 inside } T \text{ itself: } T \vdash \big(\mathrm{Con}(T) \to \neg\mathrm{Prov}_T(\ulcorner G_T\urcorner)\big), \text{ i.e. } T \vdash \mathrm{Con}(T) \to G_T.

This is the Second Incompleteness Theorem's core content: the argument of step 7 (\(T\vdash G_T \Rightarrow T\) inconsistent) is itself a chain of elementary reasoning about coded proofs, and — because \(T\) proves enough arithmetic (hypothesis iii) and its provability predicate satisfies the derivability conditions D1–D3 (Hilbert–Bernays–Löb, cited as a lemma) — that entire chain can be carried out and verified *inside* \(T\), yielding this implication as a theorem of \(T\), not merely a fact about \(T\) provable from outside. C

\text{Suppose } T \vdash \mathrm{Con}(T). \text{ Then by step 10, } T \vdash G_T. \text{ But step 9 gives } T \nvdash G_T. \text{ Contradiction.}

Modus ponens on step 10 together with the assumption, directly contradicting step 9 (which used only hypotheses i–iii, not \(\omega\)-consistency, in Rosser's strengthened form). Hence \(T \nvdash \mathrm{Con}(T)\), completing the Second Theorem. B

Result

T \text{ consistent, recursively axiomatised}, \ T \vdash Q \ \Rightarrow\ T \nvdash G_T,\ T\nvdash \neg G_T\ (\text{under } \omega\text{-consistency, or via Rosser unconditionally}); \quad T \nvdash \mathrm{Con}(T)

Reading. Any honest, mechanically checkable, sufficiently expressive axiom system for arithmetic has true statements it cannot prove, and cannot certify its own reliability from within.

Scope. Applies to every recursively axiomatised consistent theory interpreting Robinson arithmetic \(Q\) — this includes Peano Arithmetic \(\mathrm{PA}\), Zermelo–Fraenkel set theory \(\mathrm{ZFC}\), and virtually all foundational systems used in mathematics. It does not apply to weaker theories that fail to represent multiplication/exponentiation (e.g. Presburger arithmetic), nor to non-recursively-axiomatised theories such as true arithmetic \(\mathrm{Th}(\mathbb{N})\), nor does it say anything about inconsistent theories.

Corollaries & converses

No complete recursive extension. No consistent recursively axiomatised extension of \(T\) (satisfying the same hypotheses) is complete — adding \(G_T\) or \(\neg G_T\) as a new axiom just produces a new theory \(T'\) with its own Gödel sentence \(G_{T'}\).
Undecidability corollary. Any such \(T\) is undecidable (no algorithm decides theoremhood), since a decision procedure would let one mechanically settle \(G_T\), contradicting the theorem; this links incompleteness directly to the unsolvability of the halting problem via the Entscheidungsproblem.
Löb's Theorem. A closely related result: \(T \vdash \mathrm{Prov}_T(\ulcorner\varphi\urcorner) \to \varphi\) implies \(T \vdash \varphi\), of which the Second Theorem is essentially the instance \(\varphi = \bot\) (false), since \(\mathrm{Con}(T)\) is \(\neg\mathrm{Prov}_T(\ulcorner\bot\urcorner)\).
Converse fails / no converse in general. There is no meaningful single converse statement — but note the partial converse-flavoured fact: stronger theories CAN prove weaker theories' consistency. E.g. \(\mathrm{ZFC} \vdash \mathrm{Con}(\mathrm{PA})\). This does not contradict the theorem because \(\mathrm{ZFC} \neq \mathrm{PA}\); \(\mathrm{ZFC}\) still cannot prove \(\mathrm{Con}(\mathrm{ZFC})\) (assuming it is consistent).
Gentzen's consistency proof shows \(\mathrm{Con}(\mathrm{PA})\) is provable using transfinite induction up to \(\varepsilon_0\) — this is not a counterexample to the theorem because that induction principle is not itself available inside \(\mathrm{PA}\); it illustrates exactly the boundary the theorem draws.

Fails without

Drop recursive axiomatisability: true arithmetic \(\mathrm{Th}(\mathbb{N})\) is complete (trivially — it contains every true sentence and refutes every false one) and even proves its own \(\mathrm{Con}\)-analogue in a suitable sense, but it is not a "theory" any prover or algorithm could ever be handed, since its axiom set is not decidable (indeed not even recursively enumerable).
Drop sufficient strength: Presburger arithmetic (\(\langle\mathbb{N},+,0,1\rangle\), no multiplication) is consistent, recursively axiomatised, complete, AND decidable — Gödel's construction cannot be carried out because the coding of proofs as numbers essentially requires representing multiplication (exponential growth of code numbers), which this theory cannot express.
Drop consistency: an inconsistent \(T\) trivially proves \(\mathrm{Con}(T)\) (it proves everything, true or false), so the "unless inconsistent" clause is not optional decoration — it is load-bearing.
Weaken derivability condition D3 (used only for Theorem 2): one can define alternative "provability" predicates lacking D3 for which the analogue of \(\mathrm{Con}(T)\) IS provable in \(T\) — showing the second theorem genuinely needs all three Hilbert–Bernays–Löb conditions, not just "some" provability-like predicate.

Common errors

"Gödel's theorem shows mathematics is inconsistent/unreliable." False — the theorem presupposes consistency throughout; it shows a consistent-and-sufficiently-strong system cannot certify its OWN consistency, not that it lacks consistency.
"\(G_T\) is simply unprovable AND unfalsifiable, so it's meaningless/undecidable-in-truth-value." Confuses provability (a syntactic, \(T\)-relative notion) with truth (a semantic notion). \(G_T\) is a perfectly meaningful, and in fact true, sentence of arithmetic — it is just not a theorem of \(T\). Truth is not confined to what \(T\) proves.
"This means human minds can prove things machines/formal systems can't (Lucas–Penrose)." A famous but contested philosophical extrapolation, not a mathematical consequence; it silently assumes humans reason according to some fixed, sound, consistent formal system whose Gödel sentence a human could then somehow "see" as true — a step Gödel's theorem itself does not license.
Treating \(\mathrm{Con}(T)\) as some vague informal claim rather than the specific arithmetised sentence \(\forall p\, \neg \rho_{\mathrm{Prf}_T}(p, \ulcorner 0{=}1\urcorner)\). The Second Theorem is precisely about THIS coded sentence; different (non-equivalent under weak theories) formalisations of "consistency" can behave differently — this is the subtlety exploited in some folklore "paradoxes".
Applying the theorem to any old system without checking it interprets \(Q\). Students sometimes claim e.g. Euclidean geometry or propositional logic "must be incomplete by Gödel" — both are actually complete and decidable, precisely because they fail hypothesis (iii).

Discussion

Gödel proved these results in his 1931 paper "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I", originally for a system close to Russell and Whitehead's Principia Mathematica plus the Peano axioms, but noted from the outset that the argument was general. The construction is often summarised as a rigorous version of the Liar Paradox — "this sentence is unprovable" rather than "this sentence is false" — the shift from truth to provability being exactly what rescues it from outright contradiction and turns it into a genuine mathematical theorem.

The representability lemma (step 3) is the load-bearing technical achievement: it shows that syntax itself — proofs, formulas, substitution — can be faithfully mirrored inside arithmetic, so that a theory powerful enough to do school arithmetic is automatically powerful enough to talk about its own proof theory. This "arithmetisation of syntax" is one of the most influential ideas in twentieth century logic, and it is precisely the same coding technique (via primitive recursive functions and, later, Turing machines) that gives Church and Turing's independent proofs of the undecidability of the Entscheidungsproblem the following few years.

The Second Theorem is often mis-stated as "no theory can prove its own consistency", full stop — but as the corollaries above show, a strictly stronger theory can certainly prove a weaker one consistent (\(\mathrm{ZFC}\) proves \(\mathrm{Con}(\mathrm{PA})\)), and even \(T\) itself can prove its own consistency relative to extra non-finitary principles not available inside \(T\) (Gentzen's \(\varepsilon_0\)-induction proof of \(\mathrm{Con}(\mathrm{PA})\)). The theorem is a precise statement about what a theory can verify using only its own resources, not a blanket impossibility result about consistency proofs in general.

A more refined modern viewpoint recasts both theorems as fixed-point phenomena of a modal provability logic \(\mathbf{GL}\) (Gödel–Löb logic), where \(\Box\) is read as \(\mathrm{Prov}_T\); Solovay's completeness theorem (1976) shows \(\mathbf{GL}\) exactly axiomatises the schemata of provability behaviour common to all sufficiently strong r.e. theories, giving the derivability conditions D1–D3 a clean algebraic home and making Löb's theorem the modal validity \(\vdash \Box(\Box p \to p) \to \Box p\).

Worked examples

\text{Take } T = \mathrm{PA} \text{ (Peano Arithmetic). Verify hypotheses.}

\(\mathrm{PA}\)'s axiom schema (the induction schema plus finitely many basic axioms) is given by an explicit syntactic pattern, hence decidable, so \(\mathrm{PA}\) is recursively axiomatised. \(\mathrm{PA}\) is assumed/believed consistent (unprovable within \(\mathrm{PA}\) itself, by the theorem!). \(\mathrm{PA} \vdash Q\) trivially since \(Q\)'s axioms are among the basic (non-induction) axioms of \(\mathrm{PA}\). A

\text{Construct } G_{\mathrm{PA}}: \ \mathrm{PA} \vdash G_{\mathrm{PA}} \leftrightarrow \neg\mathrm{Prov}_{\mathrm{PA}}(\ulcorner G_{\mathrm{PA}}\urcorner).

Direct application of steps 1–6 of the proof to \(T=\mathrm{PA}\). A

\text{Conclude } \mathrm{PA} \nvdash G_{\mathrm{PA}}, \ \mathrm{PA}\nvdash \neg G_{\mathrm{PA}}, \text{ and } G_{\mathrm{PA}} \text{ is true in } \mathbb{N}.

By steps 7–9 of the main proof, using that \(\mathrm{PA}\) is (assumed) consistent and \(\omega\)-consistent (true of the standard system \(\mathrm{PA}\)). B

\mathrm{PA} \nvdash G_{\mathrm{PA}}, \quad \mathbb{N} \models G_{\mathrm{PA}}

Reading. There is a concrete arithmetical sentence, true of the natural numbers, that Peano Arithmetic cannot prove.

\text{Take } T = \mathrm{ZFC}. \text{ Does } \mathrm{ZFC} \vdash \mathrm{Con}(\mathrm{ZFC})?

Check hypotheses: \(\mathrm{ZFC}\)'s axiom schemata (Separation, Replacement) are decidable syntactic patterns so \(\mathrm{ZFC}\) is recursively axiomatised; \(\mathrm{ZFC}\) interprets arithmetic via the finite ordinals \(\omega\) with set-theoretic \(+,\times\), so \(\mathrm{ZFC}\vdash Q\); \(\mathrm{ZFC}\) is (widely believed, unprovably-within-itself) consistent; its natural provability predicate satisfies D1–D3 (standard, via the same arithmetisation-of-syntax argument, now carried out for the theory of finite sets). A

\text{By the Second Incompleteness Theorem applied with } T=\mathrm{ZFC}: \ \mathrm{ZFC}\nvdash \mathrm{Con}(\mathrm{ZFC}) \text{ (assuming } \mathrm{ZFC} \text{ consistent).}

Direct instantiation of steps 10–11 of the main proof. B

\text{Contrast: does some theory prove } \mathrm{Con}(\mathrm{ZFC})? \text{ Yes — e.g. } \mathrm{ZFC} + \text{"there exists an inaccessible cardinal"} \vdash \mathrm{Con}(\mathrm{ZFC}),

If \(\kappa\) is inaccessible then \(V_\kappa\) is a set model of \(\mathrm{ZFC}\), and existence of a model of \(\mathrm{ZFC}\) implies (by soundness of first-order logic) \(\mathrm{Con}(\mathrm{ZFC})\); this uses genuinely more axiomatic strength than \(\mathrm{ZFC}\) alone provides, consistent with the theorem's scope note. C

\mathrm{ZFC} \nvdash \mathrm{Con}(\mathrm{ZFC}), \qquad \mathrm{ZFC}+\text{Inaccessible} \vdash \mathrm{Con}(\mathrm{ZFC})

Reading. The everyday foundation of mathematics cannot certify its own safety from within, though modest extra axiomatic strength (a large cardinal hypothesis) suffices to certify it from outside.

Problems

State precisely which three hypotheses on a theory \(T\) are needed for the First Incompleteness Theorem to apply, and give one concrete theory failing each hypothesis while satisfying the other two.
Solution
Hypotheses: (i) recursively axiomatised, (ii) consistent, (iii) interprets/proves Robinson arithmetic \(Q\). Failing (i) only: true arithmetic \(\mathrm{Th}(\mathbb{N})\) — consistent (it's exactly the true sentences) and certainly proves \(Q\) (in fact proves every true instance), but its axiom set is not decidable. Failing (ii) only: \(Q + (0=1)\) — recursively axiomatised (finite extra axiom) and trivially "proves" \(Q\) since it proves everything, but inconsistent. Failing (iii) only: Presburger arithmetic — recursively axiomatised and consistent, but does not interpret multiplication so cannot represent \(Q\)'s multiplication axioms.
Explain precisely why the Gödel sentence \(G_T\) is not simply "this sentence is false" (a direct formalisation of the Liar Paradox), and why the actual construction avoids contradiction.
Solution
"This sentence is false", formalised via the diagonal lemma as \(\lambda \leftrightarrow \neg\mathrm{True}_T(\ulcorner\lambda\urcorner)\), leads to outright contradiction because — by Tarski's undefinability of truth — no consistent sufficiently strong \(T\) can even define a predicate \(\mathrm{True}_T(x)\) satisfying the Tarski biconditionals \(T\vdash \varphi \leftrightarrow \mathrm{True}_T(\ulcorner\varphi\urcorner)\) for all \(\varphi\); trying to do so with \(\lambda\) forces \(T \vdash \lambda \leftrightarrow \neg \lambda\), a contradiction, so \(\mathrm{True}_T\) simply cannot exist. Gödel instead uses \(\mathrm{Prov}_T(x)\) ("provable", not "true"), which — unlike truth — IS representable/definable inside \(T\) (step 3 of the proof, via the recursive relation \(\mathrm{Prf}_T\)). Provability and truth diverge (a theory need not prove all truths), so \(G_T \leftrightarrow \neg\mathrm{Prov}_T(\ulcorner G_T\urcorner)\) is consistent: \(G_T\) can be (and is) true while unprovable, with no contradiction, exactly because "\(T\nvdash G_T\)" and "\(G_T\) is false" are different claims.
A student claims: "Since \(\mathrm{PA}\) cannot prove \(\mathrm{Con}(\mathrm{PA})\), it follows that \(\mathrm{PA}\) is probably inconsistent, or at least we can never know it's consistent." Assess this claim using the theorem and the worked examples.
Solution
This conflates unprovability-within-\(\mathrm{PA}\) with unprovability outright. The Second Theorem only forbids \(\mathrm{PA}\) from proving its own consistency using its own resources; it says nothing about whether \(\mathrm{Con}(\mathrm{PA})\) can be established by other, stronger means. Two concrete counters: (a) Gentzen (1936) proved \(\mathrm{Con}(\mathrm{PA})\) using transfinite induction up to the ordinal \(\varepsilon_0\), a principle not available inside \(\mathrm{PA}\) but considered constructively acceptable; (b) \(\mathrm{ZFC}\) (assumed consistent, a strictly stronger system) proves \(\mathrm{Con}(\mathrm{PA})\) easily, since \(\mathrm{ZFC}\) can construct a set model of \(\mathrm{PA}\) (e.g. \(\omega\) itself with the usual arithmetic operations) and model existence implies consistency. So the unprovability is a precise structural fact about \(\mathrm{PA}\)'s self-referential limits, not evidence of actual inconsistency.
Where exactly in the proof of the Second Incompleteness Theorem is the derivability condition D3 (\(T \vdash \mathrm{Prov}_T(\ulcorner\varphi\urcorner) \to \mathrm{Prov}_T(\ulcorner\mathrm{Prov}_T(\ulcorner\varphi\urcorner)\urcorner)\)) used, and what would go wrong without it?
Solution
D3 is used implicitly in step 10, where the entire argument of steps 1–9 — an argument ABOUT what \(T\) can and cannot prove — must be re-run and formalised as a proof INSIDE \(T\). In particular, step 7's reasoning "if \(T \vdash G_T\) via proof-code \(\bar p\), then \(T \vdash \mathrm{Prov}_T(\ulcorner G_T\urcorner)\)" needs to be internalised as: from \(T\vdash \mathrm{Prov}_T(\ulcorner G_T\urcorner)\) as a HYPOTHESIS inside the \(T\)-formalised argument, derive \(T \vdash \mathrm{Prov}_T(\ulcorner \mathrm{Prov}_T(\ulcorner G_T\urcorner)\urcorner)\) — i.e., \(T\) needs to know, about its own provability predicate, that provability of a statement implies provability of the STATEMENT-THAT-IT'S-PROVABLE. That is precisely D3. Without D3, the internal argument establishing \(T \vdash \mathrm{Con}(T) \to G_T\) cannot be carried out, and indeed alternative "provability" predicates satisfying only D1–D2 (but not D3) are known for which \(T\) CAN prove its own analogue of consistency — showing the theorem genuinely fails without D3.
Using Löb's Theorem (\(T \vdash \mathrm{Prov}_T(\ulcorner\varphi\urcorner)\to\varphi\) implies \(T\vdash \varphi\), for \(T\) satisfying D1–D3), give a one-line derivation of the Second Incompleteness Theorem, and explain why this shows the Second Theorem is a special case of Löb's Theorem rather than an independent fact.
Solution
Apply Löb's theorem with \(\varphi := \bot\) (i.e. \(0=1\)). Löb's theorem says: IF \(T \vdash \mathrm{Prov}_T(\ulcorner\bot\urcorner)\to\bot\), THEN \(T\vdash \bot\). Now \(\mathrm{Con}(T)\) is by definition \(\neg\mathrm{Prov}_T(\ulcorner\bot\urcorner)\), i.e. \(\mathrm{Prov}_T(\ulcorner\bot\urcorner)\to\bot\) is exactly \(\mathrm{Con}(T)\) written out. So Löb's theorem instantiated here reads: \(T\vdash \mathrm{Con}(T) \Rightarrow T \vdash \bot\), i.e. if \(T\) proves its own consistency, \(T\) is (provably, in the meta-theory, using \(T\)'s actual inconsistency) inconsistent. Contrapositive: if \(T\) is consistent, \(T\nvdash \mathrm{Con}(T)\) — exactly the Second Incompleteness Theorem. This shows the Second Theorem is the \(\varphi=\bot\) instance of the strictly more general Löb phenomenon about self-referential provability claims, unifying it with the modal logic \(\mathbf{GL}\) perspective from the Discussion section.