626,262,636,626,262,163,636,362,262,112,123,262,163,323,111,123,362,262,112,262,163,323 axiom 3
Va:Va (a+Sa')=S(a+a')
626,262,163,636,362,123,666,112,123,262,163,323,111,123,362,123,666,112,262,163,323 specification
Va (SO+Sa )=S(SO+a )
362,123,666,112,123,666,323,111,123,362,123,666,112,666,323 specification
(SO+SO)=S(SO+O)
626,262,636,362,262,1l2,666,323,lll,262 axiom 2
Va:(a+O)=a
362,123,666,112,666,323,111,123,666
(SO+O)=S 0
123,362,123,666,112,666,323,111,123,123,666
S(SO+O)=SSO
362,123,666,112,123,666,323,111,123,123,666
(SO +SO) =ssospecificationinsert '123'transitivityNotice that I changed the name of the "Add S" rule to "Insert '123"', since
that is the typographical operation which it now legitimizes.
This new notation has a pretty strange feel to it. You lose all sense of
meaning; but if you had been brought up on it, you could read strings in
this notation as easily as you do TNT. You would be able to look and, at a
glance, distinguish well-formed formulas from ill-formed ones. Naturally,
since it is so visual, you would think of this as a typographical operation-
but at the same time, picking out well-formed formulas in this notation is
picking out a special class of integers, which have an arithmetical definition,
too.
Now what about "arithmetizing" all the rules of inference? As matters
stand, they are all still typographical rules. But wait! According to the
Central Proposition, a typographical rule is really equivalent to an
arithmetical rule. Inserting and moving digits in decimally represented
numbers is an arithmetical operation, which can be carried out typographi-
cally. Just as appending a '0' on the end is exactly the same as multiplying by
10, so each rule is a condensed way of describing a messy arithmetical
operation. Therefore, in a sense, we do not even need to look for equiva-
lent arithmetical rules, because all of the rules are already arithmetical!
TNT-Numbers: A Recursively Enumerable Set of NumbersLooked at this way, the preceding derivation of the theorem
"362,123,666,112,123,666,323,111,123,123,666" is a sequence of highly
convoluted number-theoretical transformations, each of which acts on one
or more input numbers, and yields an output number, which is, as before,
called a producible number, or, to be more specific, a TNT-number. Some of
the arithmetical rules take an old TNT-number and increase it in a particu-
lar way, to yield a new TNT-number; some take an old TNT-number and
decrease it; other rules take two TNT-numbers, operate on each of them in
some odd way, and then combine the results into a new TNT-number-
and so on and so forth. And instead of starting with just one known
TNT-number, we have five initial TNT-numbers-one for each (austere)
axiom, of course. Arithmetized TNT is actually extremely similar to theMurnon and Godel 269