The diagonal lemma

Figure 1: Diagonalization (where a code for a function is
fed into the function itself)

The diagonal lemma (or fixed point theorem) is an essential part of several notable mathematical proofs including Gödel's incompleteness theorems and Tarski's undefinability theorem.

The term diagonal is used because it bears some resemblance to Cantor's famous diagonal argument.

Intuitively, the diagonal lemma says that for any property A, there is a self-referential statement B saying that it has property A.[1] The lemma is expressed as a logical equivalence:

\[\boldsymbol{B \Leftrightarrow A(\#B)}\]

A can be any property about numbers such as isPrime or isEven. This means that statement B must be translatable to a number, which is indicated by the # in the lemma above. The translation is achieved by Gödel-numbering which assigns a unique natural number to every possible statement.

A simple way to implement Gödel-numbering is by converting the statement to its ASCII representation. So the statement "isEven(2)" translates to the number 69734576656e283229 in hexadecimal (which can be translated with a text to hex converter). That number is also translatable back to the original statement again. Thus there is a one-to-one mapping between a statement and its Gödel number.

Figure 2: Substitution along the diagonal

We can also represent statements containing free variables. For example, the statement "isEven(x)" translates to the Gödel number 69734576656e287829.[2] Now consider the table in Figure 2 where the rows (j) represent the Gödel numbers of statements and the columns (k) represent the possible values for x (themselves natural numbers). We can define the function sub(j, k) to translate Gödel number j as a statement, then substitute number k in place of x and, finally, translate that statement to a Gödel number. For example, sub(69734576656e287829, 8) will translate Gödel number 69734576656e287829 as "isEven(x)" then substitute 8 for x, producing the evaluable statement "isEven(8)" and finally translate that statement to the Gödel number 69734576656e283829.

Since k can be any natural number, we can also substitute the Gödel number of the statement itself. That is, sub(69734576656e287829, 69734576656e287829) will translate Gödel number 69734576656e287829 as "isEven(x)" then substitute 69734576656e287829 for x, producing the evaluable statement "isEven(69734576656e287829)" and finally translate it to Gödel number 69734576656e2836393733343537363635366532383738323929. This particular kind of substitution (where j = k) is called diagonalization because it shows up on the diagonal (i.e., the blue squares) of the table in Figure 2. This self-referential process is key to what follows.

To simplify, the diagonalization can be defined by a function with one free variable x:

\[\boldsymbol{diag(x) = sub(x, x)}\]

I will now declare one further function, C(x), as logically equivalent to the property A applied to diag(x):

\[\boldsymbol{C(x) \Leftrightarrow A(diag(x))}\]

Function C will also have a Gödel number which I'll call m. So m is the Gödel number of the function C which, on input x, is logically equivalent to interpreting x as a function, running x on itself, and then running A on the result (partially illustrated by Figure 1). For example, suppose input x is the Gödel number of "isEven(x)" and A is the property isPrime, then we would have: [3]

\[\boldsymbol{C(\#''isEven(x)'') \Leftrightarrow ~''isPrime(diag(\#''isEven(x)''))''}\]

As noted earlier, # indicates the Gödel number of the subsequent statement. Now suppose that m (the Gödel number of function C) is itself the input to function C. This will result in:

\[\boldsymbol{C(m) \Leftrightarrow A(diag(m))}\]

The diag function interprets m as a function (i.e., C(x)) and substitutes m for x (i.e., C(m)). So:

\[\boldsymbol{C(m) \Leftrightarrow A(\#C(m))}\]

Now let B = C(m) and the result is the diagonal lemma:

\[\boldsymbol{B \Leftrightarrow A(\#B)}\]

When expanded out, B is A(diag(#"A(diag(x))")) which is logically equivalent to the right-hand-side of A(#'A(diag(#"A(diag(x))"))'). For example, suppose that A is the property isEven. Statement B is then 'isEven(diag(#"isEven(diag(x))"))'. That is, B says that the diagonalization of the inner statement is an even number. But the diagonalization of the inner statement just is B's Gödel number. So, in effect, B says of itself that its Gödel number is even. Further saying that the Gödel number of B is even is, therefore, logically equivalent to what B already says of itself.[4]

The diagonal lemma can also be used to construct the famous Gödel statement where A is the property of being unprovable. That is:

\[\boldsymbol{B \Leftrightarrow isNotProvable(\#B)}\]

If B is true, then B is, as it says, not provable. Whereas if B is false, then it is false that it is not provable. That is, it is provable. Thus either statement B is true and not provable, and so the system is incomplete. Or else statement B is false and provable, and so the system is inconsistent (since it can prove a false statement). That is Gödel's first incompleteness theorem.

The diagonal lemma can also be used to construct the liar sentence where A is the property of not being true. That is:

\[\boldsymbol{B \Leftrightarrow isFalse(\#B)}\]

If B is true, then B is false. Whereas if B is false, then B truthfully asserts that. Either way, the result is a contradiction. The conclusion of Tarski's undefinability theorem is that the truth predicate is not definable in the object language, so the liar sentence cannot be constructed.

Useful references:

• Proof of Diagonalization Lemma - p181 - Professor Anita Wasilewska
• Gödel’s First Incompleteness Theorem explained - A Trivial Knot blog (also the source of Figure 2)
• "Diagonal fixed points are constructed with a weird trick where you feed a code for a function into that function itself. Given a function f, if you can construct a function g, which on input x, interprets x as a function, runs x on itself, and then runs f on the result (i.e. g(x) := f(x(x)).), then g(g) is a fixed point of f because g(g) = f(g(g))." - Fixed Point Discussion - Less Wrong
• Gödel numbering and diagonalization - Greg Restall
• Diagonalization & The Fixed Point Lemma - Brendan Cordy
• Fixed point (mathematics) - Wikipedia

--

[1] Strictly-speaking, that the numeric representation of statement B has property A. This is indicated by the # which translates from the statement to a natural number (termed its Gödel number).

[2] In this post, the term statement indicates both formulas with free variables (e.g., "IsEven(x)", where x can be any natural number) and formulas without free variables (e.g., "isEven(2)" or "isEven(3)" which are sentences that evaluate as true or false).

[3] The right-hand-side statement resolves to "isPrime(69734576656e2836393733343537363635366532383738323929)". You can use the hex to text converter to decode the Gödel number.

[4] To step through the final substitution in detail:

The inner statement says, "isEven(diag(x))", i.e., "the diagonalization of x is even". To diagonalize that statement is to substitute its Gödel number for x. That is:

    'isEven(diag(  #"isEven(diag(x))"  ))'

Which is to say, 'the diagonalization of #"the diagonalization of x is even" is even'. While the final statement just is the diagonalization of the inner statement, it also asserts a property of the diagonalization of the inner statement, namely, that it is even. Thus, in effect, the statement is asserting a property of its own Gödel number (that it is even).