Proof of the Diagonal Lemma

The diagonal lemma (or fixed-point lemma) is the technical engine behind both Gödel's incompleteness theorems and Tarski's undefinability theorem. We give a detailed proof showing how self-reference is achieved through Gödel numbering.

Statement

Theorem6.3Diagonal Lemma

Let $T$ be a theory extending Robinson arithmetic $Q$ in the language $\mathcal{L}$ . For any $\mathcal{L}$ -formula $\psi(x)$ with one free variable, there exists a sentence $\sigma$ such that $T \vdash \sigma \leftrightarrow \psi(\ulcorner \sigma \urcorner)$ .

Proof

Step 1: Substitution function. Define the computable function $\mathrm{sub}(m, n)$ that takes a Gödel number $m$ of a formula $\varphi(x)$ with one free variable and a number $n$ , and returns the Gödel number of $\varphi(\underline{n})$ (where $\underline{n}$ is the numeral for $n$ ). Since $\mathrm{sub}$ is computable and $T \supseteq Q$ , it is representable by a formula $\mathrm{Sub}(x, y, z)$ : $T \vdash \mathrm{Sub}(\underline{m}, \underline{n}, \underline{\mathrm{sub}(m,n)}) \quad \text{and} \quad T \vdash \forall z \, (\mathrm{Sub}(\underline{m}, \underline{n}, z) \to z = \underline{\mathrm{sub}(m,n)}).$

Step 2: Construct the diagonal formula. Define $\theta(x) \equiv \forall z \, (\mathrm{Sub}(x, x, z) \to \psi(z))$ . This formula says: "the result of substituting the Gödel number of $x$ into the formula with Gödel number $x$ satisfies $\psi$ ."

Step 3: Self-application. Let $m = \ulcorner \theta(x) \urcorner$ be the Gödel number of $\theta$ . Define $\sigma \equiv \theta(\underline{m})$ , i.e., the sentence $\forall z \, (\mathrm{Sub}(\underline{m}, \underline{m}, z) \to \psi(z))$ .

Step 4: Verify the fixed point. We have $\mathrm{sub}(m, m) = \ulcorner \theta(\underline{m}) \urcorner = \ulcorner \sigma \urcorner$ . In $T$ : $T \vdash \sigma \leftrightarrow \forall z \, (\mathrm{Sub}(\underline{m}, \underline{m}, z) \to \psi(z)).$ Since $T$ proves $\mathrm{Sub}(\underline{m}, \underline{m}, z) \to z = \ulcorner \sigma \urcorner$ , we get: $T \vdash \sigma \leftrightarrow \psi(\ulcorner \sigma \urcorner). \quad \square$

■

Applications

ExampleDeriving the Gödel Sentence

Applying the diagonal lemma to $\psi(x) = \neg \mathrm{Prov}_T(x)$ : there exists $G$ with $T \vdash G \leftrightarrow \neg \mathrm{Prov}_T(\ulcorner G \urcorner)$ . This is the Gödel sentence asserting its own unprovability.

ExampleDeriving the Liar Sentence

Applying the diagonal lemma to $\psi(x) = \neg \mathrm{True}(x)$ (if $\mathrm{True}$ existed): there would be $\lambda$ with $\mathbb{N} \models \lambda \leftrightarrow \neg \mathrm{True}(\ulcorner \lambda \urcorner)$ . This is the formalization of the liar paradox, yielding a contradiction and proving Tarski's theorem.

RemarkGenerality of the Construction

The diagonal lemma works for any formula with one free variable, not just $\neg \mathrm{Prov}_T(x)$ . This generality is exploited in many results: the Gödel sentence, the Rosser sentence, Löb's theorem, and constructions in provability logic all start from the diagonal lemma with different choices of $\psi$ .