Contents / Mathematical Logic / Incompleteness and Independence

Chapter 7

Incompleteness and Independence

Godel's incompleteness theorems, proof theory, forcing, and independence results in set theory.

Introduction

In 1928 Hilbert asked for a formal system for mathematics that would be consistent (it proves no contradiction), complete (it decides every sentence of its language), and decidable (an algorithm tells theorems from non-theorems), together with a finitary proof that it is consistent. Gödel's two theorems of 1931 destroyed the second and fourth demands at once, and Church and Turing finished off the third.

The argument is not a paradox and not a trick. It is a calculation. Syntax — formulas, substitution, proofs — is finite combinatorics, so it can be coded by numbers; a theory that can do elementary arithmetic can therefore talk about its own syntax; and once a theory can talk about its own proofs, a fixed-point construction hands it a sentence asserting its own unprovability. Everything in this chapter is a consequence of that one loop: code the syntax, represent the coding, diagonalise.

We build the loop in order. The first two sections do the labour nobody quotes — Gödel numbering, and the representability of recursive functions in a theory as weak as Robinson arithmetic $Q$ — and end with the diagonal lemma, proved. The next two sections cash it in: the first incompleteness theorem with its hypotheses stated exactly (Gödel's $ω$ -consistency, Rosser's improvement to bare consistency), then the second theorem via the Hilbert–Bernays–Löb derivability conditions, and Löb's theorem, which subsumes it. Tarski's undefinability of truth is the same diagonal argument with "provable" replaced by "true", and it explains why the first two theorems could not have been repaired by better axioms. The last two sections ask what remains: Gentzen's consistency proof for $PA$ and the ordinal $ε_{0}$ that measures it, and independence as a general phenomenon — Goodstein's theorem and Paris–Harrington in arithmetic, the continuum hypothesis in set theory.

Notation. Throughout, $L_{A}$ is the language of arithmetic with $0$ , the successor $S$ , $+$ , $\cdot$ and $\leq$ . $Q$ is Robinson arithmetic and $PA$ is Peano arithmetic. $T$ denotes a theory in $L_{A}$ (or one interpreting it) that is consistent and recursively axiomatised unless said otherwise. $T ⊢ φ$ means $φ$ is derivable in $T$ , and $T ⊬ φ$ that it is not. $N$ is the standard model, and $N ⊨ φ$ says $φ$ is true of the actual natural numbers.

7.1Coding Syntax as Arithmetic

A formal proof is a finite string of finite strings of symbols. Nothing about it is infinitary, so nothing about it resists being coded by a number — the same way a text file is a number in a machine. Gödel's first move is to fix such a coding and then check, laboriously, that the syntactic relations we care about become arithmetic relations of the codes.

Definition 7.1 (Gödel numbering). Fix an injective assignment of a positive integer $# s$ to each symbol $s$ of $L_{A}$ . The Gödel number of a finite string $s_{1} s_{2} \dots s_{k}$ is

