Figure 1: Diagonalization (where a code for a function is fed into the function itself) |
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:
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 |
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:
I will now declare one further function, C(x), as logically equivalent to the property A applied to diag(x):
The diagonal lemma can also be used to construct the famous Gödel statement where A is the property of being unprovable. That is:
The diagonal lemma can also be used to construct the liar sentence where A is the property of not being true. That is:
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).
This blog gets me quite exited! I have been thinking of making a similar thing on my personal website. Writing abouth my thougths on a wide range of subjectareas just so i could get them out of my head and share them with others. I cant find you on facebook or any other media (I realized there is quite a few Andrew Mcdonald´s out there). I would love to get in touch if you would like:)
ReplyDeleteHi Lars - go for it! I find the discipline of trying to communicate an idea to others definitely helps me to understand it better.
ReplyDeleteI'm not on other social media. But feel free to contact me on andrewmacmail at gmail dot com if you like.