Gödel, Escher, Bach An Eternal Golden Braid by Douglas R. Hofstadter

of the substitution operation we defined earlier. If we wanted to speak

about arithmoquining inside TNT, we would use the formula

SUB{a", a", a'}

where the first two variables are the same. This comes from the fact that we

are using a single number in two different ways (shades of the Cantor

diagonal method!). The number a" is both (1) the original Godel number,

and (2) the insertion-number. Let us invent an abbreviation for the above

formula:

ARlTHMOQUINE{a", a'}

What the above formula says, in English, is:

a' is the G6del number of the formula gotten by arithmoquining

the formula with G6del number a".

Now the preceding sentence is long and ugly. Let's introduce a concise and

elegant term to summarize it. We'll say

a' is the arithmoquinification of a"

to mean the same thing. For instance, the arithmoquinification of

262,111,123,666 is this unutterably gigantic number:

123,123,123, ..... ,123,123,123,666,111,123,666

----------~-----------262,111,123,666 copies of '123'

(This is just the Godel number of the formula we got when we
arithmoquined a=SO.) We can speak quite easily about arithmoquining
inside TNT.

The Last Straw

Now if you look back in the Air on G's String, you will see that the ultimate
trick necessary for achieving self-reference in Quine's way is to quine a
sentence which itself talks about the concept of quining. It's not enough just
to quine-you must quine a quine-mentioning sentence! All right, then-
the parallel trick in our case must be to arithmoquine some formula which
itself is talking about the notion of arithmoquining!
Without further ado, we'll now write that formula down, and call it G's
uncle:

-3a:3a':<TNT-PROOF-PAIR{a,a'}AARITHMOQUINE{a",a'}>

You can see explicitly how arithmoquinification is thickly involved in the

plot. Now this "uncle" has a G6del number, of course, which we'll call 'u'.

(^446) On Formally Undecidable Propositions