Gödel's incompleteness theorems

MotivationH

Hilbert's question

In the 1920s David Hilbert proposed a programme for the foundations of mathematics: formalise each branch of mathematics in a precise axiomatic system, in which proofs are finite strings checkable by rule; show that the system is complete (every statement of its language is proved or refuted); and prove its consistency by "finitary" means that nobody could doubt. If it succeeded, mathematical truth would coincide with provability in a fixed, mechanically checkable system, and that system would certify its own reliability.

In 1931 Kurt Gödel showed that both hopes fail for any system strong enough to do elementary arithmetic — and the reason is not a defect of a particular axiom system but a structural fact. A theory whose proofs can be checked mechanically can talk about its own proofs, because syntax can be coded in arithmetic. A diagonal argument, of the same shape as Cantor's, then produces a sentence that says, in effect, "I am not provable".

Today every proof assistant, including the Lean system used throughout this curriculum, is a mechanical proof checker of exactly the kind Hilbert envisaged. The incompleteness theorems tell us what such systems can never do: there will always be true arithmetical statements that a given system does not prove, and a consistent system cannot prove its own consistency.

IntuitionH

The liar, tamed

The liar sentence "this sentence is false" is a paradox: it is true if and only if it is false. Gödel replaced truth by provability:

G \quad\text{says}\quad \text{“}G \text{ is not provable in } T\text{.”}

Now there is no paradox, only a dilemma. If $T$ proved $G$ , then $T$ would prove a sentence asserting its own unprovability — so (if $T$ proves only truths) $G$ would be both provable and false. Hence $T$ does not prove $G$ ; and that is exactly what $G$ says, so $G$ is true but unprovable in $T$ .

Two ingredients make this rigorous, and both are mathematics rather than philosophy:

Arithmetisation. Formulas and proofs are finite strings, so they can be coded by numbers. " $x$ is the code of a proof of the formula with code $y$ " becomes an arithmetical relation between numbers, which the theory can express.
Diagonalisation. A sentence cannot literally contain itself, but it can contain a description that evaluates to its own code — just as Cantor's diagonal sequence differs from the $n$ -th listed sequence at place $n$ .

The common shape of these diagonal arguments was isolated by F. William Lawvere (1969): if every map $A \to B$ is of the form $e(a, -)$ , then every map $f : B \to B$ has a fixed point. In the diagram, $\hat e(a, a') = e(a)(a')$ and the dashed map $g = f \circ \hat e \circ \Delta$ is the "diagonal"; if $g = e(a_0)$ then $b = e(a_0)(a_0)$ is a fixed point of $f$ .

Lawvere's fixed-point theorem: if

e : A \to B^A

is surjective, the diagonal map

g

equals

e(a_0)

, and

e(a_0)(a_0)

is a fixed point of

f

.

Cantor's theorem is the case $B = \{0, 1\}$ with $f$ = negation, which has no fixed point, so no surjection $A \to 2^A$ exists. Tarski's theorem is the case where $B$ is the set of truth values of sentences and $f$ is negation. Gödel's theorem is the case where negation is replaced by "not provable", which does have a fixed point — the Gödel sentence.

DefinitionsH

Theories, codes and representability

We work in first-order logic (see the completeness theorem) in the language $L_A = \{0, S, +, \times\}$ of arithmetic. The numeral of $n \in \N$ is the term $\overline{n} = S S \cdots S 0$ with $n$ copies of $S$ .

Definition— Robinson arithmetic and Peano arithmetic

Robinson arithmetic $\mathsf{Q}$ (R. M. Robinson, 1950) is the theory with the seven axioms

\begin{aligned} &Sx \neq 0, \qquad Sx = Sy \to x = y, \qquad x \neq 0 \to \exists y\, (x = Sy),\\ &x + 0 = x, \qquad x + Sy = S(x + y), \qquad x \times 0 = 0, \qquad x \times Sy = (x \times y) + x . \end{aligned}

We write $x \le y$ for $\exists v\,(v + x = y)$ . Peano arithmetic $\mathsf{PA}$ is $\mathsf{Q}$ together with the induction schema $\big(\varphi(0) \wedge \forall x\,(\varphi(x) \to \varphi(Sx))\big) \to \forall x\, \varphi(x)$ for every formula $\varphi$ . $\mathsf{Q}$ has no induction at all; it cannot even prove $\forall x\,(0 + x = x)$ .

