The Lumenary · First-year graduate

Gödel's incompleteness theorems

Name: ______________________

Date: ______________________

You will learn to

Explain how formulas and proofs are coded by natural numbers, and why provability in a recursively axiomatised theory is expressed by a $\Sigma_1$ formula
Prove the diagonal lemma and derive the first incompleteness theorem, in Rosser's form, for consistent recursively axiomatised theories extending Robinson arithmetic $\mathsf{Q}$
State the second incompleteness theorem with the derivability conditions, and Tarski's undefinability theorem, and explain precisely what they do and do not say
Derive incompleteness from the unsolvability of the halting problem
Explain why complete decidable theories such as Presburger arithmetic and real closed fields escape the theorems

1.
To which of these theories does the first incompleteness theorem (Rosser's form) apply, assuming each is consistent? Choose all that apply.
- A.Peano arithmetic $\mathsf{PA}$
- B. $\mathsf{ZFC}$
- C.Presburger arithmetic, the theory of $(\N, 0, 1, +)$
- D.True arithmetic $\mathrm{Th}(\N)$ , all sentences true in $\N$
- E.Robinson arithmetic $\mathsf{Q}$
2.
Code a string $s_1 s_2 \cdots s_k$ by $2^{c(s_1)} 3^{c(s_2)} 5^{c(s_3)} \cdots$ , with symbol codes $c(0) = 1$ , $c(=) = 5$ and $c(S) = 3$ . What is the Gödel number of the string $S0 = 0$ ?
3.
In Gödel's form of the first theorem, part (a) shows $T \nvdash G_T$ and part (b) shows $T \nvdash \neg G_T$ . Which hypothesis does part (b) need beyond those of part (a)?
- A. $\Sigma_1$ -soundness (or Gödel's $\omega$ -consistency)
- B.Consistency
- C.The induction schema
- D.Completeness
4.
Assume $\mathsf{PA}$ is consistent, and let $T' = \mathsf{PA} + G$ where $G$ is the Gödel sentence of $\mathsf{PA}$ . Which statements are true? Choose all that apply.
- A. $T'$ is complete.
- B. $T'$ is consistent.
- C. $T' \vdash \mathrm{Con}_{\mathsf{PA}}$ .
- D. $T' \vdash \mathrm{Con}_{T'}$ .
5.
Löb's theorem: if $T \vdash \mathrm{Prov}_T(\ulcorner\varphi\urcorner) \to \varphi$ , then $T \vdash \varphi$ (for $T \supseteq \mathsf{PA}$ recursively axiomatised). Apply it with $\varphi$ the sentence $0 = S0$ . What do you obtain?
- A.If $T$ is consistent, then $T \nvdash \mathrm{Con}_T$ : the second incompleteness theorem.
- B. $T$ is incomplete.
- C.Truth is not definable in arithmetic.
- D.Nothing: the hypothesis can never be met.
6.
In the Lean file, which statement correctly formalises the abstract form of Tarski's theorem for a diagonalisable system S (with hcompl and hdiag as hypotheses)?
- A.¬ S.Expressible (S.scode '' {s | S.True s})
- B.∃ s, S.True s ∧ ¬ S.Provable s
- C.¬ ∃ s, S.True s
- D.¬ S.Expressible (S.scode '' {s | S.Provable s})
7.
The Lean theorem halting_incompleteness has hypotheses hre : REPred Provable, hc : Computable nonHalt and sound. Which hypothesis expresses that the theory is recursively axiomatised?
- A.hre : REPred Provable
- B.hc : Computable nonHalt
- C.sound
8.
Write encode(codes), which sends a list of positive symbol codes $[c_1, \dots, c_k]$ to $2^{c_1} 3^{c_2} \cdots p_k^{c_k}$ , and decode(n), which recovers the list (and [] from 1). Why is decode(encode(xs)) == xs guaranteed?
Computational — Practice

Answer key — Gödel's incompleteness theorems

1.
$\mathsf{Q}$ , $\mathsf{PA}$ and $\mathsf{ZFC}$ . Presburger arithmetic is too weak (no multiplication), and true arithmetic is complete but not recursively axiomatisable — which is itself a corollary of the theorem.
2.
The codes are $3, 1, 5, 1$ , so the Gödel number is $2^3 \cdot 3^1 \cdot 5^5 \cdot 7^1 = 8 \cdot 3 \cdot 3125 \cdot 7 = 525\,000$ .
3.
If $T \vdash \neg G_T$ then $T \vdash \mathrm{Prov}_T(\ulcorner G_T\urcorner)$ . To derive a contradiction we need this $\Sigma_1$ sentence to be true, i.e. $T$ must be $\Sigma_1$ -sound (Gödel used $\omega$ -consistency). A consistent theory such as $\mathsf{PA} + \neg\mathrm{Con}_{\mathsf{PA}}$ proves false $\Sigma_1$ sentences, which is why Rosser's sentence was needed.
4.
$T'$ is consistent ( $\N \models T'$ ) and proves $\mathrm{Con}_{\mathsf{PA}}$ , since $\mathsf{PA} \vdash \mathrm{Con}_{\mathsf{PA}} \leftrightarrow G$ . But $T'$ is again subject to both theorems: it is incomplete and does not prove $\mathrm{Con}_{T'}$ . Incompleteness regenerates.
5.
With $\varphi = \bot$ , the hypothesis $T \vdash \mathrm{Prov}_T(\ulcorner\bot\urcorner) \to \bot$ says $T \vdash \mathrm{Con}_T$ , and the conclusion says $T \vdash \bot$ . So a consistent $T$ does not prove $\mathrm{Con}_T$ : the second incompleteness theorem is the special case $\varphi = \bot$ of Löb's theorem.
6.
tarski_undefinability concludes ¬ S.Expressible (S.scode '' {s | S.True s}): no formula defines the set of codes of true sentences. Provability, by contrast, is expressible — that difference is what separates truth from provability.
7.
hre : REPred Provable. If the axioms form a decidable set, the theorems can be listed by enumerating all proofs, so the set of (codes of) theorems is computably enumerable. The proof then combines this with Mathlib's theorem that non-halting is not computably enumerable.

def primes(k):
    found = []
    candidate = 2
    while len(found) < k:
        if all(candidate % p for p in found):
            found.append(candidate)
        candidate += 1
    return found


def encode(codes):
    n = 1
    for p, c in zip(primes(len(codes)), codes):
        n *= p ** c
    return n


def decode(n):
    codes = []
    k = 1
    while n > 1:
        p = primes(k)[-1]
        e = 0
        while n % p == 0:
            n //= p
            e += 1
        codes.append(e)
        k += 1
    return codes

Decoding works by unique prime factorisation: the exponents of $2, 3, 5, \dots$ in $n$ are determined by $n$ . Because every code is positive, the primes used are exactly the first $k$ , so the length is recovered too. This injectivity is all that arithmetisation needs from a coding.