u
uS's
~
-3a': <TNT-PROOF-PAIR{O/a,a'} A ARITHMOQUINE{SSS ... SSSO/a", a'}>
-3a': <TNT-PROOF-PAIR{SO/a,a'} A ARITHMOQUINE{SSS ... SSSO/a", a'}>
-3a': <TNT-PROOF-PAlR{SSO/a,a'} A ARITHMOQUINE{SSS ... SSSO/a", a'}>
-3a': <TNT-PROOF-PAIR{SSSO/a,a'} AARITHMOQUINE{SSS ... SSSO/a", a'}>What does each one assert? Their translations, one by one, are:"0 and the arithmoquinification of u do not form a TNT -proof-pair."
"1 and the arithmoquinification of u do not form a TNT-proof-pair."
"2 and the arithmoquinification of u do not form a TNT -proof-pair."
"3 and the arithmoquinification of u do not form a TNT -proof-pair."Now each of these assertions is about whether two specific integers form a
proof-pair or not. (By contrast, C itself is about whether one specific integer
is a theorem-number or not.) Now because'C is a nontheorem, no integer
forms a proof-pair with C's Codel number. Therefore, each of the state-
ments of the family is true. Now the crux of the matter is that the property
of being a proof-pair is primitive recursive, hence represented, so that each
of the statements in the list above, being true, must translate into a theorem
of TNT-which means that everything in our infinite pyramidal family is a
theorem. And that shows why TNT is w-incomplete.Two Different Ways to Plug Up the Hole
Since C's interpretation is true, the interpretation of its negation -C is
false. And, using the assumption that TNT is consistent, we know that no
false statements are derivable in TNT. Thus neither C nor its negation -C
is a theorem of TNT. We have found a hole in our system-an undecidable
proposition. Now this need be no source of alarm, if we are philosophically
detached enough to recognize what this is a symptom of. It signifies that
TNT can be extended, just as absolute geometry could be. In fact, TNT
can be extended in two distinct directions, just as absolute geometry could
be. It can be extended in a standard direction-which corresponds to ex-
tending absolute geometry in the Euclidean direction; or, it can be ex-
tended in a nonstandard direction-which corresponds, of course, to ex-
tending absolute geometry in the non-Euclidean direction. Now the stan-
dard type of extension would involve
adding C as a new axiom.On Formally Undecidable Propositions^451