---
tag: 3PRW76471J
kind: statement
role: lemma
name: Diagonal lemma
msc: [03F40]
uses: [3K1AKGXF8A, MFJXPAF0R0, HYJ10AF6RT, DKFGQTRYZE, 92SWXST1ZM]
about: [MFJXPAF0R0]
sources:
  - url: https://en.wikipedia.org/wiki/Diagonal_lemma
same_as:
  wikidata: Q2904195
  wikipedia: Diagonal lemma
---

## Statement

Let $T$ be a [[theory|92SWXST1ZM]] in the language of arithmetic that contains [[Robinson arithmetic|3K1AKGXF8A]] $\mathsf{Q}$.
Fix a [[Gödel numbering|MFJXPAF0R0]], and let $\ulcorner \psi \urcorner$ be the numeral of the code of $\psi$.
For every [[formula|HYJ10AF6RT]] $\varphi(x)$ with exactly one free variable $x$, there is a [[sentence|DKFGQTRYZE]] $\psi$ such that
$$T \vdash \psi \leftrightarrow \varphi(\ulcorner \psi \urcorner).$$

## 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|X9WYNYE29C]].
No consistency assumption on $T$ is needed.

## Explanations

### L1 human

The lemma says that arithmetic can build sentences that talk about themselves.
For any property of sentences that arithmetic can express, there is a sentence that says "I have this property".
This self-reference is the engine behind the incompleteness theorems.

### L2 human

The diagonal lemma is the common core of [[Gödel's incompleteness theorems|X9WYNYE29C]], [[Tarski's undefinability theorem|YRV6SYK2BY]] and [[Löb's theorem|3HD30YG3DG]].
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|F3Z30M606H]], which lets a program refer to its own code.