Diagonal lemma

In mathematical logic, Gödel's diagonal lemma is a precise way of constructing self-referential statements. Let T be a theory in an extension of the language of arithmetic in which all recursive functions are representable. Let A(x) be a formula with x as its free variable. Then, there is a formula B such that

T |- B <-> A("B")

where "B" is the numeral which denotes the code of the sentence B.

Intuitively, B is a self-referential sentence, for it says of itself that it has the property A(x).

Here is a simple proof. Let A(x) be a formula with just x free. Let D(A) be the sentence A("A"). I.e., the result of substituting the quotation name of A for x in A. This mapping is called diagonalization, and D(A) is the diagonalization of A, and D is called the diagonal function. This mapping can be shown to be recursive. Since T represents all such functions, suppose diag(x) is a new function symbol which represents this function. Consider the sentence A(diag(x)). This says: the diagonalization of x has property A. Now, consider the diagonalization of A(diag(x))! I.e., let B be the sentence A(diag("A(diag(x))")). So, B has the form A(t), where t is the term diag("A(diag(x))").

Clearly,

T |- B <-> A(t)

But t denotes the diagonalization of A(diag(x)). So, t denotes B! And this is provable in T. So,

T |= t = "B"

So,

T |- B <-> A("B").