The diagonal lemma shows how to construct self-referential sentences in the language of arithmetic from formulas .

In its standard form it says that is $T$ is a theory extending minimal arithmetic (so that it can talk about recursive expressions with full generality) and $ϕ (x)$ is a formula with one free variable $x$ then there exists a sentence $S$ such that $T ⊢ S \leftrightarrow ϕ (┌ S ┐)$ .

This can be further generalized for cases with multiples formulas and variables.

The diagonal lemma is important because it allows the formalization of all kind of self-referential and apparently paradoxical sentences.

Take for example the liar's sentence affirming that "This sentence is false". Since there is no truth predicate, we will have to adapt it to our language to say "This sentence is not provable". Since there is a predicate of arithmetic expressing provability we can construct a formula $\neg □_{P A} (x)$ , which is true iff there is no proof in $P A$ of the sentence encoded by $x$ .

By invoking the diagonal's lemma, we can see that there exists a sentence $G$ such that $P A ⊢ G \leftrightarrow \neg □_{P A} (┌ G ┐)$ , which reflects the spirit of our informal sentence. The weak form of Gödel's first incompleteness theorem follows swiftly from there.

The equivalent in computation of the diagonal lemma is called quining, and refers to computer programs which produce their own source code as part of their computation.

Indeed, the key insight of the diagonal lemma and quining is that you can have subexpressions in your program that when "expanded" are identical to the original expression that contains them.

Diagonal lemma