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

This completes the table of Rules of Formation for the well-formed for-
mulas of TNT.

A Few More Translation Exercises

And now, a few practice exercises for you, to test your understanding of

the notation of TNT. Try to translate the first four of the following

N-sentences into TNT-sentences, and the last one into an open well-

formed formula.

All natural numbers are equal to 4.

There is no natural number which equals its own square.

Different natural numbers have different successors.

If 1 equals 0, then every number is odd.

b is a power of 2.

The last one you may find a little tricky. But it is nothing, compared to this

one:

b is a power of 10.

Strangely, this one takes great cleverness to render in our notation. I would

caution you to try it only if you are willing to spend hours and hours on

it-and if you know quite a bit of number theory!

A Nontypographical System

This concludes the exposition of the notation of TNT; however, we are still

left with the problem of making TNT into the ambitious system which we

have described. Success would justify the interpretations which we have

given to the various symbols. Until we have done that, however, these

particular interpretations are no more justified than the "horse-apple-

happy" interpretations were for the pq-system's symbols.

Someone might suggest the following way of constructing TNT: {1) Do

not have any rules of inference; they are unnecessary, because (2) We take

as axioms all true statements of number theory (as written in TNT-

notation). What a simple prescription! Unfortunately it is as empty as one's

instantaneous reaction says it is. Part (2) is, of course, not a typographical

description of strings. The whole purpose of TNT is to figure out if and

how it is possible to--characterize the true strings typographically.

The Five Axioms and First Rules of TNT

Thus we will follow a more difficult route than the suggestion above; we
will have axioms and rules of inference. Firstly, as was promised, all of the
rules of the Propositional Calculus are taken over into TNT. Therefore, one
theorem of TNT will be this one:

<so=Ov-so=o>

Typographical Number Theory 215