42.01.09 · mathematical-logic / first-order-logic-completeness

Gödel Numbering, the Fixed-Point Lemma, and the Incompleteness Theorems

shipped3 tiersLean: none

Anchor (Master): Enderton 2001 *A Mathematical Introduction to Logic* 2e §3.4-3.5; Boolos, Burgess and Jeffrey 2007 *Computability and Logic* 5e (Cambridge) Ch. 17-18 (the diagonal lemma, the first and second incompleteness theorems, the derivability conditions); Smorynski 1977 'The incompleteness theorems' in the *Handbook of Mathematical Logic* (North-Holland) (the modal/derivability-condition treatment, Löb's theorem, provability logic GL); Hájek and Pudlák 1993 *Metamathematics of First-Order Arithmetic* (Springer) Ch. I, III (the formalised $\Sigma_1$-completeness and the second theorem inside $I\Sigma_1$); Lindström 1997 *Aspects of Incompleteness* (Springer) (the interpretability and reflection landscape, Rosser's trick, the structure of the $\Pi_1$/$\Sigma_1$ independent sentences)

Intuition Beginner

The previous unit showed that arithmetic can mirror any computation. This unit cashes that in for the most famous result in logic. The first move is a coding trick. Pick a fixed scheme that turns every symbol, every formula, and every written proof into a whole number — the way text is stored as numbers inside a computer. Once that is fixed, a statement about formulas becomes a statement about numbers, and a theory that talks about numbers can be made to talk about its own sentences and its own proofs.

Now comes the surprising part. Using this coding, you can build a single sentence that, read through the code, says of itself: "I have no proof in this theory." Call it $G$ . Think about whether $G$ could be provable. If the theory could prove $G$ , then $G$ would be a proved sentence that announces it has no proof — the theory would be proving a falsehood. A trustworthy theory does not do that. So $G$ is not provable. But that is exactly what $G$ claims. So $G$ is true and yet unprovable.

The conclusion is stark. Any reasonable theory of arithmetic — one that is consistent and whose axioms a machine can list — must leave some true statements unproved. You cannot fix this by adding more axioms: the same trick builds a new unprovable truth for the patched-up theory. There is no complete, consistent, machine-checkable bible of all arithmetic truths.

A second sentence makes it worse. The statement "this theory is consistent" can itself be coded as a sentence of arithmetic. A consistent theory cannot prove its own consistency. The theory's faith in itself is one thing it can never establish from the inside.

Visual Beginner

The picture is a loop that bites its own tail. A coding scheme sends each sentence to a number; a special sentence is built so that, decoded, it talks about its own number. The diagram traces how "I am unprovable" closes the loop.

   STEP 1: code everything as numbers
       sentence  phi   --->  number  #phi
       a proof   P     --->  number  #P
       "p is a proof of the sentence coded x"  ---> a number-relation Prf(p, x)

   STEP 2: build a sentence G that points back at its own code

        G   says:   "there is NO number p with  Prf( p , #G )"
                                                       ^^^^
                                  G's claim is ABOUT G's own code

   STEP 3: ask if G can be proved

        if the theory proves G   -->  there IS a proof of G
                                  -->  so "no proof of G" is FALSE
                                  -->  the theory proved a falsehood   (not allowed)

        therefore   G is NOT provable
        but that is exactly what G says   -->  G is TRUE

   RESULT:  a sentence that is true but has no proof.

A code is a fixed dictionary: every sentence gets a number, no two sentences share a number, and you can mechanically translate back and forth. Once " $p$ is a proof of the sentence with number $x$ " is itself a relation between numbers, arithmetic can express it, and the self-pointing sentence $G$ becomes possible.

sentence built	what it says about itself	the outcome
$G$	"I am not provable"	true but unprovable
Con	"this theory is consistent"	true but unprovable (if the theory is consistent)
(a Liar)	"I am false / I am untrue"	shows truth is not codeable at all

The same self-pointing move yields three results: an unprovable truth, an unprovable consistency, and the impossibility of a truth-detector.

Worked example Beginner

We watch the self-reference get built with a tiny made-up coding, to see that nothing magical happens — it is bookkeeping. Suppose our only formulas are short strings, and we fix a dictionary that assigns each one a number. Say the formula " $x$ is even" gets the number $40$ , and the formula " $x$ has no proof" gets the number $77$ . These numbers are the codes.

Step 1. Set up one operation on codes: substitution. Given the code of a formula with a blank $x$ , and a number $n$ , "substitute $n$ for $x$ " produces the code of the new sentence. Write this as $sub (code, n)$ . For instance, $sub (40, 6)$ is the code of " $6$ is even." This is a definite numerical operation: feed it two numbers, get one number back.

Step 2. We want a sentence that talks about its own code. The clever step is to substitute a formula's code into that same formula. Take the formula "the sentence coded $sub (x, x)$ has no proof," and let its code be some number, say $90$ .

Step 3. Now plug $90$ in for $x$ in that very formula. By definition the result is the sentence "the sentence coded $sub (90, 90)$ has no proof." But $sub (90, 90)$ is, by construction, the code of this very sentence we just wrote. So the sentence says "the sentence coded (my own code) has no proof" — it talks about itself.

Step 4. Read what it now claims: "I have no proof." We built a self-referential sentence using only the substitution operation on codes, no paradox and no infinite regress.

What this tells us: self-reference is not a mystical trick. It is the ordinary operation of plugging a formula's code into itself, which the substitution function makes a plain numerical computation. Because arithmetic can carry out that computation, arithmetic can host sentences that speak about themselves — and "I am unprovable" is one of them.

Check your understanding Beginner

Exercise (easy, multiple-choice).

What is the point of a Gödel numbering (a coding of formulas as numbers)?

It makes formulas shorter to write.
It lets a theory about numbers also talk about its own sentences and proofs.
It proves that every formula is true.
It replaces proofs with calculations so proofs are no longer needed.

Hint

Once sentences are numbers, statements about sentences become statements about numbers.

Answer

B. Coding sentences and proofs as numbers turns "is a proof of" into a relation between numbers, so a theory of arithmetic can express facts about its own syntax. Feedback-correct: that self-reference is exactly what the incompleteness argument needs. Feedback-wrong: the coding does not shorten formulas, does not make anything true, and does not abolish proofs — it lets arithmetic describe them.

Formal definition Intermediate+

