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

arithmetized MIU-system, only there are more rules and axioms, and to

write out arithmetical equivalents explicitly would be a big bother-and

quite unenlightening, incidentally. If you followed how it was done for the

MIU-system, there ought to be no doubt on your part that it is quite

analogous here.

There is a new number-theoretical predicate brought into being by

this "Godelization" of TNT: the predicate

a is a TNT-number.

For example, we know from the preceding derivation that

362,123,666,112,123,666,323,111,123,123,666 is a TNT-number, while

on the other hand, presumably 123,666,111,666 is not a TNT-number.

Now it occurs to us that this new number-theoretical predicate is

expressible by some string of TNT with one free variable, say a. We could put

a tilde in front, and that string would express the complementary notion

a is not a TNT-number.

Now if we replaced all the occurrences of a in this second string by the

TNT-numeral for 123,666,111,666-a numeral which would contain

exactly 123,666, III ,666 5's, much too long to write out-we would have a

TNT-string which, just like MUMON, is capable of being interpreted on

two levels. In the first place, that string would say

123,666,111,666 is not a TNT-number.

But because of the isomorphism which links TNT-numbers to theorems of

TNT, there would be a second-level meaning of this string, which is:

50=0 is not a theorem of TNT.

TNT Tries to Swallow Itself

This unexpected double-entendre demonstrates that TNT contains strings
which talk about other strings of TNT. In other words, the metalanguage
in which we, on the outside, can speak about TNT, is at least partially
imitated inside TNT itself. And this is not an accidental feature of TNT; it
happens because the architecture of any formal system can be mirrored
inside N (number theory). It is just as inevitable a feature of TNT as are the
vibrations induced in a record player when it plays a record. It seems as if
vibrations should come from the outside world-for instance, from jump-
ing children or bouncing balls; but a side effect of producing sounds-and
an unavoidable one-is that they wrap around and shake the very
mechanism which produces them. It is no accident; it is a side effect which
cannot be helped. It is in the nature of record players. And it is in the
nature of any formalization of number theory that its metalanguage is
embedded within it.

(^270) Murnon and Godel