┌ s_{1} \dots s_{k} ┐ = p_{1}^{# s_{1}} p_{2}^{# s_{2}} \dots p_{k}^{# s_{k}},

where $p_{i}$ is the $i$ -th prime. A finite sequence of strings $σ_{1}, \dots, σ_{m}$ is coded the same way one level up, as $p_{1}^{┌ σ_{1} ┐} \dots p_{m}^{┌ σ_{m} ┐}$ . A Gödel numbering is any such coding that is injective and for which the decoding operations — length, $i$ -th entry, concatenation — are primitive recursive.

Unique factorisation is what makes this work: from the number you recover the exponents, hence the symbols, hence the string. Any other effective coding would do as well, and nothing below depends on the choice; prime powers are simply the coding for which the verifications are easiest to write down.

Notation. The code $┌ φ ┐$ is a number. To feed it to a formula of $L_{A}$ we need a term, and we use the numeral $\overline{n} = S (S (\dots S (0) \dots))$ with $n$ occurrences of $S$ . We follow the standard abuse and write $┌ φ ┐$ inside a formula when the numeral $\overline{┌ φ ┐}$ is meant.

Pitfall. The distinction between the number $n$ and the numeral $\overline{n}$ looks like pedantry and is not. $n$ lives in the metatheory, where we count; $\overline{n}$ is a string of symbols inside the theory. The map $n \mapsto ┌ \overline{n} ┐$ — the code of the numeral of $n$ — is itself a primitive recursive function, and the derivability condition (D3) in the section on the second theorem is exactly the statement that the theory knows this map. Confusing the two makes the whole subject look circular, which it is not.

Definition 7.2 (Primitive recursive relation). The primitive recursive functions are the least class containing the zero function, the successor and the projections, and closed under composition and under primitive recursion, that is, definitions of the form $f (0, y) = g (y)$ and $f (n + 1, y) = h (n, f (n, y), y)$ . A relation is primitive recursive when its characteristic function is. Primitive recursive functions are computable, and the class is closed under bounded quantification and bounded search.

Theorem 7.3 (Arithmetisation of syntax). Let $T$ be a theory whose set of axiom codes $Ax_{T} = {┌ α ┐ : α an axiom of T}$ is primitive recursive. Then each of the following relations of codes is primitive recursive:

$Term (x)$ , $Fml (x)$ , $Sent (x)$ — " $x$ codes a term, a formula, a sentence";
$Sub (x, y, z)$ — the function returning the code of the result of substituting the numeral of $z$ for the variable coded by $y$ in the formula coded by $x$ ;
$Prf_{T} (x, y)$ — " $x$ codes a derivation in $T$ whose last line is the formula coded by $y$ ".

Proof. Sketch, with the shape of the induction given honestly. Each clause is a finite check on the decoded string, and the decoding operations are primitive recursive by unique factorisation. For $Fml$ : a formula is built in finitely many steps from atomic formulas, so $x$ codes a formula exactly when there exists a code $s < 2^{(x + 1)^{x + 1}}$ of a construction sequence each of whose entries is atomic or is obtained from earlier entries by $\neg$ , $\land$ or $\exists v$ . The bound is crude but explicit — every entry of a construction sequence for $x$ decodes to a substring of $x$ — and bounded existential quantification keeps us inside the primitive recursive class. $Sub$ is a primitive recursion on the length of the formula. For $Prf_{T}$ : $x$ must code a sequence whose every entry is either in $Ax_{T}$ , or a logical axiom (a decidable syntactic pattern), or follows from two earlier entries by modus ponens — a conjunction of bounded checks on the entries of $x$ , and $Ax_{T}$ is primitive recursive by hypothesis. The full verification is a long but entirely mechanical list; Boolos–Jeffrey–Burgess carries it out in detail, and nothing in it is more subtle than the $Fml$ case above.∎

The hypothesis on $Ax_{T}$ is where "recursively axiomatisable" earns its keep, and it is a genuine restriction: it says the axioms can be recognised, so that a purported proof can be checked. It is satisfied by $Q$ , $PA$ , $ZFC$ and every theory a mathematician actually writes down — including theories with infinitely many axioms, since an axiom scheme is recognisable by pattern. It fails, deliberately, for the theory whose axioms are all true sentences of arithmetic, and the section on Tarski's undefinability explains why that failure is unavoidable.

Definition 7.4 (The provability predicate). For $T$ as above, fix an $L_{A}$ -formula $Prf_{T} (x, y)$ defining the proof relation and set

Prov_{T} (y) \equiv \exists x Prf_{T} (x, y) .

We abbreviate $Prov_{T} (┌ φ ┐)$ by $□_{T} φ$ , read " $φ$ is provable in $T$ ". The consistency statement is $Con (T) \equiv \neg □_{T} (\overline{0} = \overline{1})$ .

Pitfall. $Prf_{T}$ is decidable; $Prov_{T}$ is not. The unbounded $\exists x$ is the whole difficulty of the subject. Checking a proof is mechanical; searching for one is not — the search halts on theorems and runs forever otherwise. Every asymmetry in this chapter, including the fact that the two halves of the first theorem need different hypotheses, traces back to that single unbounded quantifier.

Definition 7.5 ( $Σ_{1}$ and $Π_{1}$ formulas). A $Δ_{0}$ (bounded) formula is one all of whose quantifiers are bounded, of the form $\forall x \leq t$ or $\exists x \leq t$ . A $Σ_{1}$ formula is one of the form $\exists x θ (x, y)$ with $θ$ bounded; a $Π_{1}$ formula is the negation of one. A $Σ_{1}$ sentence asserts that a search terminates; a $Π_{1}$ sentence asserts that one never does.

By the theorem above, $Prov_{T} (y)$ is $Σ_{1}$ and $Con (T)$ is $Π_{1}$ . That classification is not bookkeeping — it is what the next theorem acts on.

Theorem 7.6 ( $Σ_{1}$ -completeness of $Q$ ). Let $σ$ be a $Σ_{1}$ sentence. If $N ⊨ σ$ then $Q ⊢ σ$ — and hence $T ⊢ σ$ for every theory $T$ extending $Q$ .

Proof. First, for a bounded sentence. $Q$ proves every true atomic sentence $\overline{m} + \overline{n} = \overline{m + n}$ and $\overline{m} \cdot \overline{n} = \overline{mn}$ , and decides every $\overline{m} = \overline{n}$ and $\overline{m} \leq \overline{n}$ correctly, by an induction carried out in the metatheory on $m$ and $n$ using the recursion axioms for $+$ and $\cdot$ and the axiom $S x = S y \to x = y$ . The connectives follow at once, and a bounded quantifier $\exists x \leq \overline{t}$ is a finite disjunction over $x = \overline{0}, \dots, \overline{t}$ , which $Q$ can assemble because it proves $x \leq \overline{t} \to (x = \overline{0} \lor \dots \lor x = \overline{t})$ . So $Q$ decides every bounded sentence, and decides it correctly.

Now let $σ = \exists x θ (x)$ be true, with $θ$ bounded. Then $θ (\overline{n})$ is a true bounded sentence for some witness $n \in N$ , so $Q ⊢ θ (\overline{n})$ by the previous paragraph, and existential generalisation gives $Q ⊢ \exists x θ (x)$ .∎

Intuition. $Σ_{1}$ -completeness says a theory as weak as $Q$ cannot miss a finite fact. If a proof really exists, or a computation really does halt, then the witness is a concrete number and exhibiting it is a finite calculation. No induction is needed: you are not reasoning about all numbers, only checking one. This is why incompleteness cannot be dodged by choosing a weaker theory — weakness does not protect you from what a single witness forces.

Example 7.7 (Coding a short string and a one-line derivation). Using $# (0) = 7$ and $# (=) = 5$ , compute the Gödel number of the string $0 = 0$ , and say what number codes the one-line derivation consisting of that formula alone.

Solution. The string $0 = 0$ has three symbols, with codes $7, 5, 7$ , so

┌ 0 = 0 ┐ = 2^{7} \cdot 3^{5} \cdot 5^{7} = 128 \cdot 243 \cdot 78125 = 2430000 000.

The one-line sequence containing just this formula is coded one level up as $2^{┌ 0 = 0 ┐} = 2^{2430000000}$ .

Sanity check: the second number is absurdly large, and that is exactly the point. Nothing in the argument asks these numbers to be small, only that they exist and that the arithmetic relating them is primitive recursive. $□$ □

Example 7.8 (Where $Con (T)$ sits, and what that buys). Classify $Con (T)$ in the arithmetical hierarchy, and read off what its negation would force.

Solution. $Con (T)$ is $\neg\exists x Prf_{T} (x, ┌ \overline{0} = \overline{1} ┐)$ , that is, $\forall x \neg Prf_{T} (x, ┌ \overline{0} = \overline{1} ┐)$ : one universal quantifier over a bounded matrix, so $Π_{1}$ .

Its negation is therefore $Σ_{1}$ , and Theorem $Σ_{1}$ -completeness of $Q$ applies to it: if $T$ (extending $Q$ ) were inconsistent, then $T$ would prove $\neg Con (T)$ , since a concrete contradiction supplies a concrete witness. Inconsistency is always eventually detectable; it is consistency — the $Π_{1}$ side — that resists certification. Every theorem in this chapter lives on that asymmetry. $□$ □

Exercises for §7.1 →

7.2Representability and the Diagonal Lemma

Coding syntax was a statement about the metatheory: we, outside, can compute with codes. Incompleteness needs more. The theory itself must be able to reason about those computations, and "able to" has a precise meaning.

Definition 7.9 (Robinson arithmetic $Q$ ). $Q$ is the finitely axiomatised $L_{A}$ -theory with axioms

S x \neq = 0, S x = S y \to x = y, x \neq = 0 \to \exists y (x = S y),

x + 0 = x, x + S y = S (x + y), x \cdot 0 = 0, x \cdot S y = x \cdot y + x,

x \leq y \leftrightarrow \exists z (z + x = y) .

$PA$ is $Q$ together with the induction scheme $(φ (0) \land \forall x (φ (x) \to φ (S x))) \to \forall x φ (x)$ , one instance for each $L_{A}$ -formula $φ$ (possibly with parameters).

$Q$ is very weak. It does not prove $\forall x (x + 0 = 0 + x)$ , nor that $\leq$ is transitive; it has no induction at all. That weakness is deliberate. Everything below holds for $Q$ , so incompleteness applies to every theory that interprets $Q$ — which is essentially every foundational theory ever proposed, and many that were designed to be modest.

Definition 7.10 (Representability). Let $T \supseteq Q$ . A relation $R \subseteq N^{k}$ is representable in $T$ if there is a formula $ρ (x_{1}, \dots, x_{k})$ with

R (n_{1}, \dots, n_{k}) ⟹ T ⊢ ρ (\overline{n_{1}}, \dots, \overline{n_{k}}), \neg R (n_{1}, \dots, n_{k}) ⟹ T ⊢ \neg ρ (\overline{n_{1}}, \dots, \overline{n_{k}}) .

A function $f : N^{k} \to N$ is representable if there is a formula $φ (x, y)$ such that for all $n$ ,

T ⊢ \forall y (φ (\overline{n_{1}}, \dots, \overline{n_{k}}, y) \leftrightarrow y = \overline{f (n)}) .

The second clause — that $T$ proves the value is unique — is what makes a representable function usable inside a derivation.

Intuition. Definability and representability are different demands. Definability asks that a formula pick out the right set in the standard model: a fact about $N$ . Representability asks that the theory settle each instance by proof, one numeral at a time. A theory can define a relation it knows almost nothing about; it can only represent a relation whose every instance it can check. That is why representability is the property the diagonal lemma needs, and why it is available already in $Q$ .

Theorem 7.11 (Representability of the recursive functions). Every recursive (total computable) function is representable in $Q$ , and every recursive relation is representable in $Q$ . Consequently all of $Fml$ , $Sub$ and $Prf_{T}$ from Theorem Arithmetisation of syntax are representable in $Q$ and in every theory extending it.

Proof. Sketch; the one genuinely non-obvious ingredient is isolated as a lemma below. Argue by induction on the generation of the recursive functions. The zero function, successor and projections are represented by $y = \overline{0}$ , $y = S x$ and $y = x_{i}$ . Composition is handled by composing the representing formulas and existentially quantifying the intermediate values, the uniqueness clause carrying through. Primitive recursion and minimisation are the real work: to represent $f$ defined by recursion, one must speak inside $L_{A}$ of the finite sequence $f (0, y), \dots, f (n, y)$ of previous values, and $L_{A}$ has no sequence variables and no exponentiation. Gödel's $β$ -function supplies the missing coding, and the rest is bookkeeping: express "there is a sequence coded by $(a, b)$ that starts correctly, obeys the recursion at each step, and has $y$ as its $n$ -th entry", and check the two clauses of representability using $Σ_{1}$ -completeness for the positive half and the $Q$ -axioms for the negative half. For minimisation, $f (y) = μx [g (y, x) = 0]$ is represented by " $g (y, x) = 0$ and $g (y, z) \neq = 0$ for all $z < x$ ", which is a bounded condition once the witness is named.∎

Lemma 7.12 (Gödel's $β$ -function). Define $β (a, b, i) = rem (a, 1 + (i + 1) b)$ , the remainder of $a$ on division by $1 + (i + 1) b$ . Then for every finite sequence $k_{0}, \dots, k_{n}$ of natural numbers there exist $a, b$ with $β (a, b, i) = k_{i}$ for all $i \leq n$ . Moreover $β$ is definable in $L_{A}$ using only $+$ and $\cdot$ .

Proof. Let $s = 1 + max (n, k_{0}, \dots, k_{n})$ and put $b = s!$ . The moduli $m_{i} = 1 + (i + 1) b$ for $i \leq n$ are pairwise coprime: a common prime divisor $p$ of $m_{i}$ and $m_{j}$ with $i < j \leq n$ would divide their difference $(j - i) b$ , and $p ∤ b$ (else $p ∣ m_{i} - (i + 1) b = 1$ ), so $p ∣ j - i$ ; but $j - i \leq n < s$ , so $j - i$ divides $b = s!$ , hence $p ∣ b$ — a contradiction. Each $k_{i}$ satisfies $k_{i} < s \leq b < m_{i}$ , so by the Chinese remainder theorem there is $a$ with $a \equiv k_{i} (mod m_{i})$ for every $i \leq n$ , and then $β (a, b, i) = k_{i}$ as required. Definability is immediate: $β (a, b, i) = r$ iff $\exists q (a = q \cdot (1 + (i + 1) b) + r \land r < 1 + (i + 1) b)$ , which uses nothing but $+$ , $\cdot$ and $\leq$ .∎

The $β$ -function is the whole reason incompleteness needs multiplication. With $+$ alone one gets Presburger arithmetic, which is consistent, complete and decidable — a standing reminder that the hypotheses of the first theorem are not decoration. Multiplication is what lets a first-order arithmetic theory encode finite sequences, and encoding finite sequences is what lets it encode proofs.

Pitfall. Presburger arithmetic is complete, and the theory of real closed fields (Tarski) is complete and decidable even though it is about an uncountable structure. Neither contradicts Gödel. Both fail the hypothesis "strong enough to represent the recursive functions": Presburger cannot multiply, and the reals cannot single out the integers. "Sufficiently strong" is a precise condition — interpreting $Q$ — not a vague gesture at size.

The fixed point

Everything is now in place for the construction that generates every theorem in this chapter.

Lemma 7.13 (Diagonal lemma). Let $T \supseteq Q$ . For every $L_{A}$ -formula $ψ (x)$ with exactly one free variable there is a sentence $φ$ such that

T ⊢ φ \leftrightarrow ψ (┌ φ ┐) .

Proof. Let $diag$ be the function on codes defined by

diag (┌ θ (x) ┐) = ┌ θ (\overline{┌ θ (x) ┐}) ┐,

that is: given the code of a formula with one free variable, substitute the numeral of its own code for that variable and return the code of the result. Set $diag (n) = 0$ for $n$ not coding such a formula. Substitution and the numeral map are primitive recursive by Theorem Arithmetisation of syntax, so $diag$ is recursive, and by Theorem Representability of the recursive functions there is a formula $D (x, y)$ representing it in $T$ ; in particular, for every $n$ ,

T ⊢ \forall y (D (\overline{n}, y) \leftrightarrow y = \overline{diag (n)}) . (*)

Now put

θ (x) \equiv \forall y (D (x, y) \to ψ (y)),

let $m = ┌ θ (x) ┐$ , and define $φ \equiv θ (\overline{m})$ , i.e. $\forall y (D (\overline{m}, y) \to ψ (y))$ . By the definition of $diag$ , $diag (m) = ┌ θ (\overline{m}) ┐ = ┌ φ ┐$ . Instantiating $(*)$ at $n = m$ gives

T ⊢ \forall y (D (\overline{m}, y) \leftrightarrow y = ┌ φ ┐) .

Reasoning inside $T$ : if $φ$ holds, then since $D (\overline{m}, ┌ φ ┐)$ holds, the universal statement $φ$ applied to $y = ┌ φ ┐$ yields $ψ (┌ φ ┐)$ . Conversely, if $ψ (┌ φ ┐)$ holds, then for any $y$ with $D (\overline{m}, y)$ we have $y = ┌ φ ┐$ and so $ψ (y)$ ; that is exactly $φ$ . Hence $T ⊢ φ \leftrightarrow ψ (┌ φ ┐)$ .∎

Figure 7.14. The diagonal. Row

i

is the formula

θ_{i} (x)

; column

j

supplies the numeral

\overline{j}

. Diagonalising means reading only the shaded diagonal, where a formula is applied to its own code — the one column no row can differ from everywhere.

Intuition. The lemma is often glossed as " $φ$ says of itself that $ψ$ ". Literally, $φ$ says nothing about itself: it is a sentence about numbers, asserting a numerical relation between $\overline{m}$ and whatever $D$ picks out. The self-reference is achieved, not assumed — it comes from the arithmetic fact that $diag$ maps $m$ to the code of the very sentence built from $m$ . Self-reference here is a computed coincidence of codes, not a semantic loop, which is why it produces theorems instead of paradoxes.

Pitfall. The diagonal lemma needs no assumption about $ψ$ whatsoever — not that it is $Σ_{1}$ , not that it is a provability predicate, not that it is true of anything. Applied to $ψ (x) \equiv$ " $x$ is provable" it gives a sentence asserting its own provability (Henkin's sentence, which by Löb's theorem is provable); applied to " $x$ is not provable" it gives Gödel's; applied to " $x$ is not true" it gives Tarski's. The theorem is the machine; the choice of $ψ$ is the input.

Example 7.15 (A sentence asserting its own refutability). Apply the diagonal lemma to $ψ (x) \equiv Prov_{T} (neg (x))$ , where $neg$ is the recursive function sending $┌ α ┐$ to $┌ \neg α ┐$ . What does the resulting sentence say, and what does consistency force about it?

Solution. The lemma gives $φ$ with $T ⊢ φ \leftrightarrow □_{T} \neg φ$ : "I am refutable".

Suppose $T ⊢ φ$ . Then by the equivalence $T ⊢ □_{T} \neg φ$ . That alone is not yet a contradiction — a theory can wrongly claim a proof exists — but if $T$ is $Σ_{1}$ -sound this claim is true, so $T ⊢ \neg φ$ as well, contradicting consistency. Hence $T ⊬ φ$ .

Suppose instead $T ⊢ \neg φ$ . Then a proof of $\neg φ$ exists, so $□_{T} \neg φ$ is a true $Σ_{1}$ sentence and $T$ proves it by Theorem $Σ_{1}$ -completeness of $Q$ ; the equivalence then gives $T ⊢ φ$ , contradicting consistency.

Sanity check: so $φ$ is another independent sentence, and note the asymmetry — the first half needed soundness, the second needed only consistency. This is the same asymmetry Rosser's trick removes in the next section. $□$ □

Example 7.16 (Why representability, not definability, is the hypothesis). Where exactly would the proof of the diagonal lemma break if $D$ merely defined $diag$ in $N$ rather than representing it in $T$ ?

Solution. The proof uses the displayed line $T ⊢ \forall y (D (\overline{m}, y) \leftrightarrow y = ┌ φ ┐)$ inside a derivation: both directions of the final equivalence are established by reasoning in $T$ . Mere definability gives only $N ⊨ \forall y (D (\overline{m}, y) \leftrightarrow y = ┌ φ ┐)$ , a fact about the standard model that $T$ may be unable to prove. We would then obtain $N ⊨ φ \leftrightarrow ψ (┌ φ ┐)$ — a semantic fixed point, enough for Tarski's undefinability theorem, which is a purely semantic result — but not the derivability we need for Gödel's theorems.

Sanity check: this matches the division of labour later in the chapter. Tarski's theorem will need only the semantic version and no assumption of recursive axiomatisability; Gödel's needs the provable version and therefore $T \supseteq Q$ . $□$ □

Exercises for §7.2 →

7.3The First Incompleteness Theorem

Apply the diagonal lemma to $ψ (x) \equiv \neg Prov_{T} (x)$ . The result is a sentence $G_{T}$ with

T ⊢ G_{T} \leftrightarrow \neg □_{T} G_{T},

the Gödel sentence of $T$ : "there is no proof of me in $T$ ". Both halves of incompleteness now follow, but — and this is the point most statements of the theorem blur — they do not follow from the same hypothesis.

Definition 7.17 ( $ω$ -consistency and $Σ_{1}$ -soundness). $T$ is $ω$ -consistent if there is no formula $θ (x)$ with $T ⊢ \exists x θ (x)$ and $T ⊢ \neg θ (\overline{n})$ for every $n \in N$ . $T$ is $Σ_{1}$ -sound if every $Σ_{1}$ sentence it proves is true in $N$ .

Every $ω$ -consistent theory is consistent, and every $Σ_{1}$ -sound theory is $ω$ -consistent; neither implication reverses.

Intuition. $ω$ -inconsistency is a theory talking itself into a witness it cannot name: it proves "something has property $θ$ " while refuting $θ$ of $\overline{0}$ , of $\overline{1}$ , of $\overline{2}$ , and so on forever. Such a theory is not contradictory — no single derivation exposes the clash, because exposing it would take infinitely many. It simply has no standard model: its "witness" must be a nonstandard element, sitting beyond every numeral. The extra strength Gödel needed for half of his theorem is precisely the ruling out of this situation.

Theorem 7.18 (Gödel's first incompleteness theorem). Let $T$ be a recursively axiomatised theory extending $Q$ , and let $G_{T}$ be its Gödel sentence.

If $T$ is consistent, then $T ⊬ G_{T}$ .
If $T$ is $ω$ -consistent, then $T ⊬ \neg G_{T}$ .

Hence an $ω$ -consistent, recursively axiomatised $T \supseteq Q$ is incomplete: $G_{T}$ is neither provable nor refutable in $T$ . If in addition $T$ is sound, $G_{T}$ is true in $N$ .

Proof. (1) Suppose $T ⊢ G_{T}$ . Then some finite derivation exists, so for the number $k$ coding it, $Prf_{T} (k, ┌ G_{T} ┐)$ holds in $N$ . This is a true bounded statement, so $T ⊢ Prf_{T} (\overline{k}, ┌ G_{T} ┐)$ by Theorem $Σ_{1}$ -completeness of $Q$ , whence $T ⊢ □_{T} G_{T}$ . But the fixed point gives $T ⊢ G_{T} \to \neg □_{T} G_{T}$ , and $T ⊢ G_{T}$ by assumption, so $T ⊢ \neg □_{T} G_{T}$ . Thus $T$ proves both $□_{T} G_{T}$ and its negation, so $T$ is inconsistent. Contrapositively, consistency gives $T ⊬ G_{T}$ . Note what this half used: only $Σ_{1}$ -completeness and consistency.

(2) Suppose $T ⊢ \neg G_{T}$ . By the fixed point, $T ⊢ □_{T} G_{T}$ , i.e. $T ⊢ \exists x Prf_{T} (x, ┌ G_{T} ┐)$ . Now $T$ is in particular consistent (being $ω$ -consistent), so by part (1) $T ⊬ G_{T}$ ; therefore no number codes a proof of $G_{T}$ , so for every $n$ the bounded sentence $\neg Prf_{T} (\overline{n}, ┌ G_{T} ┐)$ is true, and $T$ proves each of them by $Σ_{1}$ -completeness. So $T$ proves $\exists x Prf_{T} (x, ┌ G_{T} ┐)$ together with the refutation of every numerical instance — exactly $ω$ -inconsistency. Contrapositively, $ω$ -consistency gives $T ⊬ \neg G_{T}$ .

Truth. If $T$ is consistent then by (1) there is genuinely no $T$ -proof of $G_{T}$ ; that is precisely what $G_{T}$ asserts, so $N ⊨ G_{T}$ . (Consistency alone suffices for the truth claim; soundness is not needed for it, only for knowing that $T$ is consistent in the first place.)∎

Gödel's asymmetry bothered him, and Rosser removed it four years later by replacing "there is no proof of me" with a sentence that compares proofs against refutations.

Theorem 7.19 (Rosser's improvement). Let $T$ be a recursively axiomatised, consistent theory extending $Q$ . Let $R$ be a fixed point, obtained from the diagonal lemma, of

ψ (x) \equiv \forall p (Prf_{T} (p, x) \to \exists q \leq p Prf_{T} (q, neg (x))),

so that $T ⊢ R \leftrightarrow \forall p (Prf_{T} (p, ┌ R ┐) \to \exists q \leq p Prf_{T} (q, ┌ \neg R ┐))$ . Then $T ⊬ R$ and $T ⊬ \neg R$ . Consistency alone suffices; no $ω$ -consistency is required.

Proof. The Rosser sentence says: "for any proof of me, some earlier proof refutes me."

Suppose $T ⊢ R$ , with a derivation coded by $k$ . Since $T$ is consistent, $T ⊬ \neg R$ , so no $q$ codes a refutation; in particular $\forall q \leq \overline{k} \neg Prf_{T} (q, ┌ \neg R ┐)$ is a true bounded sentence and $T$ proves it. Also $T ⊢ Prf_{T} (\overline{k}, ┌ R ┐)$ . Instantiating the fixed point at $p = \overline{k}$ gives $T ⊢ \exists q \leq \overline{k} Prf_{T} (q, ┌ \neg R ┐)$ , contradicting the bounded sentence just proved. So $T ⊬ R$ .

Suppose instead $T ⊢ \neg R$ , with a derivation coded by $k$ . By the fixed point, $T ⊢ \exists p (Prf_{T} (p, ┌ R ┐) \land \forall q \leq p \neg Prf_{T} (q, ┌ \neg R ┐))$ . By consistency $T ⊬ R$ , so no $p$ codes a proof of $R$ ; $Q$ proves the trichotomy $p \leq \overline{k} \lor \overline{k} \leq p$ , so split on it. For $p \leq \overline{k}$ : each of the finitely many instances $\neg Prf_{T} (\overline{0}, ┌ R ┐), \dots, \neg Prf_{T} (\overline{k}, ┌ R ┐)$ is true and hence provable, killing that case. For $\overline{k} \leq p$ : the witness $q = \overline{k}$ satisfies $Prf_{T} (\overline{k}, ┌ \neg R ┐)$ and $\overline{k} \leq p$ , so the clause $\forall q \leq p \neg Prf_{T} (q, ┌ \neg R ┐)$ fails, killing that case too. Both cases are refuted in $T$ , contradicting consistency. So $T ⊬ \neg R$ .∎

Remark. The bounded quantifier $\exists q \leq p$ is the entire trick. It converts an unbounded claim about the existence of a refutation — which a theory can assert without justification — into a finite comparison of two proof codes, and finite comparisons are decided correctly by $Q$ . Rosser bought bare consistency with a bounded quantifier.

Corollary 7.20 (Essential incompleteness). No consistent, recursively axiomatised theory extending $Q$ is complete. In particular, adding $G_{T}$ (or $R$ ) as a new axiom does not help: the theory $T^{'} = T + G_{T}$ is again consistent, recursively axiomatised and extends $Q$ , so it has its own independent sentence $G_{T^{'}}$ .

Proof. Immediate from Theorem Rosser's improvement applied to the theory in question. For the second sentence, note that $T^{'}$ has a primitive recursive axiom set (the axioms of $T$ plus one more), so the hypotheses transfer verbatim; the resulting $G_{T^{'}}$ is a different sentence, because it is built from a different provability predicate.∎

Corollary 7.21 (True arithmetic is not axiomatisable). $Th (N)$ , the set of all sentences true in the standard model, is not recursively axiomatisable, and the set of its codes is not recursively enumerable.

Proof. $Th (N)$ is consistent, complete and extends $Q$ . If it were recursively axiomatisable it would contradict Corollary Essential incompleteness. For the second claim: were the set of codes recursively enumerable, it would itself serve as a recursive axiomatisation (a theory can be axiomatised by a recursively enumerable set, since one can replace it by a recursive one — Craig's trick — listing each axiom repeated as a conjunction of growing length).∎

Figure 7.22. The theorems of a consistent recursively axiomatised

T

sit strictly inside the truths of

N

G_{T}

is true and unprovable;

\neg G_{T}

is false and also unprovable — the gap between the two regions is what incompleteness measures.

Example 7.23 (Both $T + G_{T}$ and $T + \neg G_{T}$ are consistent). Take $T = PA$ , assumed consistent and sound. Show that $PA + \neg G_{PA}$ is consistent, and describe what its models look like.

Solution. By the theorem, $PA ⊬ G_{PA}$ . A theory that does not prove $φ$ is consistent with $\neg φ$ — otherwise $PA + \neg φ ⊢ ⊥$ would give $PA ⊢ φ$ by reductio. So $PA + \neg G_{PA}$ is consistent and, by completeness, has a model $M$ .

$M$ cannot be $N$ : $G_{PA}$ is true, so $\neg G_{PA}$ fails in the standard model. In $M$ there is an element $c$ satisfying $Prf_{PA} (c, ┌ G_{PA} ┐)$ , and $c$ is not any $\overline{n}$ — for each concrete $n$ , $PA$ refutes $Prf_{PA} (\overline{n}, ┌ G_{PA} ┐)$ . So $c$ is a nonstandard element, a "proof" of infinite length.

Sanity check: the theory $PA + \neg G_{PA}$ is consistent but not $ω$ -consistent, precisely as part (2) of the theorem predicts — it asserts a witness while refuting every numeral. Consistency and having a standard model are different properties, and this example is the cleanest place to see the gap. $□$ □

Pitfall. "Gödel proved there are true statements that cannot be proved" — full stop — is not the theorem. Unprovability is always relative to a theory. $G_{PA}$ is unprovable in $PA$ and entirely provable in $PA + Con (PA)$ , and in $ZFC$ , and in ordinary informal mathematics. There is no sentence that is unprovable simpliciter; every Gödel sentence is a sentence about a particular theory and dies with it.

Pitfall. Incompleteness is not a statement about "weird" self-referential sentences only. The next sections exhibit consistency statements, and then Goodstein's theorem and the Paris–Harrington principle: combinatorial statements, formulated without any reference to provability, that are independent of $PA$ for exactly the reasons this section developed.

Exercises for §7.3 →

7.4The Second Incompleteness Theorem and Löb

Part (1) of the first theorem is an argument of a very particular kind: it is finitary, short, and about codes. A theory strong enough to formalise arithmetic is strong enough to formalise that argument. What comes out the other side is the second incompleteness theorem — but only if the provability predicate behaves, inside $T$ , the way provability behaves outside it. The three conditions that pin this down are due to Hilbert and Bernays and were streamlined by Löb.

Definition 7.24 (Hilbert–Bernays–Löb derivability conditions). A provability predicate $□_{T}$ satisfies the derivability conditions if for all sentences $A$ , $B$ :

(D1) if $T ⊢ A$ then $T ⊢ □_{T} A$ ;
(D2) $T ⊢ □_{T} (A \to B) \to (□_{T} A \to □_{T} B)$ ;
(D3) $T ⊢ □_{T} A \to □_{T} □_{T} A$ .

(D1) is $Σ_{1}$ -completeness in disguise, and holds for any $T \supseteq Q$ . (D2) says $T$ knows that its own proofs are closed under modus ponens: given codes of proofs of $A \to B$ and of $A$ , concatenating them and appending one line yields a proof of $B$ , and that concatenation is a provably total recursive operation. (D3) is the delicate one: $T$ must prove the formalised $Σ_{1}$ -completeness — that any true $Σ_{1}$ sentence, $□_{T} A$ in particular, is provable. Verifying (D3) requires induction and so is available in $PA$ but not in $Q$ .

Pitfall. The second theorem, unlike the first, is intensional: it depends on how $Con (T)$ is written, not merely on which set of sentences $T$ is. Feferman exhibited a perfectly good $Σ_{1}$ definition of the axioms of $PA$ whose associated consistency statement is provable in $PA$ — it fails (D3) for the natural provability predicate. The derivability conditions are therefore part of the statement of the theorem, not background hygiene, and " $T$ cannot prove its own consistency" is shorthand for " $T$ cannot prove the consistency statement built from a provability predicate satisfying D1–D3".

Theorem 7.25 (Gödel's second incompleteness theorem). Let $T \supseteq PA$ be recursively axiomatised with a provability predicate satisfying (D1)–(D3). If $T$ is consistent, then

T ⊬ Con (T) .

Proof. The heart is the formalisation of part (1) of the first incompleteness theorem, which we do in the $□$ -calculus. Write $⊥$ for $\overline{0} = \overline{1}$ , so $Con (T) \equiv \neg □_{T} ⊥$ , and let $G$ be the Gödel sentence, $T ⊢ G \leftrightarrow \neg □_{T} G$ .

Claim: $T ⊢ Con (T) \to G$ . From the fixed point, $T ⊢ \neg G \to □_{T} G$ is not what we want; instead argue inside $T$ as follows. By (D1) applied to the fixed point, $T ⊢ □_{T} (G \to \neg □_{T} G)$ , and (D2) gives $T ⊢ □_{T} G \to □_{T} \neg □_{T} G$ . By (D3), $T ⊢ □_{T} G \to □_{T} □_{T} G$ . Now $T$ proves that from $□_{T} □_{T} G$ and $□_{T} \neg □_{T} G$ one gets $□_{T} ⊥$ , using (D2) on the tautology $□_{T} G \to (\neg □_{T} G \to ⊥)$ together with (D1). Chaining these, $T ⊢ □_{T} G \to □_{T} ⊥$ ; contrapositively $T ⊢ Con (T) \to \neg □_{T} G$ , and the fixed point turns the consequent into $G$ . This proves the claim.

Now suppose $T ⊢ Con (T)$ . Then modus ponens with the claim yields $T ⊢ G$ , contradicting part (1) of Theorem Gödel's first incompleteness theorem, which needed only the consistency of $T$ . Hence $T ⊬ Con (T)$ .

What is being taken on trust. Only the derivability conditions themselves, whose verification for $PA$ is a long induction over the formalised proof predicate rather than a conceptual difficulty; given (D1)–(D3), the argument above is complete as written.∎

Intuition. The second theorem is the first theorem, read by the theory instead of by us. We concluded "if $T$ is consistent then $G$ is unprovable, hence true". $T$ can follow that same reasoning about itself and reach "if I am consistent then $G$ ". What $T$ cannot do is discharge the antecedent. A consistent theory understands perfectly well what its own consistency would imply; it simply has no way to establish it.

Löb arrived at a strictly more general fact while answering a question of Henkin: what happens to a sentence that asserts its own provability? The answer turned out to govern the whole $□$ -calculus.

Theorem 7.26 (Löb's theorem). Let $T \supseteq PA$ satisfy (D1)–(D3), and let $A$ be any sentence. If

T ⊢ □_{T} A \to A, then T ⊢ A .

Proof. Assume $T ⊢ □_{T} A \to A$ . Apply the diagonal lemma to $ψ (x) \equiv Prov_{T} (x) \to A$ , obtaining a sentence $L$ with

T ⊢ L \leftrightarrow (□_{T} L \to A) . (1)

From (1), $T ⊢ L \to (□_{T} L \to A)$ , so by (D1) and (D2),

T ⊢ □_{T} L \to □_{T} (□_{T} L \to A) and T ⊢ □_{T} (□_{T} L \to A) \to (□_{T} □_{T} L \to □_{T} A) .

Chaining these gives $T ⊢ □_{T} L \to (□_{T} □_{T} L \to □_{T} A)$ , and (D3) supplies $□_{T} L \to □_{T} □_{T} L$ , so

T ⊢ □_{T} L \to □_{T} A . (2)

Composing (2) with the hypothesis $T ⊢ □_{T} A \to A$ yields $T ⊢ □_{T} L \to A$ , which by (1) is $T ⊢ L$ . Then (D1) gives $T ⊢ □_{T} L$ , and (2) gives $T ⊢ □_{T} A$ ; the hypothesis finally yields $T ⊢ A$ .∎

Corollary 7.27 (Gödel II from Löb). If $T \supseteq PA$ satisfies (D1)–(D3) and is consistent, then $T ⊬ Con (T)$ .

Proof. Take $A \equiv ⊥$ in Löb's theorem. Then $□_{T} ⊥ \to ⊥$ is exactly $Con (T)$ . If $T ⊢ Con (T)$ , Löb gives $T ⊢ ⊥$ , i.e. $T$ is inconsistent.∎

Remark. Löb's theorem answers Henkin's question at once: a sentence $H$ with $T ⊢ H \leftrightarrow □_{T} H$ satisfies $T ⊢ □_{T} H \to H$ , so $T ⊢ H$ . The self-asserting sentence is provable, while the self-denying one is independent. Read in modal terms, Löb's theorem is the axiom $□ (□ p \to p) \to □ p$ that distinguishes the provability logic $GL$ from ordinary modal logics; Solovay's completeness theorem says $GL$ proves exactly the schemes of $□_{PA}$ that $PA$ verifies.

Example 7.28 ( $PA + \neg Con (PA)$ is consistent). Show this, and explain why it does not show that $PA$ might be inconsistent.

Solution. By the second theorem $PA ⊬ Con (PA)$ , so as in the previous section $PA + \neg Con (PA)$ is consistent and has a model $M$ . In $M$ there is an element $c$ that $M$ believes codes a proof of $⊥$ . Since $PA$ is in fact consistent, no standard number does, so $c$ is nonstandard.

Why this is not alarming: the sentence $\neg Con (PA)$ is $Σ_{1}$ and false, and a consistent theory may perfectly well prove false $Σ_{1}$ sentences — it merely cannot be $Σ_{1}$ -sound while doing so. The model $M$ has a "proof of $⊥$ " of nonstandard length, which is not a proof at all in the metatheory's sense, because it has no last line reachable by finitely many steps.

Sanity check: the theory $PA + \neg Con (PA)$ proves its own inconsistency and is consistent. That pair of facts is the sharpest possible warning that " $T$ proves $φ$ " and " $φ$ is true" are different properties. $□$ □

Example 7.29 (Reflection is genuinely stronger). Define $PA_{0} = PA$ and $PA_{n + 1} = PA_{n} + Con (PA_{n})$ . Is this chain strictly increasing? Does it ever reach a complete theory?

Solution. Each $PA_{n + 1}$ is recursively axiomatised, extends $PA$ , and is consistent (if $PA_{n}$ is consistent then, being true in $N$ , so is $Con (PA_{n})$ , so the extension has a model). By the second theorem $PA_{n} ⊬ Con (PA_{n})$ , so the inclusion $PA_{n} ⊊ PA_{n + 1}$ is strict for every $n$ .

It never reaches completeness. The union $PA_{ω} = ⋃_{n} PA_{n}$ is still recursively axiomatised — to check an axiom, find the $n$ it came from — so Corollary Essential incompleteness applies to it, and the process can be continued into the transfinite. Turing and Feferman studied exactly these iterations along ordinal notations.

Sanity check: this confirms that incompleteness is not a shortage of axioms that a determined mathematician could fix. Every effective repair is itself incomplete, and the repairs pile up along the ordinals rather than terminating. $□$ □

Pitfall. "Gödel proved we can never know whether mathematics is consistent" overstates the theorem twice. First, the theorem is about what $T$ proves, not about what we can know: $Con (PA)$ is provable — in $ZFC$ , and by Gentzen's finitary-plus- $ε_{0}$ argument in the next section. Second, the limitation is self-reference, not difficulty. What no consistent theory can do is certify itself; certifying a weaker theory is routine, and that is the shape all real consistency proofs take.

Exercises for §7.4 →

7.5Tarski's Undefinability of Truth

Gödel's theorems say that provability in a theory outruns the theory. Tarski's theorem, proved with the same diagonal machine, says something sharper and purely semantic: truth in $N$ cannot even be expressed in the language of $N$ . Historically this came first in Tarski's thinking and is the cleaner statement, and it explains why incompleteness was never going to be repairable by cleverer axioms.

Definition 7.30 (Definability of a set of numbers). A set $S \subseteq N$ is definable in $N$ if there is an $L_{A}$ -formula $σ (x)$ with one free variable such that for every $n$ ,

n \in S ⟺ N ⊨ σ (\overline{n}) .

A formula $Tr (x)$ is a truth predicate for $L_{A}$ if for every $L_{A}$ -sentence $φ$ ,

N ⊨ Tr (┌ φ ┐) \leftrightarrow φ .

Equivalently, $Tr$ defines the set $# Th (N) = {┌ φ ┐ : N ⊨ φ}$ .

The displayed biconditional is Tarski's T-scheme, the minimal thing anyone would demand of a notion of truth: "snow is white" is true if and only if snow is white. The theorem says no formula of arithmetic can satisfy it for all of arithmetic.

Theorem 7.31 (Tarski's undefinability of truth). There is no $L_{A}$ -formula $Tr (x)$ such that $N ⊨ Tr (┌ φ ┐) \leftrightarrow φ$ for every $L_{A}$ -sentence $φ$ . Equivalently, $# Th (N)$ is not definable in $N$ .

Proof. Suppose such a $Tr$ existed. The semantic form of the diagonal lemma — the version established in the second example of the section on representability, which needs only that $diag$ is definable in $N$ , and no assumption about any theory — applied to $ψ (x) \equiv \neg Tr (x)$ yields a sentence $λ$ with

N ⊨ λ \leftrightarrow \neg Tr (┌ λ ┐) .

But the T-scheme for $φ = λ$ gives $N ⊨ Tr (┌ λ ┐) \leftrightarrow λ$ . Combining, $N ⊨ Tr (┌ λ ┐) \leftrightarrow \neg Tr (┌ λ ┐)$ , which is false outright — $N$ is a structure and every sentence has exactly one truth value in it. The assumption is untenable.∎

Intuition. The sentence $λ$ is the liar, "I am not true", built without any appeal to natural language. The liar in English is a puzzle because English is vague about what "true" means. Here nothing is vague: every formula of $L_{A}$ has a definite truth value in $N$ , so a formula satisfying the T-scheme would give the liar a definite truth value too, and the liar has none available. The contradiction therefore does not fall on the liar; it falls on the assumption that truth was definable. Gödel's theorem is what you get by making the same move with a predicate that is definable — provability — in which case no contradiction results and a genuine independent sentence appears instead.

Corollary 7.32 (Truth and provability come apart definably). For any consistent, recursively axiomatised $T \supseteq Q$ , the set $# {φ : T ⊢ φ}$ is definable in $N$ (indeed by a $Σ_{1}$ formula), while $# Th (N)$ is not definable at all. Hence the two sets differ, and no recursively axiomatised theory proves all and only the truths.

Proof. Definability of the theorem set is Definition The provability predicate together with Theorem Arithmetisation of syntax; undefinability of the truth set is Tarski's theorem. Two sets one of which is definable and the other not are certainly different sets.∎

That corollary re-derives the first incompleteness theorem — in weaker form, since it gives no explicit independent sentence and needs the soundness of $T$ to know the difference goes the informative way — from a purely semantic fact. It is worth seeing the three statements in one line: $# Th (N)$ is not recursively enumerable (Corollary True arithmetic is not axiomatisable), not definable (Tarski), while provability is both.

Theorem 7.33 (Partial truth predicates exist). For each $n \geq 1$ there is a $Σ_{n}$ formula $Tr_{Σ_{n}} (x)$ such that for every $Σ_{n}$ sentence $φ$ , $N ⊨ Tr_{Σ_{n}} (┌ φ ┐) \leftrightarrow φ$ . Truth is definable level by level, but not uniformly across all levels.

Proof. Sketch. Satisfaction for bounded formulas is a recursive relation of the code and the assignment — evaluating a $Δ_{0}$ formula on given numbers is a terminating computation — so it is definable by a $Σ_{1}$ (indeed $Δ_{1}$ ) formula using the $β$ -function of Lemma Gödel's $β$ -function to code assignments. Prefixing $n$ alternating quantifier blocks to this base case defines $Σ_{n}$ -truth by a $Σ_{n}$ formula. The construction cannot be made uniform in $n$ : a single formula covering every level would satisfy the full T-scheme, contradicting Tarski.∎

Remark. This is the precise sense in which Tarski's theorem is a hierarchy theorem rather than a prohibition. Each level of the arithmetical hierarchy has its truth defined one level up, so the hierarchy is strict and does not collapse. Truth for the whole language sits, so to speak, at level $ω$ — outside the language. Tarski's own resolution was exactly this: the truth predicate for a language belongs to a strictly richer metalanguage.

Example 7.34 (Why the liar does not break arithmetic). $N$ contains a sentence saying "I am not provable in $PA$ " and no sentence saying "I am not true". Explain the difference in one sentence of mathematics, not of philosophy.

Solution. Because $Prov_{PA}$ is an actual $L_{A}$ -formula while $Tr$ is not, the diagonal lemma can be applied to $\neg Prov_{PA}$ and cannot be applied to $\neg Tr$ .

Running the argument anyway shows what the difference costs. With provability: $G$ satisfies $N ⊨ G \leftrightarrow \neg □_{PA} G$ , and both sides can be true, since $PA$ genuinely fails to prove $G$ . No contradiction — we learn that $PA$ is incomplete. With truth: $λ$ would satisfy $N ⊨ λ \leftrightarrow \neg Tr (┌ λ ┐)$ and the T-scheme would force $Tr (┌ λ ┐)$ to agree with $λ$ , leaving no truth value. A contradiction — we learn that $Tr$ does not exist.

Sanity check: the asymmetry is exactly that provability, unlike truth, is a $Σ_{1}$ property of codes and can therefore be underdetermined without being incoherent. $□$ □

Example 7.35 (Definable but not by any single formula). Show that the set ${┌ φ ┐ : φ is Π_{1} and N ⊨ φ}$ is definable, and reconcile this with Tarski's theorem.

Solution. By Theorem Partial truth predicates exist there is a $Π_{1}$ formula defining $Π_{1}$ -truth; conjoin it with the (recursive, hence definable) predicate " $x$ codes a $Π_{1}$ sentence" to define the displayed set.

There is no tension. Tarski forbids one formula that works for every sentence of $L_{A}$ ; he permits a different formula at each syntactic level, of increasing quantifier complexity. The truth predicate for $Π_{1}$ sentences is itself $Π_{1}$ , hence is not a truth predicate for $Σ_{2}$ sentences, and so on up.

Sanity check: if these level-by-level predicates could be assembled into one, the arithmetical hierarchy would collapse to a finite level — and it does not, precisely because Tarski's theorem forbids the assembly. $□$ □

Pitfall. Undefinability of truth is not a claim that arithmetic sentences lack truth values, nor that truth is subjective, nor that $N$ is somehow incoherent. Every $L_{A}$ -sentence has a perfectly definite truth value in $N$ . What the theorem denies is that the collection of those values can be captured by a formula of the same language. It is a statement about expressive resources, not about reality.

Exercises for §7.5 →

7.6Proof Theory and Ordinal Analysis

Gödel's second theorem says a theory cannot certify itself. It does not say nothing can certify it. Gentzen proved $Con (PA)$ in 1936 from a base so weak it is uncontroversially finitary, plus exactly one transfinite principle: induction up to the ordinal $ε_{0}$ . Proof theory is the discipline that grew out of measuring, for each theory, how much of that principle is needed — and the measurement turns out to be an ordinal.

Definition 7.36 (Sequent calculus and the cut rule). A sequent $Γ \Rightarrow Δ$ asserts that the conjunction of $Γ$ implies the disjunction of $Δ$ . Besides axioms $A \Rightarrow A$ and one left and one right rule per connective, the calculus has the cut rule

\frac{Γ \Rightarrow Δ , A A , Γ ^{'} \Rightarrow Δ ^{'}}{Γ , Γ ^{'} \Rightarrow Δ , Δ ^{'}}

The formula $A$ , which appears in the premises and not in the conclusion, is the cut formula: it is the formal counterpart of proving a lemma and then using it.

Theorem 7.37 (Gentzen's Hauptsatz, cut elimination). Every derivation in the sequent calculus for first-order logic can be transformed into a cut-free derivation of the same end-sequent. Consequently a cut-free derivation has the subformula property: every formula occurring in it is a subformula of the end-sequent.

Proof. Sketch of the standard double induction, with the measures named. Given a topmost cut, one pushes it upwards past the rules that introduced the cut formula, replacing a cut on $A \land B$ or $\forall x A (x)$ by cuts on the smaller formulas $A$ , $B$ , $A (t)$ . The measure is the pair (degree of the cut formula, height of the derivation above the cut), ordered lexicographically, and each reduction step lowers it. Two cases are not mere bookkeeping: contraction on the cut formula forces a duplication of an entire subderivation, which is why the height can grow while the degree falls, and a cut on a quantified formula substitutes a term that may be large. Both are handled by the lexicographic ordering, since degree strictly falls in each. Iterating the reduction terminates — for propositional logic in elementary time, and in general with a tower-of-exponentials blow-up in size, which is unavoidable. The subformula property is then immediate by inspection of the remaining rules, each of which has every premise formula a subformula of its conclusion.∎

Corollary 7.38 (Consistency of pure logic). The empty sequent $\Rightarrow$ is not derivable in the sequent calculus for pure first-order logic.

Proof. If it were derivable, it would have a cut-free derivation by the Hauptsatz. By the subformula property, every formula in that derivation is a subformula of the end-sequent, which has none. So the derivation consists only of axioms $A \Rightarrow A$ containing no formulas at all — impossible, since every axiom contains one.∎

The same strategy applied to $PA$ runs into the induction rule, which does not eliminate. Gentzen's answer was to keep the reduction procedure and attach an ordinal to every derivation, so that the procedure decreases the ordinal even when it increases the size.

Definition 7.39 (Cantor normal form and $ε_{0}$ ). Every ordinal $α > 0$ has a unique Cantor normal form

α = ω^{α_{1}} \cdot c_{1} + \dots + ω^{α_{k}} \cdot c_{k}, α \geq α_{1} > α_{2} > \dots > α_{k},

with $c_{1}, \dots, c_{k}$ positive integers. The exponents are strictly smaller than $α$ itself except in the degenerate case $α = ω^{α}$ , and the ordinal $ε_{0}$ is the least $α$ for which that case occurs; equivalently,

ε_{0} = sup {ω, ω^{ω}, ω^{ω^{ω}}, \dots} .

Below $ε_{0}$ every ordinal therefore has a Cantor normal form whose exponents are strictly smaller than it, so the notation bottoms out and each such ordinal has a finite description: a finite tree of natural numbers. Comparison of two notations is primitive recursive.

Intuition. $ε_{0}$ is countable, and in fact recursive: you can write a short program that decides which of two notations below it is larger. Nothing about it is mysteriously large in the sense of cardinality. What is large is its well-ordering strength — the assertion that there is no infinite descending sequence of notations below $ε_{0}$ is a genuinely powerful combinatorial principle, and it is exactly the surplus that $PA$ lacks.

Definition 7.40 (Transfinite induction up to $α$ ). $TI (α)$ , for a recursive ordinal notation system, is the scheme

\forall β < α (\forall γ < β φ (γ) \to φ (β)) \to \forall β < α φ (β),

one instance for each formula $φ$ . Equivalently: the notations below $α$ admit no infinite strictly descending sequence.

Theorem 7.41 (Gentzen's consistency proof). $PRA + TI (ε_{0}) ⊢ Con (PA)$ , where $PRA$ is primitive recursive arithmetic — a finitary base theory with no unbounded quantifier induction.

Proof. Sketch; the ordinal assignment is the content and we state its properties rather than construct it. Assign to each $PA$ -derivation $d$ an ordinal notation $o (d) < ε_{0}$ , built from the nesting of cuts and induction inferences in $d$ ; the assignment is primitive recursive. Gentzen gives a reduction procedure $d \mapsto d^{'}$ applying to any derivation of the empty sequent, such that $d^{'}$ again derives the empty sequent and $o (d^{'}) < o (d)$ . Suppose $PA$ derived a contradiction, that is, the empty sequent; iterating the reduction from that derivation produces an infinite strictly descending sequence $o (d) > o (d^{'}) > o (d^{''}) > \dots$ of notations below $ε_{0}$ , contradicting $TI (ε_{0})$ . All of this — the assignment, the reduction, the checking of each step — is primitive recursive; the only non-finitary ingredient is the well-foundedness assumption itself.∎

Theorem 7.42 ( $ε_{0}$ is exactly right). $PA ⊢ TI (α)$ for every $α < ε_{0}$ , but $PA ⊬ TI (ε_{0})$ .

Proof. Sketch. The positive half is Gentzen's second paper: for each fixed $α < ε_{0}$ one proves $TI (α)$ inside $PA$ by an induction whose complexity grows with the height of $α$ 's notation, using ordinary induction on a formula built by the "jump" operation $φ \mapsto (\forall γ < β φ (γ))$ . The negative half follows from Theorem Gentzen's consistency proof plus Gödel's second theorem: $PRA$ is interpretable in $PA$ , so if $PA$ proved $TI (ε_{0})$ it would prove $Con (PA)$ , which it does not.∎

Definition 7.43 (Proof-theoretic ordinal). The proof-theoretic ordinal $∣ T ∣$ of a theory $T$ is the least recursive ordinal $α$ such that $TI (α)$ , over a weak base such as $PRA$ , proves $Con (T)$ ; equivalently (for the theories in use) the supremum of the ordinals whose well-ordering $T$ can prove.

The two theorems above say $∣ PA ∣ = ε_{0}$ , and this is the model for the whole subject. A selection of the known values:

theory	proof-theoretic ordinal
$PRA$ , $I Σ_{1}$	$ω^{ω}$
$PA$ , $ACA_{0}$	$ε_{0}$
$ATR_{0}$	$Γ_{0}$ , the Feferman–Schütte ordinal
$ID_{1}$	the Bachmann–Howard ordinal
$Π_{1}^{1} - CA_{0}$	$ψ_{0} (Ω_{ω})$ , the Takeuti–Feferman–Buchholz ordinal
$ZFC$	unknown; far beyond current notation systems

Pitfall. Gentzen's proof is often dismissed as circular — "he assumed induction to prove induction". He did not. $PA$ proves $TI (α)$ for every $α < ε_{0}$ and nothing beyond, while Gentzen uses $TI (ε_{0})$ and no unbounded induction otherwise. The assumption is strictly stronger in one direction and strictly weaker in others, which is why the proof is informative rather than trivial — and why Gödel's second theorem guarantees in advance that any such proof must use something $PA$ lacks.

Example 7.44 (Comparing two notations below $ε_{0}$ ). Which is larger, $ω^{ω + 1} \cdot 2 + ω^{3}$ or $ω^{ω + 1} + ω^{ω} \cdot 5$ ? Give the general rule your answer uses.

Solution. Compare Cantor normal forms lexicographically, term by term, first on exponents and then on coefficients. The leading exponent is $ω + 1$ in both, so compare leading coefficients: $2 > 1$ . Hence $ω^{ω + 1} \cdot 2 + ω^{3}$ is larger, and the remaining terms are irrelevant — any tail is absorbed by a larger leading term, since $ω^{ω + 1} + ω^{ω} \cdot 5 < ω^{ω + 1} \cdot 2$ .

Sanity check: this is exactly the comparison a primitive recursive program performs on the finite trees coding these notations, which is what Definition Cantor normal form and $ε_{0}$ claimed. The ordinals are infinite; the decision procedure is finite. $□$ □

Example 7.45 (Consistency strength is not interpretability). $PA + Con (PA)$ and $PA + \neg Con (PA)$ are both consistent. Which has the larger proof-theoretic strength, and what does the other one show?

Solution. $PA + Con (PA)$ is strictly stronger than $PA$ : it proves a $Π_{1}$ sentence $PA$ cannot, and its own consistency statement is again unprovable in it, so the tower continues.

$PA + \neg Con (PA)$ is consistent but proves a false $Π_{1}$ sentence, so it is not $Σ_{1}$ -sound and, in the ordering by true $Π_{1}$ consequences, it is not an advance on $PA$ at all — it is a detour into a theory with only nonstandard models. Consistency strength orders theories by what they can certify, and certifying a falsehood earns nothing.

Sanity check: this is why proof theorists measure theories by ordinals and by $Π_{1}$ consequences rather than by mere consistency. Consistency alone is too coarse to tell a stronger theory from a wrong one. $□$ □

Exercises for §7.6 →

7.7Independence as a Phenomenon

Gödel sentences are engineered. The obvious objection to them — that they are logicians' artefacts, and that no statement a working mathematician would write down is independent — survived until 1977, when Paris and Harrington produced a purely combinatorial sentence about finite sets that $PA$ cannot prove, and Kirby and Paris did the same for a statement about elementary number sequences. This section collects the concrete independent statements of arithmetic, then turns to set theory, where independence is the normal condition of the subject rather than an exotic incident.

Definition 7.46 (Independence). A sentence $φ$ is independent of a theory $T$ if $T ⊬ φ$ and $T ⊬ \neg φ$ . Equivalently, by the completeness theorem, there is a model of $T + φ$ and a model of $T + \neg φ$ .

Intuition. The model-theoretic reading is the useful one. Proving independence is never a matter of searching for proofs and failing; it is a matter of building two worlds in which $T$ holds and $φ$ differs. In arithmetic, the two worlds are $N$ and a nonstandard model, and the work goes into showing $PA$ cannot exclude the latter. In set theory, both worlds have to be built from a given one, which is what Gödel's constructible universe and Cohen's forcing are for.

Goodstein sequences

Definition 7.47 (Hereditary base- $n$ notation and the Goodstein sequence). Write $m$ in base $n$ , then rewrite every exponent in base $n$ , and repeat until only numbers $\leq n$ remain: this is the hereditary base- $n$ representation. For example $266 = 2^{8} + 2^{3} + 2 = 2^{2^{2^{2}}} + 2^{2 + 1} + 2$ hereditarily in base $2$ .

Let $B_{n} (m)$ be the number obtained by replacing every occurrence of $n$ in that representation by $n + 1$ . The Goodstein sequence starting at $m$ is

g_{2} = m, g_{n + 1} = B_{n} (g_{n}) - 1 if g_{n} > 0, g_{n + 1} = 0 otherwise .

Example 7.48 (The Goodstein sequence starting at 4). Compute the first several terms.

Solution. Hereditarily in base $2$ , $4 = 2^{2}$ . Bump to base 3 and subtract one: $3^{3} - 1 = 26$ . Hereditarily in base 3, $26 = 2 \cdot 3^{2} + 2 \cdot 3 + 2$ ; bump and subtract: $2 \cdot 4^{2} + 2 \cdot 4 + 2 - 1 = 41$ . Continuing,

4, 26, 41, 60, 83, 109, 139, 173, \dots

at bases $2, 3, 4, \dots$ The sequence keeps climbing; it first reaches $0$ at base $3 \cdot 2^{402653211} - 1$ , a number with over a hundred million digits.

Sanity check: bumping the base multiplies by a large factor while subtracting one removes almost nothing, so growth is exactly what a first look predicts — which is why the theorem below is surprising. $□$ □

Figure 7.49. The first eight terms of the Goodstein sequence from

4

. Nothing in the numerical behaviour hints at termination; the proof works instead with an ordinal attached to each term, which strictly decreases at every step.

Theorem 7.50 (Goodstein's theorem). For every starting value $m$ , the Goodstein sequence reaches $0$ after finitely many steps.

Proof. Replace $n$ by $ω$ throughout the hereditary base- $n$ representation of $g_{n}$ , obtaining an ordinal $α_{n} < ε_{0}$ — every such representation is a Cantor normal form with exponents built the same way, so this is well defined. Base-bumping does not change the ordinal: replacing every $n$ by $n + 1$ and then every $n + 1$ by $ω$ gives what replacing every $n$ by $ω$ gave. Subtracting $1$ strictly decreases it, since it strictly decreases the finite data at the bottom of the normal form while leaving the higher terms alone. So $α_{2} > α_{3} > α_{4} > \dots$ is a strictly descending sequence of ordinals below $ε_{0}$ . By $TI (ε_{0})$ — Definition Transfinite induction up to $α$ — no such sequence is infinite, so the process halts, and it can only halt at $0$ .∎

Theorem 7.51 (Kirby–Paris). Goodstein's theorem is not provable in $PA$ (assuming $PA$ consistent). Over a weak base it implies $Con (PA)$ , and $PA + TI (ε_{0})$ proves it.

Proof. Sketch of the direction that matters, resting on the previous section. The proof above is a faithful translation: Goodstein's theorem is, over $PRA$ , equivalent to the well-foundedness of the notations below $ε_{0}$ , because the ordinal attached to $g_{n}$ ranges over all such notations as $m$ varies and the sequence of steps mirrors the descent exactly. By Theorem $ε_{0}$ is exactly right, $PA$ does not prove that well-foundedness; by Theorem Gentzen's consistency proof, that well-foundedness yields $Con (PA)$ . So a $PA$ -proof of Goodstein's theorem would give $PA ⊢ Con (PA)$ , contradicting Theorem Gödel's second incompleteness theorem.∎

Paris–Harrington

Definition 7.52 (The strengthened finite Ramsey principle). Write $[X]^{n}$ for the $n$ -element subsets of $X$ . The Paris–Harrington principle $PH$ states: for all $n, k, c$ there is $N$ such that for every colouring of $[{0, 1, \dots, N}]^{n}$ with $c$ colours there is a homogeneous set $H \subseteq {0, \dots, N}$ with $∣ H ∣ \geq k$ and, additionally, $∣ H ∣ \geq min (H)$ — the set is relatively large.

The only difference from the finite Ramsey theorem, which $PA$ proves comfortably, is the clause $∣ H ∣ \geq min (H)$ . That single extra demand pushes the growth rate of the least such $N$ past every function $PA$ can prove total.

Theorem 7.53 (Paris–Harrington). $PH$ is true in $N$ but not provable in $PA$ . Over $PA$ it is equivalent to the $1$ -consistency of $PA$ — the statement that every $Σ_{1}$ sentence $PA$ proves is true.

Proof. Sketch. Truth follows from the infinite Ramsey theorem by a compactness argument. For unprovability, the function $N (n, k, c)$ is shown to dominate every $PA$ -provably total function: one checks that $PH$ lets one build, inside a nonstandard model, an initial segment closed under all $PA$ -provably recursive functions, which is then a model of $PA$ — so $PH$ proves $Con (PA)$ and more. The equivalence with $1$ -consistency is Paris and Harrington's original indicator-function argument.∎

Remark. Goodstein and Paris–Harrington are both $Π_{2}$ statements asserting that a process terminates, and both fail in $PA$ for the same underlying reason: their termination requires a well-ordering of type $ε_{0}$ , and $PA$ 's provably total functions are exactly those with growth rate below the $ε_{0}$ level of the fast-growing hierarchy. Independence in arithmetic is, in every known natural case, a statement about growth rates.

Independence in set theory

The arithmetic examples above are all independent of $PA$ and provable in $ZFC$ — they are settled once a little set theory is allowed. Set theory itself has independent statements that no natural strengthening settles, and the first of them is the oldest open problem on Hilbert's list.

Definition 7.54 (The continuum hypothesis). $CH$ is the statement $2^{ℵ_{0}} = ℵ_{1}$ : every infinite set of reals is either countable or of the same cardinality as $R$ .

Theorem 7.55 (Independence of $CH$ ). If $ZFC$ is consistent, then so are $ZFC + CH$ (Gödel, 1938) and $ZFC + \neg CH$ (Cohen, 1963). Hence $CH$ is independent of $ZFC$ .

Proof. Sketch of the strategy only; the machinery is developed in the set-theory chapter Independence & Forcing. Both halves build a model. Gödel's half restricts: the constructible universe $L$ , obtained by iterating the definable power set along the ordinals, is an inner model of $ZFC$ in which $CH$ — indeed $GCH$ — holds, by a condensation argument. Cohen's half extends: starting from a countable transitive model $M$ , one adds $ℵ_{2}^{M}$ new reals using a partial order of finite conditions whose countable chain condition guarantees no cardinal is collapsed, so the extension $M [G]$ satisfies $2^{ℵ_{0}} \geq ℵ_{2}$ and $CH$ fails. Note the relative form of the conclusion: neither half proves $ZFC$ consistent — by Gödel's second theorem nothing in $ZFC$ could — both only transport a model into another model.∎

Remark. Chapter Independence & Forcing in the set-theory subject develops all of this properly: forcing posets, dense sets, generic filters and the Rasiowa–Sikorski lemma, $P$ -names and the forcing theorem, the condensation lemma and $CH$ in $L$ , cardinal preservation under ccc forcing, and the large cardinal hierarchy that measures consistency strength above $ZFC$ . Read it for the machinery; what belongs here is only the observation that the machinery answers a question of the same kind as Gödel's — and that it, too, is a relative consistency result resting on Gödel's second theorem for its shape.

Pitfall. "Independent" does not mean "meaningless", "unknowable" or "neither true nor false". $CH$ is a definite statement about the standard universe of sets, on which set theorists hold and argue for positions; it is simply not settled by the particular axiom list $ZFC$ . Compare $PA$ and Goodstein's theorem: the theorem is independent of $PA$ and unambiguously true, as its two-line proof using $TI (ε_{0})$ shows. Independence is a relation between a sentence and a theory, never a property of the sentence alone.

Example 7.56 (Independence from a theory is not independence from a stronger one). List, for each of $G_{PA}$ , $Con (PA)$ , Goodstein's theorem and $CH$ , a theory that settles it — or say that none is known.

Solution. $G_{PA}$ and $Con (PA)$ : both are proved in $PA + Con (PA)$ (trivially for the second, and for the first by the claim inside the proof of the second incompleteness theorem, $PA ⊢ Con (PA) \to G_{PA}$ ); both are proved in $ZFC$ , which has a model of $PA$ to hand.

Goodstein's theorem. Proved in $PA + TI (ε_{0})$ , and in $ZFC$ .

$CH$ : no accepted theory settles it. Large cardinal axioms do not — forcing can change $CH$ while preserving them — and the candidate axioms that do settle it, such as $V = L$ (giving $CH$ ) or forcing axioms like $MM$ (giving $2^{ℵ_{0}} = ℵ_{2}$ ), are exactly what is under debate.

Sanity check: the arithmetic examples climb a single ladder of consistency strength and are settled a rung or two up; $CH$ does not sit on that ladder at all, since large cardinals raise consistency strength without deciding it. The two kinds of independence are genuinely different phenomena. $□$ □

Exercises for §7.7 →

Common Mistakes

"There are true statements that cannot be proved." Only relative to a fixed theory. $G_{T}$ is unprovable in $T$ and provable in $T + Con (T)$ , and every concrete independent statement in this chapter is proved somewhere — usually one rung up the consistency ladder.
Forgetting the hypotheses. Incompleteness needs $T$ consistent, recursively axiomatised, and interpreting $Q$ . Drop the second and $Th (N)$ is a complete "theory"; drop the third and Presburger arithmetic and the theory of real closed fields are complete and decidable. Neither is a counterexample.
Confusing consistency with $ω$ -consistency. Gödel's original second half needed $ω$ -consistency, and the gap is real: $PA + \neg Con (PA)$ is consistent but not $ω$ -consistent. Rosser's sentence is what reduces the hypothesis to bare consistency, by comparing proof codes with a bounded quantifier.
Treating the second theorem as extensional. " $T$ cannot prove its own consistency" depends on the provability predicate satisfying (D1)–(D3). Feferman's example shows that a differently formulated consistency statement for $PA$ is provable in $PA$ .
Thinking Gentzen contradicts Gödel. Gentzen proves $Con (PA)$ from $PRA + TI (ε_{0})$ , a theory that is not contained in $PA$ . Gödel's second theorem forbids only a proof inside $PA$ , and in fact predicts that any correct proof must use exactly such extra strength.
Reading Tarski as scepticism about truth. Undefinability says no $L_{A}$ -formula satisfies the T-scheme for all $L_{A}$ -sentences. Every arithmetic sentence still has a definite truth value, and truth is definable level by level in the arithmetical hierarchy.
Assuming self-reference is essential. Goodstein's theorem and the Paris–Harrington principle mention no codes and no provability. They are independent of $PA$ because of growth rates, and they are the standing refutation of the idea that incompleteness only touches sentences built to be awkward.
Confusing independence with undecidability. A sentence is independent of a theory; a set (or a decision problem) is undecidable. $CH$ is independent of $ZFC$ ; the halting problem is undecidable. The two words describe different objects and the coincidence of everyday usage is unfortunate.

About the practice questions. They check that you can carry out this chapter's computations correctly, and each one is graded on a single answer. They are not proof exercises: working through them confirms the mechanics, not that you could prove the results yourself. For that, re-read the statements above and try to reconstruct their proofs with the page closed.

Practice this chapter