Definition— consistent, complete, recursively axiomatised

A theory $T$ (a set of sentences, closed under consequence when convenient) is consistent if it proves no sentence together with its negation, and complete if for every sentence $\varphi$ of its language, $T \vdash \varphi$ or $T \vdash \neg\varphi$ . It is recursively axiomatised if it has a decidable set of axioms (after coding sentences by numbers, below). Then the set of theorems of $T$ is computably enumerable: list all finite sequences of formulas and keep those that are proofs.

Definition— Gödel numbering

Fix an injective coding of the symbols by positive integers, $c(\cdot)$ , and code a string $s_1 s_2 \cdots s_k$ by $\ulcorner s_1 \cdots s_k \urcorner = 2^{c(s_1)} 3^{c(s_2)} \cdots p_k^{c(s_k)}$ , where $p_k$ is the $k$ -th prime. A proof — a finite sequence of formulas — is coded by coding the sequence of the codes of its formulas the same way. The coding is injective and computable in both directions.

Definition— Δ₀ and Σ₁ formulas

A formula is $\Delta_0$ if all its quantifiers are bounded, $\forall x \le t$ or $\exists x \le t$ ; it is $\Sigma_1$ if it has the form $\exists \bar x\, \theta$ with $\theta$ in $\Delta_0$ , and $\Pi_1$ if it has the form $\forall \bar x\, \theta$ . The truth of a $\Delta_0$ sentence in $\N$ can be decided by a finite search.

Definition— representability

A relation $R \subseteq \N^k$ is represented in $T$ by a formula $\varphi(\bar x)$ if for all $\bar n$ : when $R(\bar n)$ holds, $T \vdash \varphi(\overline{n_1}, \dots, \overline{n_k})$ , and when it fails, $T \vdash \neg\varphi(\overline{n_1}, \dots, \overline{n_k})$ . A function $f : \N^k \to \N$ is represented by $\varphi(\bar x, y)$ if for all $\bar n$ : $T \vdash \forall y\, \big(\varphi(\bar{\overline{n}}, y) \leftrightarrow y = \overline{f(\bar n)}\big)$ .

Three facts carry the technical weight. Their proofs are long but elementary; full treatments are in Smith (2013, chapters 11–20) and Boolos, Burgess and Jeffrey (2007, chapters 15–17).

Theorem— Fact A (Σ₁-completeness of Q)

Every $\Sigma_1$ sentence that is true in $\N$ is provable in $\mathsf{Q}$ . Moreover, for each $n$ , $\mathsf{Q} \vdash \forall x\,\big(x \le \overline{n} \to x = \overline{0} \vee \cdots \vee x = \overline{n}\big)$ and $\mathsf{Q} \vdash \forall x\,(x \le \overline{n} \vee \overline{n} \le x)$ .

Theorem— Fact B (representability)

Every decidable relation and every computable total function on $\N$ is representable in $\mathsf{Q}$ , hence in every consistent theory extending $\mathsf{Q}$ .

Theorem— Fact C (arithmetisation of proof)

