Gödel, Escher, Bach: An Eternal Golden Braid (78 page)

came

into.)

Thank you, Mr. T, for your lucid clarification of that obscene telephone call.

Tortoise: And thank you, Achilles, for the pleasant promenade. I hope we meet again soon.

Propositions of TNT

and Related Systems'

The Two Ideas of the "Oyster"

THIS CHAPTER'S TITLE is an adaptation of the title of Gödel’s famous 1931 paper-

"
TNT
" having been substituted for "
Principia Mathematica
". Gödel’s paper was a technical one, concentrating on making his proof watertight and rigorous; this Chapter will be more intuitive, and in it I will stress the two key ideas which are at the core of the proof. The first key idea is the deep discovery that there are strings of
TNT
which can be interpreted as speaking about other strings of
TNT
; in short, that
TNT
, as a language, is capable of "introspection", or self-scrutiny. This is what comes from Gödel-numbering.

The second key idea is that the property of self scrutiny can be entirely concentrated into a single string; thus that string's sole focus of attention is itself. This "focusing trick" is traceable, in essence, to the Cantor diagonal method.

In my opinion, if one is interested in understanding Gödel’s proof. in a deep way, then one must recognize that the proof, in its essence, consists of a fusion of these two main ideas. Each of them alone is a master stroke; to put them together took an act of genius. If I were to choose, however, which of the two key ideas is deeper, I would unhesitatingly pick the first one-the idea of Gödel-numbering, for that idea is related to the whole notion of what meaning and reference are, in symbol-manipulating systems.

This is an idea which goes far beyond the confines of mathematical logic, whereas the Cantor trick, rich though it is in mathematical consequences, has little if any relation to issues in real life.

The First Idea: Proof-Pairs

Without further ado, then, let us proceed to the elaboration of the proof itself. We have already given a fairly careful notion of what the Gödel isomorphism is about, in Chapter IX. We now shall describe a mathematical notion which allows us to translate a statement such as "The string 0=0 is a theorem of
TNT
into a statement of number theory. This will involve the notion of
proof-pairs
. A proof-pair is a pair of natural numbers related in a particular way. Here is the idea:

Two natural numbers,
m
and
n
respectively, form a
TNT
proof-pair if and only if
m
is the Gödel number of a
TNT
derivation whose bottom line is the string with Gödel number
n.

The analogous notion exists with respect to the
MIU
-system, and it is a little easier on the intuition to consider that case first. So, for a moment, let us back off from
TNT
-proofpairs, and look at
MIU
-proof-pairs. Their definition is parallel: Two natural numbers,
m
and
n
respectively, form a
MIU
-proof pair if and only if
m
is the Gödel number of a
MIU
-system derivation whose bottom line is the string with Gödel number
n.

Let us see a couple of examples involving
MIU
-proof-pairs. First, let
m
=

3131131111301,
n
= 301. These values of m and n do indeed form a MIU-proof-pair, because m is the Gödel number of the
MIU
-derivation

MI

MII

MIIII

MUI

whose last line is
MUI
, having Gödel number 301, which is
n
. By contrast, let
m
=

31311311130, and
n
= 30. Why do these two values not form a
MIU
-proof-pair? To see the answer, let us write out the alleged derivation which
m
codes for: MI

MII

MIII

MU

There is an invalid step in this alleged derivation! It is the step from the second to the third line: from
MII
to
MIII
. There is no rule of inference in the
MIU
-system which permits such a typographical step. Correspondingly-and this is most crucial-there is no arithmetical rule of inference which carries you from 311 to 3111. This is perhaps a trivial observation, in light of our discussion in Chapter IX, yet it is at the heart of the Gödel isomorphism. What we do in any formal system has its parallel in arithmetical manipulations.

In any case, the values
m
= 31311311130,
n
= 30 certainly do not form a
MIU
-

proof-pair. This in itself does not imply that 30 is not a
MIU
-number. There could be another value of
m
which forms a
MIU
proof-pair with 30. (Actually, we know by earlier reasoning that
MU
is not a
MIU
-theorem, and therefore no number at all can form a
MIU
-proof-pair with 30.)

Now what about
TNT
proof pairs? Here are two parallel examples, one being merely an alleged
TNT
proof-pair, the other being a valid
TNT
proof-pair. Can you spot which is which? (Incidentally, here is where

thè611' codon comes in. Its purpose is to separate the Gödel numbers of successive lines in a
TNT
-derivation. In that sense, '611' serves as a punctuation mark. In the
MIU
-

system, the initial '3' of all lines is sufficient-no extra punctuation is needed.) (1)
m
= 626.262,636,223,123,262,111,666,611,223,123.666.111,666

n
= 123,666.111,666

(2)
m
=626,262.636,223.123,262,111,666,611223,333,262.636,123.262,111,666

n
= 223,333,262,636,123,262.111,666

It is quite simple to tell which one is which, simply by translating back to the old notation, and making some routine examinations to see

(1) whether the alleged derivation coded for by
m
is actually a legitimate derivation; (2) if so, whether the last line of the derivation coincides with the string which
n
codes for.

Step 2 is trivial; and step 1 is also utterly straightforward, in this sense: there are no open-ended searches involved, no hidden endless loops. Think of the examples above involving the
MIU
-system, and now just mentally substitute the rules of
TNT
for the
MIU
-system's rules, and the axioms of
TNT
for the
MIU
-system's one axiom. The algorithm in both cases is the same. Let me make that algorithm explicit: Go down the lines in the derivation one by one. Mark those which are axioms.

For each line which is not an axiom, check whether it follows by any of the rules of inference from earlier lines in the alleged derivation.

If all nonaxioms follow by rules of inference from earlier lines, then you have a legitimate derivation; otherwise it is a phony derivation.

At each stage, there is a clear set of tasks to perform, and the number of them is quite easily determinable in advance.

Proof-Pair-ness Is Primitive Recursive...

The reason I am stressing the boundedness of these loops is, as you may have sensed, that I am about to assert

FUNDAMENTAL FACT 1: The property of being a proof-pair is a primitive recursive number-theoretical property, and can therefore be tested for by a BlooP

program.

There is a notable contrast to be made here with that other closely related numbertheoretical property: that of being a
theorem-number
. To

assert that n is a theorem-number is to assert that
some
value of
m
exists which forms a proof-pair with
n
. (Incidentally, these comments apply equally well to
TNT
and to the
MIU
-system; it may perhaps help to keep both in mind, the
MIU
-system serving as a prototype.) To check whether
n
is a theorem-number, you must embark on a search through all its potential proof-pair "partners"
m
-and here you may be getting into an endless chase. No one can say how far you will have to look to find a number which forms a proof-pair with
n
as its second element. That is the whole problem of having lengthening and shortening rules in the same system: they lead to a certain degree of unpredictability.

The example of the Goldbach Variation may prove helpful at this point. It is trivial to test whether a pair of numbers (
m,n
) form a
Tortoise pair
: that is to say, both m and
n + m
should be prime. The test is easy because the property of primeness is primitive recursive: it admits of a predictably terminating test. But if we want to know whether
n
possesses the Tortoise property, then we are asking, "Does any number
m
form a Tortoise-pair with
n
as its second element?"-and this, once again, leads us out into the wild,
MU
-loopy unknown.

... And Is Therefore Represented in TNT

The key concept at this juncture, then, is Fundamental Fact 1 given above, for from it we can conclude

FUNDAMENTAL FACT 2: The property of forming a proof-pair is testable in BlooP, and consequently, it is
represented
in
TNT
by some formula having two free variables.

Once again, we are being casual about specifying which system these proof-pairs are relative to; it really doesn't matter, for both Fundamental Facts hold for any formal system. That is the nature of formal systems: it is always possible to tell, in a predictably terminating way, whether a given sequence of lines forms a proof, or not-and this carries over to the corresponding arithmetical notions.

The Power of Proof-Pairs

Suppose we assume we are dealing with the
MIU
-system, for the sake of concreteness.

You probably recall the string we called "
MUMON
", whose interpretation on one level was the statement "
MU
is a theorem of the MIU-system". We can show how
MUMON

would be expressed in
TNT
, in terms of the formula which represents the notion of
MIU
-

proof-pairs. Let us abbreviate that formula, whose existence we are assured of by Fundamental Fact 2, this way:

MIU-PROOF-PAIR {α,α´}

Since it is a property of two numbers, it is represented by a formula with two free variables. (Note: In this Chapter we shall always use austere
TNT
-so be careful to distinguish between the variables a, a', a".) In order to assert "
MU
is a theorem of the
MIU
-system", we would have to make the isomorphic statement "30 is a theorem-number of the
MIU
-system", and then translate that into
TNT
-notation. With the aid of our abbreviation, this is easy (remember also from Chapter VIII that to indicate the replacement of every a' by a numeral, we write that numeral followed by "/a' 1):
Зa:MIU-PROOF- PAIRja,SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSO/a'}

Count the
S's
: there are 30. Note that this is a closed sentence of
TNT
, because one free variable was quantified, the other replaced by a numeral. A clever thing has been done here, by the way. Fundamental Fact 2 gave us a way to talk about proof-pairs; we have figured out how to talk about theorem-numbers, as well: you just add an existential quantifier in front! A more literal translation of the string above would be, "There exists some number
a
that forms a
MlIJ
-proof-pair with 30 as its second element".

Suppose that we wanted to do something parallel with respect to
TNT
-say, to express the statement "0=0 is a theorem of
TNT
". We may abbreviate the formula which Fundamental Fact 2 assures us exists, in an analogous way (with two free variables, again):

TNT- PROOF- PAIR{a,a'}

(The interpretation of this abbreviated
TNT
-formula is: "Natural numbers a and a' form a TNT-proof-pair.") The next step is to transform our statement into number theory, following the
MUMON
-model above. The statement becomes "There exists some number a which forms a
TNT
proof-pair with 666,111,666 as its second element". The
TNT
-formula which expresses this is:

Зa:TNT-PROOF-PAI R{a,SSSSS SSSSSO/a' }

many, many 5's!

(in fact, 666,111,666 of them)

-a closed sentence of
TNT
. (Let us call it "
JOSHtU
", for reasons to appear momentarily.) So you see that there is a way to talk not only about the primitive recursive notion of
TNT
-proof-pairs, but also about the related but trickier notion of
TNT
-

theorem-numbers.

To check your comprehension of these ideas, figure out how to translate into
TNT

the following statements of meta-
TNT
:.

(1) 0=0 is not a theorem of
TNT
.

(2) ~0=0 is a theorem of
TNT
.

(3) ~0=0 is not a theorem of
TNT
.