Fix the language of arithmetic $L_{A} = {0, S, +, \cdot, <}$ , its standard model $N$ 42.01.04 pending, and a theory $T$ in $L_{A}$ that is recursively axiomatised (its set of axiom codes is recursive) and extends $Q$ 42.01.08 pending. A Gödel numbering is an injective effective map $┌ \cdot ┐$ assigning to each symbol, term, formula, and finite sequence of formulas a natural number, built from a recursive coding of finite sequences (for instance $⟨ a_{0}, \dots, a_{n} ⟩ = \prod_{i \leq n} p_{i}^{a_{i} + 1}$ with $p_{i}$ the $i$ -th prime, or Gödel's $β$ -function coding of 42.01.08 pending). For a formula $φ$ the closed term $\underline{┌ φ ┐} = S^{┌ φ ┐} 0$ is its numeral, the $L_{A}$ -name of its code; we write $┌ φ ┐$ for this numeral when the context is a formula slot ^{[Enderton §3.4]}.

The substitution function $sub (┌ φ (x) ┐, n) = ┌ φ (\underline{n}) ┐$ and the diagonal function $d (e) = sub (e, e)$ are primitive recursive, hence representable in $Q$ . For recursively axiomatised $T$ the relations " $x$ codes an $L_{A}$ -formula", " $y$ codes a $T$ -axiom", and the proof predicate $$ \mathrm{Prf}_T(p, x) \equiv \text{" $p$ codes a finite $T$ -deduction whose last line is the formula coded by $x$ "} $$ are primitive recursive, so $Prf_{T}$ is representable in $Q$ by a $Δ_{0}$ formula (also written $Prf_{T}$ ). The provability predicate is the $Σ_{1}$ formula $$ \mathrm{Pr}_T(x) := \exists p,\mathrm{Prf}_T(p, x), $$ and for a sentence $σ$ one abbreviates $□_{T} σ := Pr_{T} (┌ σ ┐)$ . The consistency statement is the $Π_{1}$ sentence $$ \mathrm{Con}_T := \neg,\mathrm{Pr}_T(\ulcorner 0 = S0\urcorner), $$ expressing that the refutable sentence $0 = S 0$ has no $T$ -proof.

A theory $T$ is $ω$ -consistent when for no formula $θ (x)$ does $T ⊢ \exists x θ (x)$ while $T ⊢ \neg θ (\underline{n})$ for every $n \in N$ ; $ω$ -consistency implies consistency but is strictly stronger. The truth set is $# Th (N) = {┌ σ ┐ : σ a sentence, N ⊨ σ}$ , the set of codes of true arithmetic sentences. A set $A \subseteq N$ is arithmetically definable when $A = {n : N ⊨ α (\underline{n})}$ for some $L_{A}$ -formula $α (x)$ .

Counterexamples to common slips Intermediate+

"The Gödel sentence is provably equivalent to a paradox, so the theory is contradictory." The Liar "I am false" is a genuine paradox because truth is not arithmetically definable (Tarski). The Gödel sentence replaces "false" with the definable predicate "not provable", which is $\neg Σ_{1}$ , not $\neg$ "true"; self-reference through a definable predicate is consistent, and $G_{T}$ is simply true and unprovable.
"Incompleteness needs the full strength of $P A$ ." The first theorem needs only that $T$ extends $Q$ and is recursively axiomatised and consistent — no induction. Induction (e.g. $T \supseteq I Σ_{1}$ ) is needed only for the second theorem, whose derivability conditions require provable $Σ_{1}$ -completeness inside $T$ .
" $T ⊬ G_{T}$ and $T ⊬ \neg G_{T}$ both follow from consistency." Only $T ⊬ G_{T}$ follows from plain consistency. $T ⊬ \neg G_{T}$ needs $ω$ -consistency in Gödel's original argument; plain consistency suffices only after Rosser's modification of the provability predicate.
"The second theorem says no consistency proof of $T$ is possible." It says $T$ cannot prove $Con_{T}$ in $T$ itself. A stronger theory can prove $Con_{T}$ (Gentzen proved $Con_{P A}$ using transfinite induction up to $ε_{0}$ ); the bar is on self-certification, and it is sensitive to how consistency is formalised (a Rosser or Feferman predicate can make a $Con$ -variant provable).

Key theorem with proof Intermediate+

The hinge of the entire development is the diagonal lemma: arithmetic admits self-reference. Everything downstream — both incompleteness theorems, Tarski's theorem, Löb's theorem — is an instance of feeding a chosen predicate into a sentence that asserts that predicate of its own code.

Lemma (Diagonal / Fixed-Point). Let $T \supseteq Q$ be recursively axiomatised. For every formula $ψ (x)$ with one free variable there is a sentence $G$ with $$ T \vdash G \leftrightarrow \psi(\ulcorner G\urcorner). $$ ^{[Enderton §3.4]}.

Proof. The diagonal function $d (e) = sub (e, e)$ is primitive recursive, hence by the representability theorem 42.01.08 pending there is a formula $Diag (x, y)$ representing its graph in $Q$ : for all $e$ , $Q ⊢ \forall y (Diag (\underline{e}, y) \leftrightarrow y = \underline{d (e)})$ . Define the formula $$ \theta(x) := \exists y,\big(\mathrm{Diag}(x, y) \wedge \psi(y)\big), $$ let $g = ┌ θ (x) ┐$ be its code, and set $G := θ (\underline{g})$ , a sentence. By definition of $d$ and $sub$ , $d (g) = sub (g, g) = ┌ θ (\underline{g}) ┐ = ┌ G ┐$ . Now $T$ proves $Diag (\underline{g}, y) \leftrightarrow y = \underline{d (g)} = ┌ G ┐$ , so inside $T$ , $$ G = \theta(\underline g) = \exists y,(\mathrm{Diag}(\underline g, y) \wedge \psi(y)) ;\leftrightarrow; \psi(\underline{d(g)}) ;=; \psi(\ulcorner G\urcorner). $$ The existential collapses because $Diag (\underline{g}, y)$ pins $y$ to the single value $\underline{┌ G ┐}$ provably in $T$ . Hence $T ⊢ G \leftrightarrow ψ (┌ G ┐)$ . $□$

Theorem (Gödel's First Incompleteness Theorem). Let $T \supseteq Q$ be consistent and recursively axiomatised. Let $G_{T}$ be a fixed point of $ψ (x) = \neg Pr_{T} (x)$ , so $T ⊢ G_{T} \leftrightarrow \neg Pr_{T} (┌ G_{T} ┐)$ . Then $T ⊬ G_{T}$ , and if $T$ is $ω$ -consistent then $T ⊬ \neg G_{T}$ ; so $T$ is incomplete. Moreover $G_{T}$ is a true $Π_{1}$ sentence ^{[Enderton §3.5]}.

Proof. Suppose $T ⊢ G_{T}$ . Then there is a $T$ -proof of $G_{T}$ , coded by some $p$ , so $N ⊨ Prf_{T} (\underline{p}, ┌ G_{T} ┐)$ ; this is a true $Σ_{1}$ fact, so by $Σ_{1}$ -completeness $T ⊢ Prf_{T} (\underline{p}, ┌ G_{T} ┐)$ , whence $T ⊢ Pr_{T} (┌ G_{T} ┐)$ . But the fixed-point equivalence gives $T ⊢ G_{T} \to \neg Pr_{T} (┌ G_{T} ┐)$ , so from $T ⊢ G_{T}$ we get $T ⊢ \neg Pr_{T} (┌ G_{T} ┐)$ , contradicting consistency. Hence $T ⊬ G_{T}$ .

For the second half, suppose $T ⊢ \neg G_{T}$ , i.e. $T ⊢ Pr_{T} (┌ G_{T} ┐)$ , that is $T ⊢ \exists p Prf_{T} (p, ┌ G_{T} ┐)$ . Since $T ⊬ G_{T}$ , no number $p$ actually codes a proof of $G_{T}$ , so for every $n$ the sentence $Prf_{T} (\underline{n}, ┌ G_{T} ┐)$ is false, hence ( $Σ_{1}$ -completeness, refuting false closed $Δ_{0}$ sentences) $T ⊢ \neg Prf_{T} (\underline{n}, ┌ G_{T} ┐)$ for every $n$ . Together with $T ⊢ \exists p Prf_{T} (p, ┌ G_{T} ┐)$ this is exactly an $ω$ -inconsistency. So under $ω$ -consistency $T ⊬ \neg G_{T}$ . Finally, $G_{T}$ is true: $T ⊬ G_{T}$ means no $p$ codes a proof, so $N ⊨ \neg Pr_{T} (┌ G_{T} ┐)$ , and the fixed point gives $N ⊨ G_{T}$ ; and $G_{T}$ is $Π_{1}$ because $\neg Pr_{T}$ is $\neg Σ_{1} = Π_{1}$ . $□$

Bridge. The diagonal lemma is the foundational reason a theory of numbers can refer to itself, and the first incompleteness theorem is exactly this self-reference pointed at the provability predicate $Pr_{T}$ that representability 42.01.08 pending makes available. It builds toward Tarski's undefinability of truth — the same diagonal aimed at a hypothetical truth predicate yields a contradiction rather than an unprovable truth, the difference being that "not provable" is definable while "true" is not — and it appears again in the second incompleteness theorem [42.01.10 context], where the metatheoretic step "if $T$ is consistent then $T ⊬ G_{T}$ " is itself formalised inside $T$ as $T ⊢ Con_{T} \to G_{T}$ . This is the central insight: the gap between truth and provability, measured by the $Σ_{1} / Π_{1}$ asymmetry of 42.01.08 pending, is not an accident of a particular theory but a fixed point of the theory's own provability operator. Putting these together, completeness 42.01.06 pending and incompleteness do not conflict — completeness equates $⊢$ with semantic consequence $⊨$ across all models, while incompleteness concerns truth in the single standard model $N$ , where $G_{T}$ holds but is underivable because some nonstandard model of $T$ refutes it.

Exercises Intermediate+

Exercise 3 (medium, symbolic).

Apply the diagonal lemma to $ψ (x) = Pr_{T} (x)$ to construct a Henkin sentence $H$ with $T ⊢ H \leftrightarrow Pr_{T} (┌ H ┐)$ ( $H$ asserts its own provability). State what $H$ "says" and why its truth value is not settled by the construction alone.

Hint

The diagonal lemma takes any $ψ$ ; here $ψ$ is the provability predicate itself, not its negation.

Answer

The diagonal lemma with $ψ (x) = Pr_{T} (x)$ yields a sentence $H$ with $T ⊢ H \leftrightarrow Pr_{T} (┌ H ┐)$ ; decoded, $H$ says "I am provable in $T$ ." Unlike $G_{T}$ , the construction alone does not fix whether $H$ is provable: a priori $H$ could be true-and-provable or false-and-unprovable. Henkin's problem asked which holds, and Löb's theorem answers it — $T ⊢ Pr_{T} (┌ H ┐) \to H$ holds (it is the fixed-point equivalence in one direction), so by Löb $T ⊢ H$ , hence $H$ is provable and true. Rubric: full credit for the construction, the self-provability reading, and the observation that the construction underdetermines the truth value (resolved by Löb).

Exercise 5 (medium, symbolic).

Using Tarski's theorem and the $Σ_{1}$ -ness of $Pr_{T}$ , explain why the set of $T$ -theorems is arithmetically definable but the set of truths is not, and why this gap is the content of incompleteness for a sound $T$ .

Hint

Provability is $Σ_{1}$ , hence definable; truth is not definable. A sound theory's theorems are a definable subset of an undefinable set.

Answer

The theorem set ${┌ σ ┐ : T ⊢ σ}$ is defined by the $Σ_{1}$ formula $Pr_{T} (x)$ , so it is arithmetically definable (indeed recursively enumerable). The truth set $# Th (N)$ is not definable (Tarski). If $T$ is sound ( $T ⊢ σ \Rightarrow N ⊨ σ$ ), the theorem set is a definable subset of the undefinable truth set, so the two cannot coincide: some true sentence is unprovable. The undefinability of truth is the semantic reason a definable (machine-listable) theory cannot capture all truths. Rubric: full credit for definable-theorems vs undefinable-truths and the soundness-driven strict inclusion.

Exercise 6 (medium, symbolic).

Write the Rosser provability predicate $Pr_{T}^{R} (x)$ and explain in one or two sentences why the Rosser sentence is independent of $T$ from plain consistency alone, with no $ω$ -consistency.

Hint

Rosser's predicate says "there is a proof of $x$ with no smaller proof of $\neg x$ ."

Answer

$Pr_{T}^{R} (x) := \exists p (Prf_{T} (p, x) \land \forall q \leq p \neg Prf_{T} (q, neg (x)))$ , where $neg (x)$ codes the negation of the formula coded by $x$ . Diagonalising $\neg Pr_{T}^{R}$ gives a Rosser sentence $R$ with $T ⊢ R \leftrightarrow \neg Pr_{T}^{R} (┌ R ┐)$ . If $T ⊢ R$ , a proof $p$ of $R$ exists; consistency forbids a proof of $\neg R$ , so in particular none with code $\leq p$ , making $Pr_{T}^{R} (┌ R ┐)$ true and provable, contradicting $R$ . Symmetrically $T ⊢ \neg R$ leads to contradiction. Both directions use only the finite, bounded comparison of proof codes, which plain consistency settles; no statement about all numerals at once is needed. Rubric: full credit for the predicate and the bounded-comparison reason that consistency suffices.

Exercise 7 (hard, symbolic).

Assume the three derivability conditions (D1)-(D3) on $Pr_{T}$ . Prove Löb's theorem: if $T ⊢ Pr_{T} (┌ σ ┐) \to σ$ then $T ⊢ σ$ .

Hint

Diagonalise $ψ (x) = Pr_{T} (x) \to σ$ to get a sentence $L$ with $T ⊢ L \leftrightarrow (Pr_{T} (┌ L ┐) \to σ)$ , then push $Pr_{T}$ through using (D1)-(D3).

Answer

By the diagonal lemma fix $L$ with $T ⊢ L \leftrightarrow (Pr_{T} (┌ L ┐) \to σ)$ . From left to right, $T ⊢ L \to (Pr_{T} (┌ L ┐) \to σ)$ ; by (D1) and (D2), $T ⊢ Pr_{T} (┌ L ┐) \to Pr_{T} (┌ Pr_{T} (┌ L ┐) \to σ ┐)$ , and again by (D2) $T ⊢ Pr_{T} (┌ L ┐) \to (Pr_{T} (┌ Pr_{T} (┌ L ┐) ┐) \to Pr_{T} (┌ σ ┐))$ . By (D3), $T ⊢ Pr_{T} (┌ L ┐) \to Pr_{T} (┌ Pr_{T} (┌ L ┐) ┐)$ , so chaining, $T ⊢ Pr_{T} (┌ L ┐) \to Pr_{T} (┌ σ ┐)$ . With the hypothesis $T ⊢ Pr_{T} (┌ σ ┐) \to σ$ this gives $T ⊢ Pr_{T} (┌ L ┐) \to σ$ , which is the right side of the fixed point, so $T ⊢ L$ . Then (D1) gives $T ⊢ Pr_{T} (┌ L ┐)$ , and modus ponens on $T ⊢ Pr_{T} (┌ L ┐) \to σ$ yields $T ⊢ σ$ . Rubric: full credit for the diagonal step, the (D1)-(D3) pushes, and the final detachment.

Exercise 8 (hard, symbolic).

Deduce Gödel's second incompleteness theorem ( $T ⊬ Con_{T}$ , for consistent $T \supseteq I Σ_{1}$ ) from Löb's theorem in one line, and separately from the formalised first theorem $T ⊢ Con_{T} \to G_{T}$ .

Hint

Take $σ = (0 = S 0)$ in Löb's theorem; note $Con_{T} = \neg Pr_{T} (┌ 0 = S 0 ┐)$ .

Answer

Via Löb. Put $σ := (0 = S 0)$ . Then $Pr_{T} (┌ σ ┐) \to σ$ is, by contraposition, equivalent over $T$ to $\neg σ \to \neg Pr_{T} (┌ σ ┐)$ ; since $T ⊢ \neg σ$ (as $T \supseteq Q$ proves $0 \neq = S 0$ ), $T ⊢ Con_{T} \leftrightarrow (Pr_{T} (┌ σ ┐) \to σ)$ — more directly, $T ⊢ Con_{T}$ would give $T ⊢ Pr_{T} (┌ σ ┐) \to σ$ , so by Löb $T ⊢ σ$ , i.e. $T ⊢ 0 = S 0$ , contradicting consistency. Hence $T ⊬ Con_{T}$ .

Via the formalised first theorem. The first theorem's argument " $T$ consistent $\Rightarrow T ⊬ G_{T}$ " formalises, using (D1)-(D3), to $T ⊢ Con_{T} \to \neg Pr_{T} (┌ G_{T} ┐)$ , and the fixed point gives $T ⊢ \neg Pr_{T} (┌ G_{T} ┐) \to G_{T}$ , so $T ⊢ Con_{T} \to G_{T}$ . If $T ⊢ Con_{T}$ then $T ⊢ G_{T}$ , contradicting the first theorem. Rubric: full credit for both routes, the $σ = 0 = S 0$ instance of Löb, and the $Con_{T} \to G_{T}$ formalisation.

Advanced results Master

The diagonal lemma supports four developments: the abstract first theorem and its hypotheses, Rosser's elimination of $ω$ -consistency, the second theorem through the derivability conditions and Löb's theorem, and the landscape of concrete independent statements and the misreadings the theorems invite.

Theorem 1 (the first theorem, abstract form, and its exact hypotheses). For consistent recursively axiomatised $T \supseteq Q$ , the Gödel sentence $G_{T}$ obtained by diagonalising $\neg Pr_{T}$ is unprovable; under $ω$ -consistency it is also irrefutable; in every case it is a true $Π_{1}$ sentence ^{[Boolos-Burgess-Jeffrey Ch. 17]}. Each hypothesis does exact work: recursive axiomatisability makes $Prf_{T}$ primitive recursive and hence representable, so $Pr_{T}$ exists as a $Σ_{1}$ formula; extension of $Q$ supplies $Σ_{1}$ -completeness, the bridge from a real proof to its formalised witness; consistency blocks $T ⊢ G_{T}$ ; $ω$ -consistency blocks $T ⊢ \neg G_{T}$ . Weakening any one breaks a step: a non-recursively-axiomatised $T$ (e.g. true arithmetic $Th (N)$ itself) has no representable proof predicate and is complete, dodging the theorem precisely because its axiom set is undefinable. The theorem is therefore not about the content of arithmetic but about the tension between effective axiomatisability and completeness.

Theorem 2 (Rosser's theorem: incompleteness from plain consistency). Replacing $Pr_{T}$ by the Rosser predicate $Pr_{T}^{R} (x) = \exists p (Prf_{T} (p, x) \land \forall q \leq p \neg Prf_{T} (q, neg (x)))$ and diagonalising $\neg Pr_{T}^{R}$ yields a Rosser sentence $R$ with $T ⊬ R$ and $T ⊬ \neg R$ from plain consistency alone ^{[Lindström Ch. 2]}. The asymmetry of Gödel's argument — provability is $Σ_{1}$ but refutability had to be controlled over all numerals — is repaired by building the comparison of proof codes into the predicate, so that both non-provability claims reduce to bounded statements that $Q$ decides. Rosser's sentence is no longer simply "true": its truth value depends on the ordering of proofs, and it is not in general equivalent to $Con_{T}$ , unlike the Gödel sentence. The cost of dropping $ω$ -consistency is the loss of the clean "true but unprovable" reading.

Theorem 3 (the second theorem and Löb's theorem). With $Pr_{T}$ satisfying the Hilbert-Bernays-Löb conditions (D1) $T ⊢ σ \Rightarrow T ⊢ □_{T} σ$ ; (D2) $T ⊢ □_{T} (σ \to τ) \to (□_{T} σ \to □_{T} τ)$ ; (D3) $T ⊢ □_{T} σ \to □_{T} □_{T} σ$ , a consistent $T \supseteq I Σ_{1}$ satisfies $T ⊬ Con_{T}$ ^{[Enderton §3.5]}. Löb's theorem $T ⊢ □_{T} σ \to σ$ iff $T ⊢ σ$ subsumes it at $σ = ⊥$ , and resolves Henkin's problem: the self-asserting-provability sentence $H$ is provable. The conditions are where induction is consumed — (D3) is the internalised $Σ_{1}$ -completeness of 42.01.08 pending, provable only with enough induction ( $I Σ_{1}$ ), which is why $Q$ alone gives the first theorem but not the second. Solovay's completeness theorem identifies the schematically valid principles of $□_{T}$ with the modal logic GL (Gödel-Löb), axiom $□ (□ p \to p) \to □ p$ ; the second theorem and Löb's theorem are theorems of GL, so the entire calculus of provability is a decidable modal logic.

Theorem 4 (concrete independence and the limits of the theorems). Beyond the metamathematical $G_{T}$ and $Con_{T}$ , there are genuinely combinatorial $Π_{2}$ statements independent of $P A$ : the Paris-Harrington strengthened finite Ramsey theorem and Goodstein's theorem on the termination of Goodstein sequences, each true (provable in $ZFC$ via transfinite induction past $ε_{0}$ ) but unprovable in $P A$ , with the unprovability shown by encoding the $ε_{0}$ -recursion that bounds $P A$ 's provably total functions ^{[Lindström Ch. 3]}; these connect to the Ramsey-theoretic combinatorics of 40.05.04. What the theorems do not show: not that there are absolutely unknowable truths (each $G_{T}$ is provable in a stronger system, e.g. $P A + Con_{P A}$ ); not that mathematics is inconsistent or that $N$ is ill-defined; not, against the Lucas-Penrose argument, that human minds transcend machines — that argument assumes the human can know its own consistency to assert its Gödel sentence, the very self-certification the second theorem forbids for any consistent recursively axiomatised system, so a consistent mechanical mind is in the same position and the alleged advantage evaporates. The theorems bound effective axiomatic capture, not knowledge or truth.

Synthesis. The diagonal lemma is the foundational reason every result here exists, and putting these together it organises all four developments as one construction aimed at four predicates: $\neg Pr_{T}$ gives the unprovable $G_{T}$ of Theorem 1, $\neg Pr_{T}^{R}$ gives the Rosser sentence of Theorem 2 that needs only consistency, $Pr_{T} \to σ$ gives Löb's sentence and through it the second theorem of Theorem 3, and $\neg Tr$ gives the Liar that proves truth undefinable — the same self-application separating "definable predicate" (provability, $Σ_{1}$ ) from "undefinable predicate" (truth). This is the central insight: incompleteness is the fixed point of the provability operator, and the second theorem is dual to the first across the move from " $G_{T}$ is true" (semantic, in $N$ ) to " $Con_{T} \to G_{T}$ is provable" (syntactic, in $T$ ), a move that costs exactly the induction ( $I Σ_{1}$ ) needed for the derivability conditions. The provability operator $□_{T}$ generalises from arithmetic to the modal logic GL, so that the whole phenomenon is the decidable calculus of a single modality, and the theorems integrate with computation 42.04.02: the proof set is recursively enumerable and complete, its undecidability is the recursion-theoretic shadow of incompleteness, and Church's theorem on the Entscheidungsproblem 42.01.10 pending routes through the very representability 42.01.08 pending that powers $Pr_{T}$ . Completeness 42.01.06 pending and incompleteness are the bridge between the two readings of " $⊢$ ": complete across all models, incomplete against the standard one — no tension, because $G_{T}$ fails in some nonstandard model of $T$ .

Full proof set Master

Proposition 1 (Diagonal lemma). For recursively axiomatised $T \supseteq Q$ and any $ψ (x)$ , there is a sentence $G$ with $T ⊢ G \leftrightarrow ψ (┌ G ┐)$ .

Proof. The diagonal function $d (e) = sub (e, e)$ is primitive recursive (substitution of a numeral into a formula is a bounded recursion on the code), hence by 42.01.08 pending represented in $Q$ by a formula $Diag (x, y)$ with $Q ⊢ \forall y (Diag (\underline{e}, y) \leftrightarrow y = \underline{d (e)})$ for each $e$ . Set $θ (x) := \exists y (Diag (x, y) \land ψ (y))$ , $g := ┌ θ ┐$ , $G := θ (\underline{g})$ . Then $d (g) = sub (g, g) = ┌ θ (\underline{g}) ┐ = ┌ G ┐$ , and $T$ extends $Q$ so $T ⊢ \forall y (Diag (\underline{g}, y) \leftrightarrow y = ┌ G ┐)$ . Substituting into $G = \exists y (Diag (\underline{g}, y) \land ψ (y))$ , the unique $y = ┌ G ┐$ survives, giving $T ⊢ G \leftrightarrow ψ (┌ G ┐)$ . $□$

Proposition 2 (First incompleteness, non-provability of $G_{T}$ ). For consistent recursively axiomatised $T \supseteq Q$ and $G_{T}$ a fixed point of $\neg Pr_{T}$ , $T ⊬ G_{T}$ .

Proof. If $T ⊢ G_{T}$ then some $p$ codes a proof, so $Prf_{T} (\underline{p}, ┌ G_{T} ┐)$ is a true closed $Σ_{1}$ (indeed $Δ_{0}$ ) sentence; by $Σ_{1}$ -completeness of $Q$ 42.01.08 pending, $T ⊢ Prf_{T} (\underline{p}, ┌ G_{T} ┐)$ , hence $T ⊢ Pr_{T} (┌ G_{T} ┐)$ by existential introduction. The fixed point gives $T ⊢ G_{T} \to \neg Pr_{T} (┌ G_{T} ┐)$ , so $T ⊢ \neg Pr_{T} (┌ G_{T} ┐)$ , and with $T ⊢ Pr_{T} (┌ G_{T} ┐)$ this makes $T$ inconsistent. So $T ⊬ G_{T}$ , whence $N ⊨ \neg Pr_{T} (┌ G_{T} ┐)$ and $N ⊨ G_{T}$ : $G_{T}$ is true. $□$

Proposition 3 (First incompleteness, non-refutability under $ω$ -consistency). If moreover $T$ is $ω$ -consistent, then $T ⊬ \neg G_{T}$ .

Proof. By Proposition 2, $T ⊬ G_{T}$ , so no $n$ codes a $T$ -proof of $G_{T}$ ; each $Prf_{T} (\underline{n}, ┌ G_{T} ┐)$ is a false closed $Δ_{0}$ sentence, hence $T ⊢ \neg Prf_{T} (\underline{n}, ┌ G_{T} ┐)$ for every $n$ by $Σ_{1}$ -completeness. Were $T ⊢ \neg G_{T}$ , the fixed point gives $T ⊢ Pr_{T} (┌ G_{T} ┐)$ , i.e. $T ⊢ \exists p Prf_{T} (p, ┌ G_{T} ┐)$ ; together with $T ⊢ \neg Prf_{T} (\underline{n}, ┌ G_{T} ┐)$ for all $n$ , this is an $ω$ -inconsistency. So $T ⊬ \neg G_{T}$ . $□$

Proposition 4 (Tarski's undefinability of truth). No $L_{A}$ -formula $Tr (x)$ satisfies $N ⊨ Tr (┌ σ ┐) \leftrightarrow σ$ for all sentences $σ$ ; equivalently $# Th (N)$ is not arithmetically definable.

Proof. Suppose $Tr$ works. Diagonalise $\neg Tr (x)$ : there is $L$ with $N ⊨ L \leftrightarrow \neg Tr (┌ L ┐)$ (the diagonal lemma is provable in $Q$ , sound in $N$ ). The defining property of $Tr$ gives $N ⊨ Tr (┌ L ┐) \leftrightarrow L$ , so $N ⊨ L \leftrightarrow \neg L$ , impossible. If $# Th (N)$ were defined by $α (x)$ , then $α$ would be such a $Tr$ , contradiction. $□$

Proposition 5 (Löb's theorem). Under (D1)-(D3), $T ⊢ Pr_{T} (┌ σ ┐) \to σ$ implies $T ⊢ σ$ .

Proof. Diagonalise to get $L$ with $T ⊢ L \leftrightarrow (Pr_{T} (┌ L ┐) \to σ)$ . Then $T ⊢ L \to (Pr_{T} (┌ L ┐) \to σ)$ ; applying (D1) and (D2) twice and (D3) once yields $T ⊢ Pr_{T} (┌ L ┐) \to Pr_{T} (┌ σ ┐)$ (the box distributes over the implication and (D3) supplies $Pr_{T} (┌ L ┐) \to Pr_{T} (┌ Pr_{T} (┌ L ┐) ┐)$ ). With the hypothesis $T ⊢ Pr_{T} (┌ σ ┐) \to σ$ , $T ⊢ Pr_{T} (┌ L ┐) \to σ$ , which is the right side of the fixed point, so $T ⊢ L$ . By (D1), $T ⊢ Pr_{T} (┌ L ┐)$ , and detaching gives $T ⊢ σ$ . $□$

Proposition 6 (Gödel's second incompleteness theorem). For consistent recursively axiomatised $T \supseteq I Σ_{1}$ , $T ⊬ Con_{T}$ .

Proof. Take $σ := (0 = S 0)$ in Löb's theorem; $Con_{T} = \neg Pr_{T} (┌ σ ┐)$ and $T ⊢ \neg σ$ . If $T ⊢ Con_{T}$ , i.e. $T ⊢ \neg Pr_{T} (┌ σ ┐)$ , then $T ⊢ Pr_{T} (┌ σ ┐) \to σ$ vacuously (its antecedent is refuted), so by Proposition 5 $T ⊢ σ$ , i.e. $T ⊢ 0 = S 0$ , contradicting consistency. The hypothesis $T \supseteq I Σ_{1}$ is used to secure (D3), the formalised $Σ_{1}$ -completeness inside $T$ , which $Q$ alone does not provide. $□$

Connections Master

Representability of recursive functions 42.01.08 pending supplies every ingredient consumed here: the proof predicate $Prf_{T}$ is primitive recursive and so $Δ_{0}$ -representable in $Q$ , the substitution function $sub$ is representable and so the diagonal lemma holds, and the $Σ_{1}$ -completeness proved there is exactly what turns a real proof into a provable formal witness and supplies derivability condition (D3) for the second theorem. That unit owns the bridge from computation to provable-numeral facts; this unit aims that bridge at the theory's own syntax to manufacture self-reference, so $42.01.08$ is the engine and $42.01.09$ is the destination of the chapter.
The completeness theorem for first-order logic 42.01.06 pending is the apparent foil that turns out to be no tension: completeness equates $⊢$ with semantic consequence over all structures, while the first incompleteness theorem concerns truth in the single standard model $N$ . The Gödel sentence $G_{T}$ is true in $N$ yet unprovable, which by completeness means some model of $T$ refutes it — a nonstandard model. Completeness even underwrites the existence of that model, so the two theorems are complementary descriptions of the same turnstile.
The halting problem and the recursion theorem 42.04.02 are the computational form of this unit's self-reference: Kleene's recursion theorem (a program can access its own code) is the diagonal lemma in the language of computation, and the undecidability of the halting set is the undecidability of the $Σ_{1}$ -complete provability set. The Gödel sentence is the proof-theoretic image of a program that halts iff it does not, and the unsolvability of halting and the unprovability of $G_{T}$ are one phenomenon in two metatheories.
Church's theorem and the Entscheidungsproblem 42.01.10 pending, co-produced with this unit, draw the undecidability conclusion: because $Pr_{Q}$ is representable and the provability set is recursively enumerable but not recursive (its complement is productive), first-order validity is undecidable. The same arithmetisation that yields incompleteness yields the negative solution of Hilbert's decision problem, so $42.01.09$ and $42.01.10$ are the two faces — incompleteness and undecidability — of the representability of 42.01.08 pending.
The strengthened finite Ramsey theorem and combinatorial independence 40.05.04 give the concrete payoff: the Paris-Harrington principle is a true $Π_{2}$ Ramsey-theoretic statement unprovable in $P A$ , the first natural mathematical (rather than metamathematical) example, with unprovability shown by the $ε_{0}$ -recursion bounding $P A$ 's provably total functions. It instantiates this unit's general theorem in everyday combinatorics rather than in self-referential coding.

Historical & philosophical context Master

Kurt Gödel proved both incompleteness theorems in Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I (1931), constructing the proof predicate by arithmetising the syntax of Principia Mathematica via primitive recursive functions and the $β$ -function, building the self-referential sentence by the diagonal construction, and stating the second theorem (the unprovability of consistency) with only a sketch, the full proof of the derivability conditions being deferred ^{[Enderton §3.4]}. David Hilbert and Paul Bernays supplied the detailed derivability conditions and the formalised second theorem in Grundlagen der Mathematik II (1939), and Martin Hilbert Löb proved the theorem now bearing his name in "Solution of a problem of Leon Henkin" (1955), answering whether a sentence asserting its own provability is provable ^{[Smoryński §1]}.

Alfred Tarski's undefinability of truth appeared in "Der Wahrheitsbegriff in den formalisierten Sprachen" (1936; Polish 1933), the semantic counterpart isolating that the obstruction is the indefinability of truth, not of provability ^{[Boolos-Burgess-Jeffrey Ch. 17]}. J. Barkley Rosser removed the $ω$ -consistency hypothesis in "Extensions of some theorems of Gödel and Church" (1936) with the ordered-proof predicate. The collapse of Hilbert's programme — a finitistic, internal consistency proof for a theory containing arithmetic — followed directly from the second theorem; Gerhard Gentzen's 1936 consistency proof of $P A$ by transfinite induction to $ε_{0}$ showed what an external proof must cost. Robert Solovay's "Provability interpretations of modal logic" (1976) identified the modal logic GL as the complete calculus of the provability operator, and Petr Hájek and Pavel Pudlák fixed the exact fragment ( $I Σ_{1}$ ) over which the derivability conditions and the second theorem hold ^{[Lindström Ch. 2]}.

Bibliography Master

@book{enderton2001logic,
  author    = {Enderton, Herbert B.},
  title     = {A Mathematical Introduction to Logic},
  edition   = {2},
  publisher = {Harcourt/Academic Press},
  year      = {2001}
}

@article{godel1931,
  author  = {G\"{o}del, Kurt},
  title   = {\"{U}ber formal unentscheidbare S\"{a}tze der {Principia Mathematica} und verwandter Systeme {I}},
  journal = {Monatshefte f\"{u}r Mathematik und Physik},
  volume  = {38},
  year    = {1931},
  pages   = {173--198}
}

@book{hilbertbernays1939,
  author    = {Hilbert, David and Bernays, Paul},
  title     = {Grundlagen der Mathematik II},
  publisher = {Springer},
  year      = {1939}
}

@article{lob1955,
  author  = {L\"{o}b, Martin H.},
  title   = {Solution of a problem of {Leon Henkin}},
  journal = {Journal of Symbolic Logic},
  volume  = {20},
  number  = {2},
  year    = {1955},
  pages   = {115--118}
}

@article{rosser1936,
  author  = {Rosser, J. Barkley},
  title   = {Extensions of some theorems of {G\"{o}del} and {Church}},
  journal = {Journal of Symbolic Logic},
  volume  = {1},
  number  = {3},
  year    = {1936},
  pages   = {87--91}
}

@incollection{tarski1936truth,
  author    = {Tarski, Alfred},
  title     = {Der Wahrheitsbegriff in den formalisierten Sprachen},
  journal   = {Studia Philosophica},
  volume    = {1},
  year      = {1936},
  pages     = {261--405}
}

@article{solovay1976,
  author  = {Solovay, Robert M.},
  title   = {Provability interpretations of modal logic},
  journal = {Israel Journal of Mathematics},
  volume  = {25},
  year    = {1976},
  pages   = {287--304}
}

@article{parisharrington1977,
  author  = {Paris, Jeff and Harrington, Leo},
  title   = {A mathematical incompleteness in {Peano} arithmetic},
  journal = {Handbook of Mathematical Logic},
  year    = {1977},
  pages   = {1133--1142}
}

@book{boolosburgessjeffrey2007,
  author    = {Boolos, George S. and Burgess, John P. and Jeffrey, Richard C.},
  title     = {Computability and Logic},
  edition   = {5},
  publisher = {Cambridge University Press},
  year      = {2007}
}

@book{lindstrom1997,
  author    = {Lindstr\"{o}m, Per},
  title     = {Aspects of Incompleteness},
  series    = {Lecture Notes in Logic 10},
  publisher = {Springer},
  year      = {1997}
}

@incollection{smorynski1977incompleteness,
  author    = {Smory\'{n}ski, Craig},
  title     = {The incompleteness theorems},
  booktitle = {Handbook of Mathematical Logic},
  editor    = {Barwise, Jon},
  publisher = {North-Holland},
  year      = {1977},
  pages     = {821--865}
}

Prerequisites

42.01.08

Tier anchors

beginner: Enderton 2001 *A Mathematical Introduction to Logic* 2e (Harcourt/Academic Press) §3.4-3.5 read informally — the idea that every sentence and every proof can be turned into a number by a fixed coding scheme, so that a theory of numbers can be made to talk about its own sentences and its own proofs; the trick of building a sentence that says, in coded form, 'I have no proof,' and the conclusion that such a sentence is true exactly when it is unprovable, so a consistent theory that can check its own proofs must leave some true statements unproved; the difference between a statement being true and a statement being provable, made concrete by one self-referential example
intermediate: Enderton 2001 *A Mathematical Introduction to Logic* 2e §3.4-3.5 (Gödel numbering / arithmetisation of syntax; the substitution function and the diagonal lemma — for every formula $\psi(x)$ a sentence $G$ with $T \vdash G \leftrightarrow \psi(\ulcorner G\urcorner)$; the provability predicate $\mathrm{Pr}_T$ from the representable proof predicate of §3.3; Gödel's first incompleteness theorem for consistent recursively axiomatised $T \supseteq Q$, via $\omega$-consistency and via Rosser's refinement to plain consistency; Tarski's undefinability of arithmetical truth; Gödel's second incompleteness theorem and the Hilbert-Bernays-Löb derivability conditions; the contrast with the completeness theorem)
master: Enderton 2001 *A Mathematical Introduction to Logic* 2e §3.4-3.5; Boolos, Burgess and Jeffrey 2007 *Computability and Logic* 5e (Cambridge) Ch. 17-18 (the diagonal lemma, the first and second incompleteness theorems, the derivability conditions); Smorynski 1977 'The incompleteness theorems' in the *Handbook of Mathematical Logic* (North-Holland) (the modal/derivability-condition treatment, Löb's theorem, provability logic GL); Hájek and Pudlák 1993 *Metamathematics of First-Order Arithmetic* (Springer) Ch. I, III (the formalised $\Sigma_1$-completeness and the second theorem inside $I\Sigma_1$); Lindström 1997 *Aspects of Incompleteness* (Springer) (the interpretability and reflection landscape, Rosser's trick, the structure of the $\Pi_1$/$\Sigma_1$ independent sentences)

References

Enderton, H. B. — A Mathematical Introduction to Logic · 2nd edition, Harcourt/Academic Press (2001), §3.4-3.5. Carries the arithmetisation of syntax to its destination in the incompleteness theorems. Fix a Gödel numbering $\ulcorner \cdot \urcorner$: an injective effective assignment of natural numbers to the symbols, terms, formulas, and finite sequences of formulas of the language of arithmetic $\mathcal{L}_A = \{0, S, +, \cdot, <\}$, built from a coding of finite sequences (the $\beta$-function of §3.3, or a prime-power coding $\langle a_0, \dots, a_n\rangle = \prod_i p_i^{a_i + 1}$). The numeral of the code of $\varphi$ is written $\ulcorner\varphi\urcorner$ as a closed term. The syntactic operations — 'is a formula,' 'is an axiom of $T$,' 'is a proof in $T$ of,' the substitution function $\mathrm{sub}(\ulcorner\varphi(x)\urcorner, n) = \ulcorner\varphi(\underline n)\urcorner$, and the diagonal function $d(\ulcorner\varphi(x)\urcorner) = \ulcorner\varphi(\underline{\ulcorner\varphi(x)\urcorner})\urcorner$ — are primitive recursive for any recursively axiomatised $T$, hence (§3.3) representable in $Q$. The PROOF PREDICATE $\mathrm{Prf}_T(p, x)$ ('$p$ codes a $T$-proof of the formula coded by $x$') is $\Delta_0$-representable, and the PROVABILITY PREDICATE $\mathrm{Pr}_T(x) = \exists p\,\mathrm{Prf}_T(p, x)$ is $\Sigma_1$. THE DIAGONAL (FIXED-POINT) LEMMA: for every formula $\psi(x)$ there is a sentence $G$ with $T \vdash G \leftrightarrow \psi(\ulcorner G\urcorner)$; proved by representing $\mathrm{sub}$ (or $d$) and self-applying. GÖDEL'S FIRST INCOMPLETENESS THEOREM: for $T$ consistent, recursively axiomatised, and extending $Q$, the Gödel sentence $G_T$ obtained from $\psi = \neg\mathrm{Pr}_T$ satisfies $T \vdash G_T \leftrightarrow \neg\mathrm{Pr}_T(\ulcorner G_T\urcorner)$; $T \nvdash G_T$ (using consistency) and $T \nvdash \neg G_T$ (using $\omega$-consistency), so $T$ is incomplete; $G_T$ is a true $\Pi_1$ sentence unprovable in $T$. ROSSER'S refinement replaces $\mathrm{Pr}_T$ by the Rosser provability predicate $\mathrm{Pr}_T^R(x) = \exists p\,(\mathrm{Prf}_T(p,x) \wedge \forall q \le p\,\neg\mathrm{Prf}_T(q, \mathrm{neg}(x)))$, giving incompleteness from plain consistency, no $\omega$-consistency needed. TARSKI'S UNDEFINABILITY OF TRUTH: the set $\#\mathrm{Th}(\mathfrak{N}) = \{\ulcorner\sigma\urcorner : \mathfrak{N} \models \sigma\}$ of (codes of) true arithmetic sentences is not definable by any $\mathcal{L}_A$-formula, by diagonalising a putative truth predicate to a Liar sentence. GÖDEL'S SECOND INCOMPLETENESS THEOREM: with $\mathrm{Con}_T := \neg\mathrm{Pr}_T(\ulcorner 0 = S0\urcorner)$, a consistent recursively axiomatised $T \supseteq Q$ (with enough induction, $T \supseteq I\Sigma_1$ or $PA$) does not prove $\mathrm{Con}_T$; the proof formalises the first theorem's 'if $T$ is consistent then $T \nvdash G_T$' as $T \vdash \mathrm{Con}_T \to G_T$, so $T \vdash \mathrm{Con}_T$ would give $T \vdash G_T$, contradiction. The HILBERT-BERNAYS-LÖB DERIVABILITY CONDITIONS on $\mathrm{Pr}_T$: (D1) $T \vdash \sigma \Rightarrow T \vdash \mathrm{Pr}_T(\ulcorner\sigma\urcorner)$; (D2) $T \vdash \mathrm{Pr}_T(\ulcorner\sigma \to \tau\urcorner) \to (\mathrm{Pr}_T(\ulcorner\sigma\urcorner) \to \mathrm{Pr}_T(\ulcorner\tau\urcorner))$; (D3) $T \vdash \mathrm{Pr}_T(\ulcorner\sigma\urcorner) \to \mathrm{Pr}_T(\ulcorner\mathrm{Pr}_T(\ulcorner\sigma\urcorner)\urcorner)$. LÖB'S THEOREM: $T \vdash \mathrm{Pr}_T(\ulcorner\sigma\urcorner) \to \sigma$ iff $T \vdash \sigma$; the second theorem is the case $\sigma = (0=S0)$. The consequence for Hilbert's programme: a finitistic consistency proof of a theory $\supseteq PA$ cannot be carried out inside that theory.
Boolos, G., Burgess, J. and Jeffrey, R. — Computability and Logic · 5th edition, Cambridge University Press (2007), Chapters 17-18. Ch. 17 ('Indefinability, Undecidability, Incompleteness') proves the diagonal lemma (there called the fixed-point or self-reference lemma), Tarski's theorem on the indefinability of truth, Church's theorem on the undecidability of first-order validity, and Gödel's first incompleteness theorem in the semantic form (a consistent, recursively axiomatised, true extension of $Q$ has a true unprovable sentence) and in the syntactic $\omega$-consistency form, with Rosser's strengthening to plain consistency via the Rosser sentence. Ch. 18 ('The Unprovability of Consistency') states the three Hilbert-Bernays-Löb derivability conditions, derives Gödel's second incompleteness theorem from them by formalising the first theorem, and proves Löb's theorem and its connection to the second theorem. The book is careful to separate the abstract diagonal argument (which needs only representability of substitution) from the arithmetical specifics, and to flag what hypotheses each theorem actually consumes — recursive axiomatisability for representability of the proof predicate, consistency for non-provability of $G_T$, $\omega$-consistency (or Rosser's trick) for non-refutability, and the derivability conditions for the second theorem.
Smoryński, C. — The incompleteness theorems · in J. Barwise (ed.), Handbook of Mathematical Logic, North-Holland (1977), pp. 821-865. The standard survey of the incompleteness phenomenon at the level of the derivability conditions and provability logic. Develops the arithmetised metamathematics abstractly: the provability predicate $\Box \sigma := \mathrm{Pr}_T(\ulcorner\sigma\urcorner)$ treated as a modal operator satisfying (D1) necessitation, (D2) distribution, and (D3) $\Box\sigma \to \Box\Box\sigma$, whence the diagonal lemma yields the Gödel sentence $G \leftrightarrow \neg\Box G$ and the Henkin sentence $H \leftrightarrow \Box H$. Proves Löb's theorem $\vdash \Box\sigma \to \sigma \Rightarrow \vdash \sigma$ (resolving Henkin's problem: $H$ is provable) and derives the second incompleteness theorem $\nvdash \mathrm{Con}_T$ as the instance $\sigma = \bot$. Surveys the provability logic GL (Gödel-Löb), whose axiom $\Box(\Box p \to p) \to \Box p$ is Löb's theorem and which Solovay's completeness theorem (1976) shows captures exactly the schematically $T$-provable facts about $\Box$, the modal calculus of provability. Also treats the independence of the consistency statement, the reflection principles $\mathrm{Pr}_T(\ulcorner\sigma\urcorner) \to \sigma$, the hierarchy of iterated consistency extensions, and the careful intensionality issues (the choice of proof predicate matters: a non-standard but extensionally correct $\mathrm{Pr}$, e.g. Rosser's or a Feferman provability predicate, can make $\mathrm{Con}_T$ provable, so the second theorem is sensitive to how consistency is formalised).
Lindström, P. — Aspects of Incompleteness · Lecture Notes in Logic 10, Springer (1997), Chapters 1-3. A monograph on the fine structure of incompleteness for recursively enumerable extensions of $PA$ (and of $I\Sigma_1$). Sets up the arithmetised provability predicate, the derivability conditions, and the diagonal lemma, then develops: the first and second incompleteness theorems with attention to the exact base theory needed; Rosser's theorem and the difference between the Gödel and Rosser sentences; the Gödel-Rosser and Ehrenfeucht-Feferman results on independent sentences; interpretability and the Orey-Hájek characterisation; reflection principles and their stratification; and the model-theoretic side (the existence of $\Pi_1$ and $\Sigma_1$ independent sentences, nonstandard models in which $\mathrm{Con}_T$ fails). The reference for the statement that the Gödel sentence is true and $\Pi_1$, that it is equivalent over the base theory to $\mathrm{Con}_T$, and for the precise hypotheses (recursive enumerability of the axioms, $\Sigma_1$-soundness or mere consistency) under which each form of the theorem holds.

Estimated time

beginner: 20m
intermediate: 55m
master: 92m