Diagonal lemma


by Jaime Sevilla Molina Jul 10 2016 updated Jul 22 2016

Constructing self-referential sentences

[summary: If F(x) is a one place formula of First Order Logic and $~$T$~$ is a theory extending [ minimal arithmetic] then there exists a sentence $~$S$~$ such that $~$T\vdash S\iff F(\ulcorner S \urcorner)$~$.]

The diagonal lemma shows how to construct self-referential sentences in the language of arithmetic from formulas $~$\phi(x)$~$.

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 $~$\phi(x)$~$ is a formula with one free variable $~$x$~$ then there exists a sentence $~$S$~$ such that $~$T\vdash S\leftrightarrow \phi(\ulcorner S\urcorner)$~$.

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 \square_{PA} (x)$~$, which is true iff there is no proof in [3ft $~$PA$~$] of the sentence encoded by $~$x$~$.

By invoking the diagonal's lemma, we can see that there exists a sentence $~$G$~$ such that $~$PA\vdash G\leftrightarrow \neg \square_{PA} (\ulcorner G\urcorner)$~$, 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.