Since it is a property of two numbers, it is represented by a formula with
two free variables. (Note: In this Chapter we shall always use austere
TNT-so be careful to distinguish between the variables a, a', a".) In order
to assert "MU is a theorem of the MI U-system", we would have to make the
isomorphic statement "30 is a theorem-number of the MIU-system", and
then translate that into TNT -notation. With the aid of our abbreviation,
this is easy (remember also from Chapter VIII that to indicate the replace-
ment of every a' by a numeral, we write that numeral followed by "la' "):3a:MI U-PROO F-PAl R{ a,SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSOI a'}Count the S's: there are 30. Note that this is a closed sentence of TNT,
because one free variable was quantified, the other replaced by a numeraL
A clever thing has been done here, by the way. Fundamental Fact 2 gave us
a way to talk about proof-pairs; we have figured out how to talk about
theorem-numbers, as well: you just add an existential quantifier in front! A
more literal translation of the string above would be, "There exists some
number a that forms a MIU-proof-pair with 30 as its second element".
Suppose that we wanted to do something parallel with respect to
TNT-say, to express the statement "0=0 is a theorem of TNT". We may
abbreviate the formula which Fundamental Fact 2 assures us exists, in an
analogous way (with two free variables, again):TNT-PROOF-PAIR{a,a'}(The interpretation of this abbreviated TNT-formula is: "Natural numbers
a and a' form a TNT-proof-pair.") The next step is to transform our
statement into number theory, following the MUMON-model above. The
statement becomes "There exists some number a which forms a TNT-
proof-pair with 666,111,666 as its second element". The TNT-formula
which expresses this is:3a:TNT-PROOF-PAIR{a,SSSSS ........ .sSSSSO/a'}
-------------many, many S's!
(in fact, 666,111,666 of them)-a closed sentence of TNT. (Let us call it "jOSHO", for reasons to appear
momentarily.) So you see that there is a way to talk not only about the
primitive recursive notion of TNT -proof-pairs, but also about the related
but trickier notion of TNT-theorem-numbers.
To check your comprehension of these ideas, figure out how to trans-
late into TNT the following statements of meta-TNT:
(1) 0=0 is not a theorem of T:\IT.
(2) -0=0 is a theorem of TKT.
(3) -0=0 is not a theorem of TNT.442 On Formally Undecidable Propositions