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

Vc:(c+d)=(d+c)

premise

(38)

(c+d)=(d+c)

specification

(39)

S(c+d)=S(d+c)

add S

(40)

(c+Sd)=S(c+d)

carry over 30

(41)

(c+Sd)=S(d+c)

transitivity

(42)

S(d+c)=(d+Sc)

carry over 33

(43)

(c+Sd)=(d+Sc)

transitivity

(44)

(d+Sc)=(Sd+c)

carry over 35

(45)

(c+Sd)=(Sd+c)

transitivity

(46)

Vc:(c+Sd)=(Sd+c)

generalization

(47)
]

pop

(48)
⊃
Vc:(c+Sd)=(Sd+c)>

fantasy rule

(49)
Vd:< Vc:(c+d)=(d+c)
⊃
Vc:(c+Sd)=(Sd+c)>

generalization

[If
d
commutes with every c, then
Sd
does too.

* * * * *

specification (line 20)

(51)
Va:(O+a)=a

previous theorem

(52)
(O+c)=c

specification

(53)
c=(O+c)

symmetry

(54)
(c+0)=(0+c)

transitivity (lines 50,53)

(55)
Vc:(c+0)=(O+c)

generalization

[
0
commutes with every
c
.]

(56)
Vd: Vc:(c+d)=(d+c)

induction (lines 49,55)

[Therefore, every
d
commutes with every
c
.]

Tension and Resolution in TNT

TNT
has proven the commutativity of addition. Even if you do not follow this derivation in detail, it is important to realize that, like a piece of music, it has its own natural

"rhythm". It is not just a random walk that happens to have landed on the desired last line. I have inserted "breathing marks” to show some of the "phrasing" of this derivation.

Line 28 in particular turning point in the derivation, something like the halfway point it
AABB
type of piece, where you resolve momentarily, even if not in the t key. Such important intermediate stages are often called "lemmas".

It is easy to imagine a reader starting at line 1 of this derivation ignorant of where it is to end up, and getting a sense of where it is going as he sees each new line. This would set up an inner tension, very much the tension in a piece of music caused by chord progressions that let know what the tonality is, without resolving. Arrival at line 28 w, confirm the reader's intuition and give him a momentary feeling of satisfaction while at the same time strengthening his drive to progress tow what he presumes is the true goal.

Now line 49 is a critically important tension-increaser, because of "almost-there"

feeling which it induces. It would be extremely unsatisfactory to leave off there! From there on, it is almost predictable how things must go. But you wouldn't want a piece of music to quit on you just when had made the mode of resolution apparent. You don't want to
imagine
ending-you want to
hear
the ending. Likewise here, we have to c things through. Line 55 is inevitable, and sets up all the final tension which are resolved by Line 56.

This is typical of the structure not only of formal derivations, but of informal proofs. The mathematician's sense of tension is intimately related to his sense of beauty, and is what makes mathematics worthy doing. Notice, however, that in
TNT
itself, there seems to be no reflection of these tensions. In other words,
TNT
doesn't formalize the notions of tension and resolution, goal and subgoal, "naturalness" and "inevitable any more than a piece of music is a book about harmony and rhythm. Could one devise a much fancier typographical system which is
aware
of the tensions and goals inside derivations?

Formal Reasoning vs. Informal Reasoning

I would have preferred to show how to derive Euclid's Theorem (the infinitude of primes) in
TNT
, but it would probably have doubled the length of the book. Now after this theorem, the natural direction to go would be to prove the associativity of addition, the commutativity and associativity of multiplication and the distributivity of multiplication over addition. These would give a powerful base to work from.

As it is now formulated,
TNT
has reached "critical mass" (perhaps a strange metaphor to apply to something called "
TNT
"). It is of the same strength as the system of
Principia Mathematica
; in TNT one can now prove every theorem which you would find in a standard treatise on number theory. Of course, no one would claim that deriving theorems in
TNT
is the best way to do number theory. Anybody who felt that way would fall in the same class of people as those who think that the best way to know what 1000 x 1000 is, is to draw a 1000 by 1000 grid, and count all the squares in it ... No; after total formalization, the only way to go is towards relaxation of the formal system. Otherwise, it is so enormously unwieldy as to be, for all practical purposes, useless. Thus, it is important to embed
TNT
within a wider context, a context which enables new rules of inference to be derived, so that derivations can be speeded up. This would require formalization of the language in which rules of inference are expressed-that is, the metalanguage. And one could go considerably further. However, none of these speeding-up tricks would make
TNT
any more
powerful
; they would simply make it more
usable
.

The simple fact is that we have put into
TNT
every mode of thought that number theorists rely on. Embedding it in ever larger contexts will not enlarge the space of theorems; it will just make working in
TNT
-or in each "new, improved version"-look more like doing conventional number theory.

Number Theorists Go out of Business

Suppose that you didn't have advance knowledge that
TNT
will turn out to be incomplete, but rather, expected that it is complete-that is, that every true statement expressible in the
TNT
-notation is a theorem. In that case, you could make a decision procedure for all of number theory. The method would be easy: if you want to know if
N
-

statement X is true or false, code it into
TNT
-sentence x. Now if X is true, completeness says that
x
is a theorem; and conversely, if not-X is true, then completeness says that
~x
is a theorem. So either
x
or
~x
must be a theorem, since either X or not-X is true. Now begin systematically enumerating all the theorems of
TNT
, in the way we did for the
MIU
-system and pq-system. You must come to
x
or
~x
after a while; and whichever one you hit tells you which of X and not-X is true. (Did you follow this argument? It crucially depends on your being able to hold separate in your mind the formal system
TNT
and its informal counterpart
N
. Make sure you understand it.) Thus, in prince-ple, if
TNT
were complete, number theorists would be put out of business any question in their field could be resolved, with sufficient time, in a purely mechanical way. As it turns out, this is impossible, which, depending on your point of view, is a cause either for rejoicing, or for mourning.

Hilbert's Program

The final question which we will take up in this Chapter is whether should have as much faith in the consistency of
TNT
as we did consistency of the Propositional Calculus; and, if we don't, whether possible to increase our faith in
TNT
, by
proving
it to be consistent could make the same opening statement on the "obviousness" of
TNT
’s consistency as Imprudence did in regard to the Propositional Calculus namely, that each rule embodies a reasoning principle which we believe in, and therefore to question the consistency of
TNT
is to question our own sanity. To some extent, this argument still carries weight-but not quite so much weight as before. There are just too many rules of inference and some of them just might be slightly "off ". Furthermore, how do we know that this mental model we have of some abstract entities called "natural numbers" is actually a coherent construct? Perhaps our own thought processes, those informal processes which we have tried to capture in the formal rules of the system, are themselves inconsistent! It is of course not the kind of thing we expect, but it gets more and more conceivable that our thoughts might lead us astray, the more complex the subject matter gets-and natural numbers are by no means a trivial subject matter. Prudence's cry for a
proof
of consistency has to be taken more seriously in this case. It's not that we seriously doubt that
TNT
could be inconsistent but there is a
little
doubt, a flicker, a glimmer of a doubt in our minds, and a proof would help to dispel that doubt.

But what means of proof would we like to see used? Once again, faced with the recurrent question of circularity. If we use all the equipment in a proof
about
our system as we have inserted into it, what will we have accomplished? If we could manage to convince ourselves consistency of
TNT
, but by using a weaker system of reasoning than we will have beaten the circularity objection! Think of the way a heavy rope is passed between ships (or so I read when I was a kid): first a light arrow is fired across the gap, pulling behind it a thin rope. Once a connection has been established between the two ships this way, then the heavy rope pulled across the gap. If we can use a "light" system to show that a system is consistent, then we shall have really accomplished something.

Now on first sight one might think there is a thin rope. Our goal is to prove that
TNT
has a certain typographical property (consistency): that no theorems of the form
x
and .
~x
ever occur. This is similar to trying to show that
MU
is not a theorem of the
MIU
-system. Both are statements about
typographical
properties of symbol-manipulation systems. The visions of a thin rope are based on the presumption that
facts
about number theory won’t be

needed
in proving that such a typographical property holds. In other words, if properties of integers are not used-or if only a few extremely simple ones are used-then we could achieve the goal of proving
TNT
consistent, by using means which are weaker than its own internal modes of reasoning.

This is the hope which was held by an important school of mathematicians and logicians in the early part of this century, led by David Hilbert. The goal was to prove the consistency of formalizations of number theory similar to
TNT
by employing a very restricted set of principles of reasoning called "finitistic" methods of reasoning. These would be the thin rope. Included among finitistic methods are all of propositional reasoning, as embodied in the Propositional Calculus, and additionally some kinds of numerical reasoning. But Gödel’s work showed that any effort to pull the heavy rope of
TNT's
consistency across the gap by using the thin rope of finitistic methods is doomed to failure. Gödel showed that in order to pull the heavy rope across the gap, you can't use a lighter rope; there just isn't a strong enough one. Less metaphorically, we can say:
Any
system that is strong enough to prove
TNT
's consistency is at least as strong as
TNT

itself.
And so circularity is inevitable.

A Mu Offering

The Tortoise and Achilles have just been to hear a lecture on the origins of the
Genetic Code, and are now drinking some tea at Achilles' home.

Achilles: I have something terrible to confess, Mr. T.

Tortoise: What is it, Achilles?

Achilles: Despite the fascinating subject matter of that lecture, I drifter to sleep a time or two. But in my drowsy state, I still was semi-awake aware of the words coming into my ears. One strange image that floated up from my lower levels was that À' and `T', instead of standing "adenine" and "thymine", stood for my name and yours-and double-strands of
DNA
had tiny copies of me and you along backbones, always paired up, just as adenine and thymine always Isn't that a strange symbolic image?

Tortoise: Phooey! Who believes in that silly kind of stuff? Anyway, about `C' and `G'?

Achilles: Well, I supposèC' could stand for Mr. Crab, instead o cytosine. I'm not sure about `G', but I'm sure one could thin something. Anyway, it was amusing to imagine my DNA being with minuscule copies of you-as well as tiny copies of myself, for matter. Just think of the infinite regress THAT leads to!

Tortoise: I can see you were not paying too much attention to the lecture.

Achilles: No, you're wrong. I was doing my best, only I had a hard keeping fancy separated from fact. After all, it is such a strange netherworld that those molecular biologists are exploring.

Tortoise: How do you mean?

Achilles: Molecular biology is filled with peculiar convoluted loops which I can't quite understand, such as the way that folded proteins, which are coded for in DNA, can loop back and manipulate the DNA which came from, possibly even destroying it.