Diagonal lemma

Remarks

Proof idea: the diagonal function $d$, which sends the code of a formula $\theta(x)$ to the code of $\theta(\ulcorner \theta \urcorner)$, is computable. So it is represented in $\mathsf{Q}$ by a formula $D(x, y)$. Let $\theta(x)$ be $\exists y\, (D(x, y) \wedge \varphi(y))$ and let $\psi$ be $\theta(\ulcorner \theta \urcorner)$. Then $\psi$ says that $\varphi$ holds of $d(\ulcorner \theta \urcorner)$, which is the code of $\psi$, and $\mathsf{Q}$ proves this equivalence.

Example: with $\varphi(x) = \neg \mathrm{Prov}_T(x)$, the lemma gives a sentence that says of itself "I am not provable in $T$", the Gödel sentence of Gödel's incompleteness theorems. No consistency assumption on $T$ is needed.

Going deeper

For a student

The diagonal lemma is the common core of Gödel's incompleteness theorems, Tarski's undefinability theorem and Löb's theorem. Each of them applies the lemma to a well-chosen formula: unprovability, falsity, or a provability implication. It is an arithmetic version of Kleene's recursion theorem, which lets a program refer to its own code.