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

Something Is Missing

Now if you experiment around for a while with the rules and axioms of

TNT so far presented, you will find that you can produce the following

pyramidal family of theorems (a set of strings all cast from an identical mold,

differing from one another only in that the numerals 0, SO, SSO, and so on

have been stuffed in):

(0+0)=0

(O+SO)=SO

(O+SSO)=SSO

(O+SSSO)=SSSO

(O+SSSSO)=SSSSO

etc.

As a matter of fact, each of the theorems in this family can be derived from

the one directly above it, in only a couple of lines. Thus it is a sort of

"cascade" of theorems, each one triggering the next. (These theorems are

very reminiscent of the pq-theorems, where the middle and right-hand

groups of hyphens grew simultaneously.)

Now there is one string which we can easily write down, and which

summarizes the passive meaning of them all, taken together. That univer-

sally quantified summarizing string is this:

Va:(O+a)=a

Yet with the rules so far given, this string eludes production. Try to

produce it yourself if you don't believe me.

You may think that we should immediately remedy the situation with

the following

(PROPOSED) RULE OF ALL: If all the strings in a pyramidal family are theo-

rems, then so is the universally quantified string which summarizes

them.

The problem with this rule is that it cannot be used in the M-mode. Only

people who are thinking about the system can ever know that an infinite set

of strings are all theorems. Thus this is not a rule that can be stuck inside

any formal system.

w-Incomplete Systems and Undecidable Strings

So we find ourselves in a strange situation, in which we can typographically
produce theorems about the addition of any specific numbers, but even such
a simple string as the one above, which expresses a property of addition in
general, is not a theorem. You might think that is not all that strange, since
we were in precisely that situation with the pq-system. However, the pq-
system had no pretensions about what it ought to be able to do; and in fact

Typographical Number Theory 221