If $T$ is recursively axiomatised, the relation " $m$ is the code of a $T$ -proof of the formula with code $n$ " is decidable (indeed primitive recursive, after replacing the axioms by an equivalent primitive recursive set — Craig's trick). Hence it is represented in $\mathsf{Q}$ by a formula $\mathrm{Prf}_T(x, y)$ that also defines it in $\N$ and can be chosen to be $\Sigma_1$ . Then $\mathrm{Prov}_T(y) := \exists x\, \mathrm{Prf}_T(x, y)$ is a $\Sigma_1$ formula, true in $\N$ of exactly the codes of theorems of $T$ .

Worked examplesH

Examples and non-examples

Example— Theories the theorems apply to

$\mathsf{Q}$ , $\mathsf{PA}$ , second-order arithmetic, and $\mathsf{ZFC}$ (which interprets $\mathsf{PA}$ by taking the finite von Neumann ordinals as numbers) are all recursively axiomatised and — we believe — consistent. Each is therefore incomplete, and none proves its own consistency. Adding the Gödel sentence as a new axiom does not help: $T + G_T$ is again recursively axiomatised and consistent, and has its own Gödel sentence.

Example— Complete theories: not enough arithmetic

Presburger arithmetic, the theory of $(\N, 0, 1, +)$ , is complete and decidable (Presburger, 1929, by quantifier elimination). Multiplication is not definable in it — the formal section cites Mathlib's proof of this.
The theory of real closed fields — the first-order theory of $(\R, 0, 1, +, \times, <)$ — is complete and decidable (Tarski, published 1948 and 1951). The integers are not definable in $\R$ by a first-order formula, so arithmetic cannot be interpreted.
True arithmetic $\mathrm{Th}(\N)$ , the set of all sentences true in $\N$ , is complete and consistent — but by the first incompleteness theorem it is not recursively axiomatisable (indeed, by Tarski's theorem it is not even arithmetically definable).

Example— A Gödel number

With symbol codes $c(0) = 1$ , $c(S) = 3$ and $c(=) = 5$ , the string " $S0$ " has code $2^3 \cdot 3^1 = 24$ , and " $0 = 0$ " has code $2^1 \cdot 3^5 \cdot 5^1 = 2430$ . Any injective computable coding would serve; the experiment below uses a bijective base- $k$ coding instead.

ProofH

The diagonal lemma and the first theorem

Throughout, $T$ is a recursively axiomatised theory extending $\mathsf{Q}$ .

Theorem— Diagonal lemma (Gödel 1931; Carnap 1934)

For every formula $\varphi(y)$ with one free variable there is a sentence $G$ such that

\mathsf{Q} \vdash G \leftrightarrow \varphi(\ulcorner G \urcorner),

where $\ulcorner G \urcorner$ abbreviates the numeral of the code of $G$ .

Proof

Let $\mathrm{diag} : \N \to \N$ send the code of a formula $\theta(x)$ to the code of the sentence $\theta(\overline{\ulcorner \theta \urcorner})$ , and every other number to $0$ . It is computable, so by Fact B some formula $D(x, y)$ represents it in $\mathsf{Q}$ :

\mathsf{Q} \vdash \forall y\,\big(D(\overline{n}, y) \leftrightarrow y = \overline{\mathrm{diag}(n)}\big) \quad\text{for every } n.

Put $\psi(x) := \exists y\,\big(D(x, y) \wedge \varphi(y)\big)$ , let $n = \ulcorner \psi \urcorner$ and let $G := \psi(\overline{n})$ . By definition $\mathrm{diag}(n) = \ulcorner G \urcorner$ . Reasoning in $\mathsf{Q}$ ,

G \;\leftrightarrow\; \exists y\,\big(D(\overline{n}, y) \wedge \varphi(y)\big) \;\leftrightarrow\; \exists y\,\big(y = \ulcorner G \urcorner \wedge \varphi(y)\big) \;\leftrightarrow\; \varphi(\ulcorner G \urcorner). \qquad\blacksquare

∎

Applying the lemma to $\neg\mathrm{Prov}_T(y)$ gives a Gödel sentence $G_T$ with $\mathsf{Q} \vdash G_T \leftrightarrow \neg\mathrm{Prov}_T(\ulcorner G_T \urcorner)$ .

Theorem— First incompleteness theorem, Gödel's form

(a) If $T$ is consistent, then $T \nvdash G_T$ . (b) If moreover $T$ is $\Sigma_1$ -sound (every $\Sigma_1$ sentence it proves is true in $\N$ ), then $T \nvdash \neg G_T$ . Consequently $G_T$ is true in $\N$ but not provable in $T$ .

Proof

(a) Suppose $m$ codes a $T$ -proof of $G_T$ . By Fact C, $\mathsf{Q} \vdash \mathrm{Prf}_T(\overline{m}, \ulcorner G_T \urcorner)$ , so $T \vdash \mathrm{Prov}_T(\ulcorner G_T \urcorner)$ , and by the diagonal equivalence $T \vdash \neg G_T$ . Then $T$ is inconsistent.

(b) If $T \vdash \neg G_T$ , then $T \vdash \mathrm{Prov}_T(\ulcorner G_T \urcorner)$ , a $\Sigma_1$ sentence; by $\Sigma_1$ -soundness it is true, so $T \vdash G_T$ , and $T$ is inconsistent, contradicting (a).

Finally, $\mathsf{Q}$ is true in $\N$ , so the diagonal equivalence holds in $\N$ ; since $T \nvdash G_T$ , the sentence $\neg\mathrm{Prov}_T(\ulcorner G_T \urcorner)$ is true in $\N$ , hence so is $G_T$ .

∎

Gödel's original hypothesis for (b) was $\omega$ -consistency, which implies $\Sigma_1$ -soundness. J. Barkley Rosser (1936) removed it with a cleverer sentence: "if I am provable, there is a shorter proof of my negation".

Theorem— First incompleteness theorem, Rosser's form

If $T$ is a consistent, recursively axiomatised theory extending $\mathsf{Q}$ , then $T$ is incomplete: there is a sentence $R$ with $T \nvdash R$ and $T \nvdash \neg R$ .

Proof

Let $\mathrm{neg}$ be the computable function $\ulcorner \chi \urcorner \mapsto \ulcorner \neg\chi \urcorner$ , and write $\mathrm{Prf}_T(z, \mathrm{neg}(y))$ for the formula expressing this via a representing formula (Fact B). By the diagonal lemma there is a sentence $R$ with

T \vdash R \leftrightarrow \forall x\,\Big(\mathrm{Prf}_T(x, \ulcorner R \urcorner) \to \exists z \le x\; \mathrm{Prf}_T(z, \ulcorner \neg R \urcorner)\Big).

$T \nvdash R$ . Suppose $m$ codes a proof of $R$ . As $T$ is consistent, no number codes a proof of $\neg R$ , so by Fact C, $T \vdash \neg\mathrm{Prf}_T(\overline{k}, \ulcorner \neg R \urcorner)$ for each $k \le m$ . By Fact A, every $z \le \overline{m}$ is one of $\overline{0}, \dots, \overline{m}$ , so $T \vdash \neg\exists z \le \overline{m}\, \mathrm{Prf}_T(z, \ulcorner \neg R \urcorner)$ . Together with $T \vdash \mathrm{Prf}_T(\overline{m}, \ulcorner R \urcorner)$ (take $x = \overline{m}$ ) this gives $T \vdash \neg R$ , contradicting consistency.

$T \nvdash \neg R$ . Suppose $m$ codes a proof of $\neg R$ , so $T \vdash \mathrm{Prf}_T(\overline{m}, \ulcorner \neg R \urcorner)$ . As $T$ is consistent, $T \nvdash R$ , so $T \vdash \neg\mathrm{Prf}_T(\overline{k}, \ulcorner R \urcorner)$ for each $k \le m$ . Now argue inside $T$ : let $x$ satisfy $\mathrm{Prf}_T(x, \ulcorner R \urcorner)$ . By Fact A, $x \le \overline{m}$ or $\overline{m} \le x$ . The first case is impossible, since then $x$ is one of $\overline{0}, \dots, \overline{m}$ ; so $\overline{m} \le x$ , and $z = \overline{m}$ witnesses $\exists z \le x\; \mathrm{Prf}_T(z, \ulcorner \neg R \urcorner)$ . Hence $T \vdash R$ , again contradicting consistency.

With more care in the choice of $\mathrm{Prf}_T$ , the Rosser sentence can be taken to be (equivalent to) a $\Pi_1$ sentence, like the Gödel sentence.

∎

ProofH

The second theorem, and Tarski

Let $\mathrm{Con}_T$ be the sentence $\neg\mathrm{Prov}_T(\ulcorner 0 = S0 \urcorner)$ , with $\mathrm{Prov}_T$ the standard $\Sigma_1$ provability formula of Fact C. When $T$ extends $\mathsf{PA}$ , it satisfies the Hilbert–Bernays–Löb derivability conditions: for all sentences $\varphi, \psi$ ,

D1 if $T \vdash \varphi$ then $T \vdash \mathrm{Prov}_T(\ulcorner \varphi \urcorner)$ ;
D2 $T \vdash \mathrm{Prov}_T(\ulcorner \varphi \to \psi \urcorner) \to \big(\mathrm{Prov}_T(\ulcorner \varphi \urcorner) \to \mathrm{Prov}_T(\ulcorner \psi \urcorner)\big)$ ;
D3 $T \vdash \mathrm{Prov}_T(\ulcorner \varphi \urcorner) \to \mathrm{Prov}_T(\ulcorner \mathrm{Prov}_T(\ulcorner \varphi \urcorner) \urcorner)$ .

D1 is Fact A applied to a true $\Sigma_1$ sentence; D2 formalises modus ponens; D3, the hard one, is the formalisation inside $\mathsf{PA}$ of Fact A itself (it needs induction; see Boolos 1993, chapter 2).

Theorem— Second incompleteness theorem (Gödel 1931; Hilbert–Bernays 1939)

If $T$ is consistent, recursively axiomatised and extends $\mathsf{PA}$ , then $T \nvdash \mathrm{Con}_T$ .

Proof

Write $\square\varphi$ for $\mathrm{Prov}_T(\ulcorner \varphi \urcorner)$ , $\bot$ for $0 = S0$ and $G$ for $G_T$ , so $T \vdash G \leftrightarrow \neg\square G$ .

From $T \vdash \square G \to \neg G$ , by D1 and D2: $T \vdash \square\square G \to \square\neg G$ .
By D3: $T \vdash \square G \to \square\square G$ ; so $T \vdash \square G \to \square\neg G$ .
Since $T \vdash G \to (\neg G \to \bot)$ , D1 and D2 (twice) give $T \vdash \square G \to (\square\neg G \to \square\bot)$ .
From 2 and 3: $T \vdash \square G \to \square\bot$ ; contrapositively $T \vdash \neg\square\bot \to \neg\square G$ , that is, $T \vdash \mathrm{Con}_T \to G$ .

If $T \vdash \mathrm{Con}_T$ , then $T \vdash G$ , contradicting part (a) of the first theorem.

∎

The proof shows more: $T \vdash \mathrm{Con}_T \to G_T$ , and in fact $T \vdash \mathrm{Con}_T \leftrightarrow G_T$ . Löb (1955) refined the argument to: if $T \vdash \square\varphi \to \varphi$ then $T \vdash \varphi$ — the second theorem is the case $\varphi = \bot$ .

Theorem— Tarski's undefinability theorem (1933)

There is no formula $\mathrm{True}(y)$ of $L_A$ such that, for every sentence $\varphi$ , $\N \models \varphi \leftrightarrow \mathrm{True}(\ulcorner \varphi \urcorner)$ . The set of codes of true arithmetical sentences is not arithmetically definable.

Proof

Apply the diagonal lemma to $\neg\mathrm{True}(y)$ : some sentence $L$ satisfies $\mathsf{Q} \vdash L \leftrightarrow \neg\mathrm{True}(\ulcorner L \urcorner)$ , so this holds in $\N$ . If $\mathrm{True}$ defined truth, we would have $\N \models L \leftrightarrow \neg L$ .

∎

Since $\mathrm{Prov}_T$ is definable, Tarski's theorem gives another proof that for a sound $T$ , provability and truth differ — without exhibiting the witness.

ProofH

Incompleteness from the halting problem

A computability-theoretic route, due essentially to Turing (1936) and Kleene, makes incompleteness look inevitable. Recall from computability that the halting set $K = \{(c, n) : \text{program } c \text{ halts on input } n\}$ is computably enumerable but not decidable, so its complement is not computably enumerable.

Theorem— Theorem (Turing–Kleene incompleteness)

Let $T \supseteq \mathsf{Q}$ be recursively axiomatised and sound (every theorem is true in $\N$ ). For each program $c$ and input $n$ let $H_{c,n}$ be the natural $\Sigma_1$ sentence "the computation of $c$ on $n$ halts". Then there are $c, n$ such that $\neg H_{c,n}$ is true but $T \nvdash \neg H_{c,n}$ .

Proof

The set $\{(c, n) : T \vdash \neg H_{c,n}\}$ is computably enumerable (list the theorems of $T$ ). By soundness it is contained in the complement of $K$ . If it contained every pair outside $K$ it would equal the complement of $K$ , which would then be computably enumerable — so $K$ would be decidable, which it is not.

∎

This version needs soundness. Using a pair of computably inseparable c.e. sets instead of $K$ recovers Rosser's version, which needs only consistency. The theorem also says something Gödel's construction hides: the unprovable sentences include very concrete ones — "this particular program never halts". By the MRDP theorem (see the viewpoints) they include "this particular polynomial equation has no solution in natural numbers".

Formal mathematicsF

The diagonal argument in Lean

Mathlib does not contain Gödel's theorems for $\mathsf{PA}$ : Facts A–C are long and not yet formalised there. The Lean module therefore proves the logical skeleton of the theorems in full, with the arithmetical facts as explicit hypotheses, and proves one genuine incompleteness theorem about programs from Mathlib's computability library.

First, Lawvere's fixed-point theorem and Cantor's theorem as its corollary:

lawvere_fixed_pointLean 4Proved here from basic factsFormally verified

/-- **Lawvere's fixed-point theorem** (1969), the abstract core of the diagonal arguments of
Cantor, Russell, Gödel, Tarski and Turing. If `e : A → (A → B)` hits *every* function
`A → B`, then every map `f : B → B` has a fixed point.
Proof: the diagonal function `g a = f (e a a)` is `e a₀` for some `a₀`, and then
`e a₀ a₀ = g a₀ = f (e a₀ a₀)`. -/
theorem lawvere_fixed_point {A B : Type*} (e : A → A → B) (he : Function.Surjective e)
    (f : B → B) : ∃ b, f b = b := by
  obtain ⟨a₀, ha₀⟩ := he (fun a => f (e a a))
  -- Evaluate the equation `e a₀ = g` at the diagonal point `a₀`.
  exact ⟨e a₀ a₀, (congrFun ha₀ a₀).symm⟩

Axioms used: No axiomsformal/Lumenary/Incompleteness.leanTry it in the Lean web editor

cantor_from_lawvereLean 4Proved here from basic factsFormally verified

/-- Cantor's theorem as a corollary: there is no surjection from `A` onto the predicates
`A → Prop`, because negation `¬ : Prop → Prop` has no fixed point (`P ↔ ¬P` is absurd).
Mathlib's version for sets is `Function.cantor_surjective`. -/
theorem cantor_from_lawvere {A : Type*} (e : A → A → Prop) : ¬ Function.Surjective e := by
  intro he
  obtain ⟨P, hP⟩ := lawvere_fixed_point e he Not
  exact iff_not_self (Iff.of_eq hP.symm)

Axioms used: No axiomsformal/Lumenary/Incompleteness.leanTry it in the Lean web editor

Next, an abstract diagonalisable system in the sense of Smullyan (1992): formulas, sentences, Gödel numbers, substitution of numerals, negation, truth and provability. A set of numbers is expressible if some formula defines it.

DiagSystemLean 4Formally verified

/-- An abstract **diagonalisable system**, after R. M. Smullyan, *Gödel's Incompleteness
Theorems* (1992), chapter 1. It has formulas with one free variable, sentences, Gödel numbers
for both, the substitution `subst φ n = φ(n̄)` of a numeral, a negation, and two predicates on
sentences: truth (in the intended model) and provability (in the theory). The number
`diag (code ψ)` is the Gödel number of the *diagonalisation* `ψ(⌜ψ⌝)`. For first-order
arithmetic all of this is real: Gödel numbers are natural numbers and `diag` is primitive
recursive. -/
structure DiagSystem where
  /-- Formulas with one free variable. -/
  Formula : Type
  /-- Sentences (no free variables). -/
  Sentence : Type
  /-- The Gödel number `⌜ψ⌝` of a formula. -/
  code : Formula → ℕ
  /-- The Gödel number of a sentence. -/
  scode : Sentence → ℕ
  /-- Different sentences have different Gödel numbers. -/
  scode_injective : Function.Injective scode
  /-- `subst ψ n` is the sentence `ψ(n̄)`. -/
  subst : Formula → ℕ → Sentence
  /-- Negation of sentences. -/
  neg : Sentence → Sentence
  /-- Truth in the intended model. -/
  True : Sentence → Prop
  /-- Provability in the theory. -/
  Provable : Sentence → Prop
  true_neg : ∀ s, True (neg s) ↔ ¬ True s
  /-- The diagonal function on Gödel numbers. -/
  diag : ℕ → ℕ
  diag_code : ∀ ψ, diag (code ψ) = scode (subst ψ (code ψ))

Axioms used: No axiomsformal/Lumenary/Incompleteness.leanTry it in the Lean web editor

ExpressibleLean 4Formally verified

/-- A set `A` of natural numbers is **expressible** if some formula `ψ` defines it:
`ψ(n̄)` is true exactly when `n ∈ A`. -/
def Expressible (A : Set ℕ) : Prop :=
  ∃ ψ : S.Formula, ∀ n, S.True (S.subst ψ n) ↔ n ∈ A

Axioms used: No axiomsformal/Lumenary/Incompleteness.leanTry it in the Lean web editor

The diagonal lemma is proved exactly as on paper, by a three-step calc chain. Its hypothesis hdiag — expressible sets are closed under taking preimages along diag — is the abstract counterpart of "the diagonal function is representable" (Fact B):

diagonal_lemmaLean 4Proved here from basic factsFormally verified

/-- **The diagonal lemma (semantic form).** Suppose that whenever `A` is expressible, so is
`diag⁻¹(A) = {n | diag n ∈ A}` (in arithmetic: substitution is definable). Then for every
expressible `A` there is a sentence `G` that is true iff its own Gödel number lies in `A`.
Proof: let `ψ` express `diag⁻¹(A)` and put `G = ψ(⌜ψ⌝)`. Then
`G` true ⟺ `⌜ψ⌝ ∈ diag⁻¹(A)` ⟺ `diag ⌜ψ⌝ ∈ A` ⟺ `⌜G⌝ ∈ A`. -/
theorem diagonal_lemma
    (hdiag : ∀ A : Set ℕ, S.Expressible A → S.Expressible (S.diag ⁻¹' A))
    {A : Set ℕ} (hA : S.Expressible A) : ∃ G : S.Sentence, S.True G ↔ S.scode G ∈ A := by
  obtain ⟨ψ, hψ⟩ := hdiag A hA
  refine ⟨S.subst ψ (S.code ψ), ?_⟩
  calc S.True (S.subst ψ (S.code ψ)) ↔ S.code ψ ∈ S.diag ⁻¹' A := hψ (S.code ψ)
    _ ↔ S.diag (S.code ψ) ∈ A := Iff.rfl
    _ ↔ S.scode (S.subst ψ (S.code ψ)) ∈ A := by rw [S.diag_code ψ]

Axioms used: No axiomsformal/Lumenary/Incompleteness.leanTry it in the Lean web editor

From it, Tarski's theorem and the semantic first incompleteness theorem. Here hprov ("the provable codes form an expressible set") stands for Fact C, and sound for soundness. In the arithmetical setting all four hypotheses are theorems; here they are assumptions, and the formal content is that the conclusions follow from them by the diagonal argument and nothing else.

tarski_undefinabilityLean 4Proved here from basic factsFormally verified

/-- **Tarski's undefinability of truth (abstract form).** If expressible sets are closed under
complements (negation is definable) and under `diag⁻¹` (substitution is definable), then the set
of Gödel numbers of *true* sentences is not expressible.
Proof: otherwise its complement is expressible, and the diagonal lemma gives a sentence `G`
that is true iff `⌜G⌝` is not the number of a true sentence, i.e. iff `G` is false. -/
theorem tarski_undefinability
    (hcompl : ∀ A : Set ℕ, S.Expressible A → S.Expressible Aᶜ)
    (hdiag : ∀ A : Set ℕ, S.Expressible A → S.Expressible (S.diag ⁻¹' A)) :
    ¬ S.Expressible (S.scode '' {s | S.True s}) := by
  intro hT
  obtain ⟨G, hG⟩ := S.diagonal_lemma hdiag (hcompl _ hT)
  -- `⌜G⌝` is the code of a true sentence iff `G` is true, by injectivity of the coding.
  have hcode : S.scode G ∈ S.scode '' {s | S.True s} ↔ S.True G :=
    S.scode_injective.mem_set_image
  have : S.True G ↔ ¬ S.True G := hG.trans (not_congr hcode)
  exact iff_not_self this