In mathematical logic, the diagonal lemma (also known as diagonalization lemma, self-reference lemma or fixed point theorem) establishes the existence of self-referential sentences in certain formal theories.

A particular instance of the diagonal lemma was used by Kurt Gödel in 1931 to construct his proof of the incompleteness theorems as well as in 1933 by Tarski to prove his undefinability theorem. In 1934, Carnap was the first to publish the diagonal lemma at some level of generality. The diagonal lemma is named in reference to Cantor's diagonal argument in set and number theory.

The diagonal lemma applies to any sufficiently strong theories capable of representing the diagonal function. Such theories include first-order Peano arithmetic ${\displaystyle {\mathsf {PA}}}$, the weaker Robinson arithmetic ${\displaystyle {\mathsf {Q}}}$ as well as any theory containing ${\displaystyle {\mathsf {Q}}}$ (i.e. which interprets it). A common statement of the lemma (as given below) makes the stronger assumption that the theory can represent all recursive functions, but all the theories mentioned have that capacity, as well.

The diagonal lemma also requires a Gödel numbering ${\displaystyle \alpha }$. We write ${\displaystyle \alpha (\varphi )}$ for the code assigned to ${\displaystyle \varphi }$ by the numbering. For ${\displaystyle {\overline {n}}}$, the standard numeral of ${\displaystyle n}$ (i.e. ${\displaystyle {\overline {0}}=_{df}{\mathsf {0}}}$ and ${\displaystyle {\overline {n+1}}=_{df}{\mathsf {S}}({\overline {n}})}$), let ${\displaystyle \ulcorner \varphi \urcorner }$ be the standard numeral of the code of ${\displaystyle \varphi }$ (i.e. ${\displaystyle \ulcorner \varphi \urcorner }$ is ${\displaystyle {\overline {\alpha (\varphi )}}}$). We assume a standard Gödel numbering

Let ${\displaystyle \mathbb {N} }$ be the set of natural numbers. A first-order theory ${\displaystyle T}$ in the language of arithmetic containing ${\displaystyle {\mathsf {Q}}}$ represents the ${\displaystyle k}$-ary recursive function ${\displaystyle f:\mathbb {N} ^{k}\rightarrow \mathbb {N} }$ if there is a formula ${\displaystyle \varphi _{f}(x_{1},\dots ,x_{k},y)}$ in the language of ${\displaystyle T}$ s.t. for all ${\displaystyle m_{1},\dots ,m_{k}\in \mathbb {N} }$, if ${\displaystyle f(m_{1},\dots ,m_{k})=n}$ then ${\displaystyle T\vdash \forall y(\varphi _{f}({\overline {m_{1}}},\dots ,{\overline {m_{k}}},y)\leftrightarrow y={\overline {n}})}$.

The representation theorem is provable, i.e. every recursive function is representable in ${\displaystyle T}$.

Diagonal Lemma: Let ${\displaystyle T}$ be a first-order theory containing ${\displaystyle {\mathsf {Q}}}$ (Robinson arithmetic) and let ${\displaystyle \psi (x)}$ be any formula in the language of ${\displaystyle T}$ with only ${\displaystyle x}$ as free variable. Then there is a sentence ${\displaystyle \varphi }$ in the language of ${\displaystyle T}$ s.t. ${\displaystyle T\vdash \varphi \leftrightarrow \psi (\ulcorner \varphi \urcorner )}$.

Intuitively, ${\displaystyle \varphi }$ is a self-referential sentence which "says of itself that it has the property ${\displaystyle \psi }$."