The head and tail of u's decimal expansion, and even a teeny bit of its
midsection, can be read off directly:u = 223,333,262,636,333,262,163,636,212, ... ,161, ... ,213
For the rest, we'd have to know just how the formulas TNT-PROOF-PAIR
and ARITHMOQUINE actually look when written out. That is too complex,
and it is quite beside the point, in any case.
Now all we need to do is-arithmoquine this very uncle! What this
entails is "booting out" all free variables-of which there is only one,
namely a"-and putting in the numeral for u everywhere. This gives us:-3a:3a':<TNT-PROOF-PAIR{a,a'}AARITHMOQUINE{SSS ... SSSO/a",a'}>
----------uS'sAnd this, believe it or not, is Godel's string, which we can call 'G'. Now there
are two questions we must answer without delay. They are(1) What is G's Godel number?
(2) What is the interpretation of G?Question 1 first. How did we make G? Well, we began with the uncle, and
arithmoquined it. So, by the definition of arithmoquinification, G's Godel
number is:
the arithmoquinification of u.Now question 2. We will translate G into English in stages, getting gradually
more comprehensible as we go along. For our first rough try, we make a
pretty literal translation:"There do not exist numbers a and a' such that both (1) they form
a TNT-proof-pair, and (2) a' is the arithmoquinification of u."Now certainly there is a number a' which is the arithmoquinification of
u-so the problem must lie with the other number, a. This observation
allows us to rephrase the translation of G as follows:"There is no number a that forms a TNT -proof-pair
with the arithmoquinification of u."(This step, which can be confusing, is explained below in more detail.) Do
you see what is happening? G is saying this:"The formula whose Godel number is the arithmoquinification
of u is not a theorem of TNT."But-and this should come as no surprise by now-that formula is none
other than G itself; whence we can make the ultimate translation of G as"G is not a theorem of TNT."On Formally Undecidable Propositions 447