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

q -

-the letters
p, q,
and the hyphen.

The pq-system has an infinite number of axioms. Since we can't write them all down, we have to have some other way of describing what they are. Actually, we want more than just a description of the axioms; we want a way to tell whether some given string is an axiom or not. A mere description of axioms might characterize them fully and yet weakly-which was the problem with the way theorems in the
MIU
-system were characterized. We don't want to have to struggle for an indeterminate-possibly infinite length of time, just to find out if some string is an axiom or not. Therefore, we will define axioms in such a way that there is an obvious decision procedure for axiomhood of a string composed of
p
's,
q
's, and hyphens.

DEFINITION: x
p
-
q
x is an axiom, whenever x is composed of hyphens only.

Note that 'x' must stand for the same string of hyphens in both occurrences For example, -

-
p-q
---is an axiom. The literal expression `
xp-qx
-' i,, not an axiom, of course (becausèx'

does not belong to the pq-system); it is more like a mold in which all axioms are cast-and it is called an axiom schema.

The
pq
-system has only one rule of production:

RULE: Suppose x, y, and z all stand for particular strings containing only hyphens. And suppose that x
p
y
q
z is known to be a theorem. Thè x
py-qz
- is a theorem.

For example, take x to be'--', y to be'---', and z to be'-'. The rule tells us: If --
p
---
q
- turns out to be a theorem, then so will --
p
----
q
--.

As is typical of rules of production, the statement establishes a causal connection between the theoremhood of two strings, but without asserting theoremhood for either one on its own.

A most useful exercise for you is to find a decision procedure for the theorems of the pq-system. It is not hard; if you play around for a while you will probably pick it up.

Try it.

The Decision Procedure

I presume you have tried it. First of all, though it may seem too obvious to mention, I would like to point out that every theorem of the pq-system has three separate groups of hyphens, and the separating elements are one
p
, and one
q
, in that order. (This can be shown by an argument based on "heredity", just the way one could show that all
MIU
-

system theorems had to begin with
M
.) This means that we can rule out, from its form alone, o string such as --
p--p--p--q
.

Now, stressing the phrase "from its form alone" may seem silly; what else is there to a string except its form? What else could possibly play a roll in determining its properties?

Clearly nothing could. But bear this in mint as the discussion of formal systems goes on; the notion of "form" will star to get rather more complicated and abstract, and we will have to think more about the meaning of the word "form". In any case, let us give the name
well formed string
to any string which begins with a hyphen-group, then ha one p, then has a second hyphen-group, then a q, and then a final hyphen-group.

Back to the decision procedure ... The criterion for theoremhood is that the first two hyphen-groups should add up, in length, to the third

hyphen-group. for instance
, --p--q -
is a theorem, since 2 plus 2 equals 4, whereas
--p--q-is not, since 2 plus 2 is not 1. To see why this is the proper criterion, look first at the axiom schema. Obviously, it only manufactures axioms which satisfy the addition criterion. Second, look at the rule of production. If the first string satisfies the addition criterion, so must the second one-and conversely, if the first string does not satisfy the addition criterion, then neither does the second string. The rule makes the addition criterion into a hereditary property of theorems: any theorem passes the property on to its offspring. This shows why the addition criterion is correct.

There is, incidentally, a fact about the pq-system which would enable us to say with confidence that it has a decision procedure, even before finding the addition criterion. That fact is that the pq-system is not complicated by the opposing currents of
lengthening and shortening
rules; it has only lengthening rules. Any formal system which tells you how to make longer theorems from shorter ones, but never the reverse, has got to have a decision procedure for its theorems. For suppose you are given a string. First check whether it's an axiom or not (I am assuming that there is a decision procedure for axiomhood-otherwise, things are hopeless). If it is an axiom, then it is by definition a theorem, and the test is over. So suppose instead that it's not an axiom. Then, to be a theorem, it must have come from a shorter string, via one of the rules. By going over the various rules one by one, you can pinpoint not only the rules that could conceivably produce that string, but also exactly which shorter strings could be its forebears on the

"family tree". In this way, you "reduce" the problem to determining whether any of several new but shorter strings is a theorem. Each of them can in turn be subjected to the same test. The worst that can happen is a proliferation of more and more, but shorter and shorter, strings to test. As you continue inching your way backwards in this fashion, you must be getting closer to the source of all theorems-the axiom schemata. You just can't get shorter and shorter indefinitely; therefore, eventually either you will find that one of your short strings is an axiom, or you'll come to a point where you're stuck, in that none of your short strings is an axiom, and none of them can be further shortened by running some rule or other backwards. This points out that there really is not much deep interest in formal systems with lengthening rules only; it is the interplay of lengthening and shortening rules that gives formal systems a certain fascination..

Bottom-up
vs
. Top-down

The method above might be called a
top-down
decision procedure, to be contrasted with a
bottom-up
decision procedure, which I give now. It is very reminiscent of the genie's systematic theorem-generating method for the
MIU
-system, but is complicated by the presence of an axiom schema. We are going to form a "bucket" into which we throw theorems as they are generated. Here is how it is done:

(1a)

Throw the simplest possible axiom
(-p-q--
) into the bucket.

(I b) Apply the rule of inference to the item in the bucket, and put the result into the bucket.

(2a) Throw the second-simplest axiom into the bucket.

(2b) Apply the rule to each item in the bucket, and throw all results into the bucket.

(3a) Throw the third-simplest axiom into the bucket.

(3b) Apply the rule to each item in the bucket, and throw all results into the bucket.

etc., etc.

A moment's reflection will show that you can't fail to produce every theorem of the pqsystem this way. Moreover, the bucket is getting filled with longer and longer theorems, as time goes on. It is again a consequence of that lack of shortening rules. So if you have a particular string, such as
--p---q
---- , which you want to test for theoremhood, just follow the numbered steps, checking all the while for the string in question. If it turns up-theorem! If at some point everything that goes into the bucket is longer than the string in question, forget it-it is not a theorem. This decision procedure is bottom=up because it is working its way up from the basics, which is to say the axioms. The previous decision procedure is top-down because it does precisely the reverse: it works its way back down towards the basics.

Isomorphisms Induce Meaning

Now we come to a central issue of this Chapter-indeed of the book. Perhaps you have already thought to yourself that the pq-theorems are like additions. The string
--p---q---
is a theorem because 2 plus 3 equals 5. It could even occur to you that the theorem
--p---q--

is a
statement
, written in an odd notation, whose
meaning
is that 2 plus 3 is 5. Is this a reasonable way to look at things? Well, I deliberately chose '
p
' to remind you of 'plus', and '
q
' to remind you of 'equals' . . . So, does the string
--p---q----
actually
mean
"2 plus 3 equals 5"?

What would make us feel that way? My answer would be that we have perceived an
isomorphism
between pq-theorems and additions. In the Introduction, the word

"isomorphism" was defined as an information preserving transformation. We can now go into that notion a little more deeply, and see it from another perspective. The word

"isomorphism' applies when two complex structures can be mapped onto each other, in such a way that to each part of one structure there is a corresponding part in the other structure, where "corresponding" means that the two part play similar roles in their respective structures. This usage of the word "isomorphism" is derived from a more precise notion in mathematics.

It is cause for joy when a mathematician discovers an isomorphism between two structures which he knows. It is often a "bolt from the blue", and a source of wonderment. The perception of an isomorphism between two known structures is a significant advance in knowledge-and I claim that it is such perceptions of isomorphism which create
meanings
in the minds of people. A final word on the perception of isomorphisms: since they come in many shapes and sizes, figuratively speaking, it is not always totally clear when you really have found an isomorphism. Thus, "isomorphism" is a word with all the usual vagueness of words-which is a defect but an advantage as well.

In this case, we have an excellent prototype for the concept of isomorphism.

There is a "lower level" of our isomorphism-that is, a mapping between the parts of the two structures:

p <= => plus

q <= => equals

- <= => one

-- <= => two

---- <= => three

etc.

This symbol-word correspondence has a name:
interpretation
.

Secondly, on a higher level, there is the correspondence between true statements and theorems. But-note carefully-this higher-level correspondence could not be perceived without the prior choice of an interpretation for the symbols. Thus it would be more accurate to describe it as a correspondence between true statements and
interpreted
theorems. In any case we have displayed a two-tiered correspondence, which is typical of all isomorphisms.

When you confront a formal system you know nothing of, and if you hope to discover some hidden meaning in it, your problem is how to assign interpretations to its symbols in a meaningful way-that is, in such a way that a higher-level correspondence emerges between true statements and theorems. You may make several tentative stabs in the dark before finding a good set of words to associate with the symbols. It is very similar to attempts to crack a code, or to decipher inscriptions in an unknown language like Linear B of Crete: the only way to proceed is by trial and error, based on educated guesses. When you hit a good choice, a "meaningful" choice, all of a sudden things just feel right, and work speeds up enormously. Pretty soon everything falls into place. The excitement of such an experience is captured in
The Decipherment of Linear
B
by John Chadwick.

But it is uncommon, to say the least, for someone to be in the position of

"decoding" a formal system turned up in the excavations of a ruined civilization!

Mathematicians (and more recently, linguists, philosophers, and some others) are the only users of formal systems, and they invariably have an interpretation in mind for the formal systems which they use and publish. The idea of these people is to set up a formal system whose

Theorems reflect some portion of reality isomorphically. In such a case, the choice of symbols is a highly motivated one, as is the choice of typographical rules of production.

When I devised the pq-system, I was in position. You see why I chose the symbols I chose. It is no accident theorems are isomorphic to additions; it happened because I deliberately sought out a way to reflect additions typographically.

Meaningless and Meaningful Interpretations

You can choose interpretations other than the one I chose. You need make every theorem come out true. But there would be very little reason make an interpretation in which, say, all theorems came out false, certainly even less reason to make an interpretation under which there is no correlation at all, positive or negative, between theoremhood and tri Let us therefore make a distinction between two types of interpretations a formal system. First, we can have a
meaningless
interpretation, one un which we fail to see any isomorphic connection between theorems of system, and reality.

Such interpretations abound-any random choice a will do. For instance, take this one:
p
<= => horse