I'm reading through Gödel, Escher, Bach, and I found myself stuck at chapter 9. I've been rereading through several times already, but I must be missing something. To clarify my background, I'm a computer scientist, not a mathematician.
On page 273, D. R. Hofstadter states that
Could it be, therefore, that the means with which to answer any question about any formal system lies within just a single formal system-TNT? It seems plausible. Take, for instance, this question:
Is MU a theorem of the MIU-system?
Finding the answer is equivalent to determining whether 30 is a MIU number or not. Because it is a statement of number theory, we should expect that, with some hard work, we could figure out how to translate the sentence "30 is a MIU-number" into TNT-notation, in somewhat the same way as we figured out how to translate other number-theoretical sentences into TNT-notation.
I get it how the "statement of number theory"
b is a power of 2
can be translated to TNT. I can imagine that the statement
b is a power of 10
can be translated to TNT, even though it is very hard to do.
I'm beginning to lose it with translating the original statement
30 is a MIU number
to TNT. All right, still, maybe we can somehow translate the ideas from Mumon Shows Us How to Solve the MU-puzzle, p. 268 into TNT? Maybe.. but from the paragraph following this question it seems that Hofstadter takes the even more difficult road, first translating
b is a MIU number
into TNT, and then substituting b for SSSSSSSSSSSSSSSSSSSSSSSSSSSSSS0! He states that the task of translating b is a MIU number into TNT is difficult, but how should I believe him that it is at all possible (other than having some smart guy invent the translation)? Is it somehow obvious, that even though the translation is difficult, it must exist?
Hofstadter says that Because it is a statement of number theory, we should expect that, with some hard work, we could figure out how to translate the sentence "30 is a MIU-number" into TNT-notation. I must be missing something - I know that some number theory statements can be translated to TNT, but I'm not expecting that this particular one can be translated to TNT, and I'm not expecting at all that all number theory statements can be translated to TNT. I'm not even sure - is the b is a MIU number really a statement of number theory?
On the next page, 274, Hofstadter states that
... This state of affairs comes about because of two facts:
Fact 1. Statements such as "MU is a theorem" can be coded into number theory via Gödel’s isomorphism.
Fact 2. Statements of number theory can be translated into TNT.
It could be said that MUMON is, by Fact 1, a coded message, where the symbols of the code are, by Fact 2, just symbols of TNT.
I'm not sure that I understand these facts correctly. For Fact 1, I imagine something like that: MU is a theorem translates into 30 is a MIU-number. Is this understanding correct?
Fact 2 is the very one that isn't at all clear to me. Does that (amongst other things) mean, that all statements of the form
b is a SOME_FORMAL_SYSTEM-number
where SOME_FORMAL_SYSTEM = pq, MIU, TNT, whatever.. can be translated into TNT?
These facts seem to be very important to the understanding of the chapter... Hofstadter uses these as a jumping board for turning the Gödelization onto TNT itself on p. 278
α is a TNT-number
...Now it occurs to us that this new number-theoretical! predicate is expressible by some string of TNT with one free variable, say a.
Sorry, it does not at all occur to me. Being a TNT-number means being a number that is defined recursively from a set of highly complex arithmetic rules. I cannot even imagine the shape of the resulting TNT formula. Would the TNT form also use recursion in some way? Or is there some trick to "unroll" the recursion? I'm completely lost here.
I feel that without answering these questions, I can not continue to what's next and at least pretend that I understand what's going on. I feel kinda cheated - reading through 280 pages, and then get stuck on what was probably supposed to be the climax of the first part of the book, not being able to comprehend. Any help will be really appreciated.
UPDATE 1
I'm slowly digging through Mauro ALLEGRANZA answer.
Comment 1 seems to be easily understandable to me.
Now I'm pondering Comment 2 and 3. This is my current understanding of what's going on:
Having the arithmetical question from Comment 1
is c a MIU-producible number?
We can translate:
- this question (probably inseparably) along with a set of the arithmetic rules for generating MIU-producible numbers
- into a TNT predicate with one free variable.
More light on the method is shed in Comment 3, but basically it is just an immensely more complex variation of translating e. g. the arithmetic question
is c an even number?
into TNT (∃a:(SS0.a)=c).
After that, we'll substitute all the occurences of the free variable c in the TNT predicate by the numeral SSS...(30x)...0 and we'll obtain a TNT formula (no more free variables).
This TNT formula is isomorphically tied with the original question
is MU a theorem of the MIU-system?
in the following way:
- If the formula is a TNT theorem (a simple example of such formula:
(SSS0+0)=(0+SSS0)), it means that 30 is a MIU-producible number, and therefore MU is a MIU theorem. - If the TNT formula with prepended
~is a theorem, it means that 30 is not a MIU-producible number, and therefore MU is not a MIU theorem
Is the above correct? I hope so, so I can continue on my journey through the last comment and more GEB...
We can try with a step-by-step approach ...
Comment 1
The first basic concept is that of formal system i.e. a language (usually based on a finite alphabet of symbols) some rules for producing "well-formed" expressions (i.e. finite sequnces of symbols), some "initial" expressions (axiosm) and some rules for manipulating expressions, i.e. for generating new expressions from the set of already available ones.
$\mathsf {TNT}$ as well as $\mathsf {MIU}$ are formal systems.
You can see Gödel-Numbering the $\mathsf {MIU}$-System [ I'll not refer to page numbers, because my edition has a different paging ...] for the "encoding" of the system with "numerals" (i.e. symbols denoting numbers).
You can imagine to write a piece of code implementing $\mathsf {MIU}$-system rules : running the code you can generate "theorems", i.e. expressions; after encoding, those expressions will look like : $31, 311, 30110, \ldots$.
But you can ask yourself about some "feature" of the system, like the silly one : is $\mathsf {MIU}$-system able to generate the expression $20$ ? Of course not, because $2$ is not used in the coding of the alphabet of the system, and no rule of the system alllows us to "add" (or introduce) the symbol $2$.
This is the gist of the question :
i.e. are the rules of the system "able" to produce the expression $\mathsf {MU}$ ? which is the same as, given the encoding :
Comment 2
The second step is into Seeing Things Both Typographically and Arithmetically to "translate" the rule of the formal system $\mathsf {MIU}$ into rules for manipulating numbers.
Having done this [see Arithmetical Rule 1a, ... as well as the (only) axiom : We can make $31$] we can "play" a double game : with numbers (i.e. Arithmetically) and with symbols denoting numbers : the numerals (i.e. Typographically) :
Thus, our original question :
that we have translated, via encoding, into :
can now been rephrased into the language of $\mathsf {TNT}$ (because the question "speaks of" numbers and numbers are denoted by numerals, and we are asking for : "is $SS \ldots 0$ [with $30$ leading $S$] a string of $\mathsf {MIU}$ ?").
Thus :
Comment 3
The next step is one of Gödel's fundamental intuitions : see Gödel Numbering and The Diagonalization Lemma.
If you want to grasp the details, there is no other way than take a look at some mathematical logic textbook and study it.
But the idea is (nowadays) fundamentally simple; you are a computer scientist, and thus you must be familiar with programming, assembler and machine code.
With "low level" languages we are able to specify data and instructions for a machine; at the ground level, we have ony sequences of bits : $0,1$ that codify not only numbers, but every kind of data. In addition we encode with bits also instructions, i.e. rules.
This is the gist of Gödel's idea of arithmetization : with the seemingly limited resources of arithmetic, we can "codify" not only numbers and their properties, but also expressions and their properties, provided that they are "managed" according to a formal system (see above) i.e. according to a finite set of "algorithmic" rules.
Thus, we can define suitable arithmetic formulae encoding the properties of the formal system, like: being a (well-formed) expression, being an axiom and - finally - being a theorem of the formal system.
This allows Gödel (and Hofstadter) to express (again : via encoding) the question :
into "pure" arithmetical terms; the result will be something (very very complex in practice, but ideally simple) like the question :
Comment 4
Having said that, how it is possible that the property :
This fundamental result is obtained through a long exercise into encoding : i.e. a tour de force in machine code.
You can see this post for a concrete little exercise into encoding (alas! with a different encoding schema, i.e. a different "assembler language").
In it we can find how to "encode" the number-theoretical predicate $Even(x)$, i.e. a predicate (with one free variable) such that, for any number $n$, outputs $TRUE$ if $n$ is even and outputs $FALSE$ if $n$ is odd.
In first-order arithmetic $Even(x)$ is expressed as :
thus, we have to "encode" : $(\exists v_2 v_1 = v_2 \cdot SS0)$ i.e. :
Its encoding will be : $2^2 \cdot 3^6 \cdot 5^1 \cdot 7^{14} \cdot 11^2 \cdot 13^6 \cdot 17^{10} \cdot 19^{14} \cdot 23^{12} \cdot 29^{11} \cdot 31^{14} \cdot 37^5 \cdot 39^5 \cdot 43^3 \cdot 47^4 \cdot 53^4$.
Having computed it, we have the so-called Gödel number encoding the formula expressing $Even(x)$.
The same will happen with the "$\mathsf {TNT}$-theoretical" predicate $\mathsf {TNT}_{num}(x)$, i.e. a predicate (with one free variable) such that, for any number $\alpha$, outputs $TRUE$ if $\alpha$ is a $\mathsf {TNT}$-number and outputs $FALSE$ if $\alpha$ is not a $\mathsf {TNT}$-number.