Diagonal lemma

The di­ag­o­nal lemma shows how to con­struct self-refer­en­tial sen­tences in the lan­guage of ar­ith­metic from for­mu­las \(\phi(x)\).

In its stan­dard form it says that is \(T\) is a the­ory ex­tend­ing min­i­mal ar­ith­metic (so that it can talk about re­cur­sive ex­pres­sions with full gen­er­al­ity) and \(\phi(x)\) is a for­mula with one free vari­able \(x\) then there ex­ists a sen­tence \(S\) such that \(T\vdash S\leftrightarrow \phi(\ulcorner S\urcorner)\).

This can be fur­ther gen­er­al­ized for cases with mul­ti­ples for­mu­las and vari­ables.

The di­ag­o­nal lemma is im­por­tant be­cause it al­lows the for­mal­iza­tion of all kind of self-refer­en­tial and ap­par­ently para­dox­i­cal sen­tences.

Take for ex­am­ple the liar’s sen­tence af­firm­ing that “This sen­tence is false”. Since there is no truth pred­i­cate, we will have to adapt it to our lan­guage to say “This sen­tence is not prov­able”. Since there is a pred­i­cate of ar­ith­metic ex­press­ing prov­abil­ity we can con­struct a for­mula \(\neg \square_{PA} (x)\), which is true iff there is no proof in \(PA\) of the sen­tence en­coded by \(x\).

By in­vok­ing the di­ag­o­nal’s lemma, we can see that there ex­ists a sen­tence \(G\) such that \(PA\vdash G\leftrightarrow \neg \square_{PA} (\ulcorner G\urcorner)\), which re­flects the spirit of our in­for­mal sen­tence. The weak form of Gödel’s first in­com­plete­ness the­o­rem fol­lows swiftly from there.

The equiv­a­lent in com­pu­ta­tion of the di­ag­o­nal lemma is called quin­ing, and refers to com­puter pro­grams which pro­duce their own source code as part of their com­pu­ta­tion.

In­deed, the key in­sight of the di­ag­o­nal lemma and quin­ing is that you can have subex­pres­sions in your pro­gram that when “ex­panded” are iden­ti­cal to the origi­nal ex­pres­sion that con­tains them.


  • Quine

    A com­puter pro­gram that prints (or does other com­pu­ta­tions to) its own source code, us­ing in­di­rect self-refer­ence.


  • Mathematics

    Math­e­mat­ics is the study of num­bers and other ideal ob­jects that can be de­scribed by ax­ioms.