-or if you prefer,
"I am not a theorem of TNT."We have gradually pulled a high-level interpretation-a sentence of
meta-TNT -out of what was originally a low-level interpretation-a sen-
tence of number theory.TNT Says "UncleI"The main consequence of this amazing construction has already been
delineated in Chapter IX: it is the incompleteness of TNT. To reiterate the
argument:Is G a TNT-theorem? If so, then it must assert a truth. But
what in fact does G assert? Its own nontheoremhood. Thus from
its theoremhood would follow its nontheoremhood: a contradic-
tion.
Now what about G being a nontheorem? This is acceptable, in
that it doesn't lead to a contradiction. But G's nontheoremhood is
what G asserts-hence G asserts a truth. And since G is not a
theorem, there exists (at least) one truth which is not a theorem of
TNT.
Now to explain that one tricky step again. I will use another similar
example. Take this string:-3a:3a':<TORTOISE-PAIR{a,a'}ATENTH-POWER{SSO/a",a'}>where the two abbreviations are for strings of TNT which you can write
down yourself. TENTH-POWER{a",a'} represents the statement "a' is the
tenth power of a"". The literal translation into English is then:"There do not exist numbers a and a' such that both (1) they form
a Tortoise-pair, and (2) a' is the tenth power of 2."But dearly, there is a tenth power of 2-namely lO24. Therefore, what the
string is really saying is that"There is no number a that forms a Tortoise-pair with lO24"which can be further boiled down to:"lO24 does not have the Tortoise property."The point is that we have achieved a way of substituting a description of a
number, rather than its numeral, into a predicate. It depends on using one
extra quantified variable (a'). Here, it was the number lO24 that was
described as "the tenth power of 2"; above, it was the number described as
"the arithmoquinification of u".448 On Formally Undecidable Propositions