Read Gödel, Escher, Bach: An Eternal Golden Braid Online
Authors: Douglas R. Hofstadter
Tags: #Computers, #Art, #Classical, #Symmetry, #Bach; Johann Sebastian, #Individual Artists, #Science, #Science & Technology, #Philosophy, #General, #Metamathematics, #Intelligence (AI) & Semantics, #G'odel; Kurt, #Music, #Logic, #Biography & Autobiography, #Mathematics, #Genres & Styles, #Artificial Intelligence, #Escher; M. C
How do the solutions differ from the example done above, and from each other' Here are a few more translation exercises.
(4) JOSHU is a theorem of
TNT
. (Call the
TNT
-string which expresses this
":METAJOSH t'".)
(5) META-JOSH[. is a theorem of TNT. (Call the TNT-string which expresses this
"META-META-JOSHC".)
(6)META-META-JOSHU is a theorem of TNT
(7)META-META- ME IA -JOSHU is a theorem of
TNT
(etc., etc.)
Example 5 shows that statements of meta-meta-TNT can be translated into TNT-notation; example 6 does the same for meta-meta-meta-TNT, etc.
It is important to keep in mind the difference between expressing a property, and
representing
it, at this point. The property of being a TNT theorem-number, for instance, is
expressed
by the formula
Зa:TNT- PROOF- PAI R{a,a' }
Translation: "a' is a
TNT
-theorem-number". However, we have no guarantee that this formula
represents
the notion, for we have no guarantee that this property is primitive recursive-in fact, we have more than a sneaking suspicion that it isn't. (This suspicion is well warranted. The property of being a TNT-theorem-number is not primitive recursive, and no TNT-formula can represent the property!) By contrast, the property of being a proof-pair, by virtue of its primitive recursivity, is both expressible and representable, by the formula already introduced.
Substitution Leads to the Second Idea
The preceding discussion got us to the point where we saw how
TNT
can "introspect" on the notion of
TNT
-theoremhood. This is the essence of the first part of the proof. We now wish to press on to the second major idea of the proof, by developing a notion which allows the concentration of this introspection into a single formula. To do this, we need to look at what happens to the Gödel number of a formula when you modify the formula structurally in a simple way. In fact, we shall consider this specific modification: replacement of all free variables by a specific numeral
. Below are shown a couple of examples of this operation in the left hand column, and in the right hand column are exhibited the parallel changes in Gödel numbers.
Formula
Gödel number
a=a
262,1 11,262
We now replace all
free variables by
the numeral for 2:
123,123,666,111.123,123,666
SSO=SSO
223,333,262,636,333,262,163,636,
3a:3a':a"=(SSa•SSa')
262,163,163,111,362,123,123,262,
236,123,123,262,163,323
We now replace all
free variables by
the numeral for 4:
223,333,262,636,333,262,163,636,
---3a:3a':SSSSO=(SSa•SSa')
123,123,123,123,666,111,362,123,
123,262,236,123,123,262,163,323
An isomorphic arithmetical process is going on in the right-hand column, in which one huge number is turned into an even huger number. The function which makes the new number from the old one would not be too difficult to describe arithmetically, in terms of additions, multiplications, powers of 10 and so on-but we need not do so. The main point is this: that the relation among (1) the original Gödel number, (2) the number whose numeral is inserted, and (3) the resulting Gödel number, is a primitive recursive relation. That is to say, a BlooP test could be written which, when fed as input any three natural numbers, says
YES
if they are related in this way, and
NO
if they aren't. You may test yourself on your ability to perform such a test-and at the same time convince yourself that there are no hidden open-ended loops to the process-by checking the following two sets of three numbers:
(1)
362,262,112,262,163,323,111,123,123,123,123,666;
2:
362,123,123,666,112,123,123,666,323,111,123,123,123,123,666.
(2)
223,362,123,666,236,123,666,323,111,262,163.
1
223,362,262,236,262,323,111,262,163;
As usual, one of the examples checks, the other does not. Now this relationship between three numbers will be called the substitution relationship. Because it is primitive recursive, it is represented by some formula of
TNT
having three free variables. Lets us abbreviate that TNT – formula by the following notation
SUB (a,a´,a´´)
Because this formula represents the substitution relationship, the formula shown below must be a
TNT
-theorem:
SU B{SSSSS SSSSSO/a,SSO/a',SSSSSS SSSSO/a"}
262,111,262 S's
123,123,666,111,123,123,666 S's
(This is based on the first example of the substitution relation shown in the parallel columns earlier in this section.) And again because the
SUB
formula represents the substitution relation, the formula shown below certainly is not a
TNT
-theorem:
SU B{SSSO/a,SSO/a',S0/a"}
Arithmoquining
We now have reached the crucial point where we can combine all of our disassembled parts into one meaningful whole. We want to use the machinery of the
TNT-PROOF
-
PAIR
and SUB formulas in some way to construct a single sentence of TNT whose interpretation is: "This very string of
TNT
is not a
TNT
-theorem." How do we do it%
Even at this point, with all the necessary machinery in front of us, the answer is not easy to find.
A curious and perhaps frivolous-seeming notion is that of substituting a formula's own Gödel number into itself. This is quite parallel to that other curious, and perhaps frivolous-seeming, notion of "quining" in the
Air on G's String
. Yet quining turned out to have a funny kind of importance, in that it showed a new way of making a self-referential sentence. Self reference of the Quine variety sneaks up on you from behind the first time you see it-but once you understand the principle, you appreciate that it is quite simple and lovely. The arithmetical version of quining-let's call it
arithmoquining
-will allow us to make a
TNT
-sentence which is "about itself ".
Let us see an example of arithmoquining. We need a formula with at least one free variable. The following one will do:
a=SO
This formula's Gödel number is 262,111,123,666, and we will stick this number into the formula itself-or rather, we will stick its numeral in. Here is the result:
SSSSS
SSSSSO=SO
262,111,123,666 S's
This new formula a asserts a silly falsity-that 262.111.123.666 equals 1: If we had begun with the string ~a=S0 and then arthmoquined, we would have cone up with a true statement—as you can see for yourself.
When you arithmoquine, you are of course performing a special case of the substitution operation we defined earlier. If we wanted to speak about arithmoquining inside
TNT
, we would use the formula
SUB{a" a" a'}
where the first two variables are the same. This comes from the fact that we are using a single number in two different ways (shades of the Cantor diagonal method!). The number a" is both (1) the original Gödel number, and (2) the insertion-number. Let us invent an abbreviation for the above formula:
ARITHMOQUINE{a", a'}
What the above formula says, in English, is:
a' is the Gödel number of the formula gotten by arithmoquining the formula with Gödel number a".
Now the preceding sentence is long and ugly. Let's introduce a concise and elegant term to summarize it. We'll say
a' is the arithmoquinification of a"
to mean the same thing. For instance, the arithmoquinification of 262,111,123,666 is this unutterably gigantic number:
123,123,123 123,123,123,666,111,123,666
262,111,123,666 copies of '1231
(This is just the Gödel number of the formula we got when we arithmoquined
a=SO
.) We can speak quite easily about arithmoquining inside
TNT
.
The Last Straw
Now if you look back in the
Air on G's String
, you will see that the ultimate trick necessary for achieving self-reference in Quine's way is to quine a sentence which itself talks about the concept of quining. It's not enough just to quine-you must quine a quine-mentioning sentence! All right, then the parallel trick in our case must be to arithmoquine some formula which itself is talking about the notion of arithmoquining!
Without further ado, we'll now write that formula down, and call it
G
's uncle
:
-3a:3a':
“uncle” has a Gödel number, of course, which we’ll call ù´
The head and tail of u's decimal expansion, and even a teeny bit of its midsection, can be read off directly:
u = 223,333,262,636,333,262,163,636,212, ... ,161, ... ,213
For the rest, we'd have to know just how the formulas
TNT-PROOF-PAIR
and
ARITHMOQUINE
actually look when written out. That is too complex, and it is quite beside the point, in any case.
Now all we need to do is-arithmoquine this very uncle! What this entails is
"booting out" all free variables-of which there is only one, namely a"-and putting in the numeral for u everywhere. This gives us:
-3a:3a':
And this, believe it or not, is Gödel’s string, which we can call '
G
'. Now there are two questions we must answer without delay. They are
(1) What Is
G
's Gödel number?
(2) What is the interpretation of G?
Question 1 first. How did we make
G
? Well, we began with the uncle, and arithmoquined it. So, by the definition of arithmoquinification,
G'
s Gödel number is the arithmoquinification of u.
Now question 2. We will translate
G
into English in stages, getting gradually more comprehensible as we go along. For our first rough try, we make a pretty literal translation:
"There do not exist numbers
a
and
a'
such that both (1) they form a
TNT
-proofpair. and (2)
a'
is the arithmoquinification of u."
Now certainly there is a number a' which is the arithmoquinification of u-so the problem must lie with the other number, a. This observation allows us to rephrase the translation of
G
as follows:
"There is no number
a
that forms a
TNT
-proof-pair with the arithmoquinification of u."
(This step, which can be confusing, is explained below in more detail.) Do you see what is happening?
G
is saying this:
"The formula whose Gödel number is the arithmoquinification
of u is not a theorem of
TNT
."
But-and this should come as no surprise by now-that formula is none other than
G
itself; whence we can make the ultimate translation of
G
; as
“
G
is not a theorem of
TNT
.”
-or if you prefer,
"I am not a theorem of
TNT
."
We have gradually pulled a high-level interpretation-a sentence of meta-
TNT
-out of what was originally a low-level interpretation-a sentence of number theory.
-
TNT Says "Uncle!"
The main consequence of this amazing construction has already been delineated in Chapter IX: it is the incompleteness of
TNT
. To reiterate the argument: Is
G
a
TNT
-theorem? If so, then it must assert a truth. But what in fact does
G
assert? Its own nontheoremhood. Thus from its theoremhood would follow its nontheoremhood: a contradiction.
Now what about
G
being a nontheorem? This is acceptable, in that it doesn't lead to a contradiction. But G's nontheoremhood is what
G
asserts-hence
G
asserts a truth. And since
G
is not a theorem, there exists (at least) one truth which is not a theorem of
TNT
.
Now to explain that one tricky step again. I will use another similar example. Take this string:
--3a:3a':
TNT
which you can write down yourself.
TENTH-POWER
{a",a'} represents the statement "a' is the tenth power of
a"".
The literal translation into English is then:
"There do not exist numbers a and a' such that both (1) they form a Tortoise-pair, and (2) a' is the tenth power of 2."
But clearly, there is a tenth power of 2-namely 1024. Therefore, what the string is really saying is that
"There is no number a that forms a Tortoise-pair with 1024"
which can be further boiled down to:
"1024 does not have the Tortoise property."
The point is that we have achieved a way of substituting a
description
of a number, rather than its numeral, into a predicate. It depends on using one °extra quantified variable (
a
').
Here, it was the number 1024 that was described as the “tenth power of 2”; above it was the number described as the arithmoquinification of a”.
"Yields Nontheoremhood When Arithmoquined"
Let us pause for breath for a moment, and review what has been done. The best way I know to give some perspective is to set out explicitly how it compares with the version of the Epimenides paradox due to Quine. Here is a map: