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

Rounding Out the List of Rules

We have not yet stated all the rules of the Propositional Calculus. The complete set of rules is listed below, including the three new ones.

JOINING RULE: If x and y are theorems, then < x∧y> is a theorem.

SEPARATION RULE: If < x∧y> is a theorem, then both x and y are theorems.

DOUBLE-TILDE RULE: The string '~~' can be deleted from any theorem can also be inserted into any theorem, provided that the result string is itself well-formed.

FANTASY RULE: If y can be derived when x is assumed to be a theorem then < x⊃y> is a theorem.

CARRY-OVER RULE: Inside a fantasy, any theorem from the "reality" c level higher can be brought in and used.

RULE OF DETACHMENT: If x and < x⊃y> are both theorems, then y is a theorem.

CONTRAPOSITIVE RULE: and <~y⊃~x> are interchangeable DE MORGAN'S RULE: <~x∧~y> and ~< x∨y> are interchangeable.

SWITCHEROO RULE: and <~x⊃y> are interchangeable.

(The Switcheroo rule is named after Q. q. Switcheroo, an Albanian railroad engineer who worked in logic on the siding.) By "interchangeable" in foregoing rules, the following is meant: If an expression of one form occurs as either a theorem or part of a theorem, the other form may be

substituted, and the resulting string will also be a theorem. It must be kept in mind that the symbols ‘x’ and ‘y’ always stand for well-formed strings of the system.

Justifying the Rules

Before we see these rules used inside derivations, let us look at some very short justifications for them. You can probably justify them to yourself better than my examples – which is why I only give a couple.

The contrapositive rule expresses explicitly a way of turning around conditional statements which we carry out unconsciously. For instance, the “Zentence” If you are studying it, then you are far from the Way

Means the same thing as

If you are close to the Way, then you are not studying it.

De Morgan’s rule can be illustrated by our familiar sentence “The flag is not moving and the wind is not moving”. If
P
symbolizes “the flag is not moving”, and
Q

symbolizes “the wind is moving”, then the compound sentence is symbolized by

<
~P
∧
~Q
>, which, according to Morgan’s law, is interchangeable with
~∨
Q>.
whose interpretation would be “It is not true that either the flag or the wind is moving”. And no one could deny that it is a Zensible conclusion to draw.

For the Switrcheroo rule, consider the sentence “Either a cloud is hanging over the mountain, or the moonlight is penetrating the waves of the lake,” which might be spoken, I suppose, by a wistful Zen master remembering a familiar lake which he can visualize mentally but cannot see. Now hang on to your seat, for the Swircheroo rule tells us that this is interchangeable with the thought “If a cloud is not hanging over the mountain, then the moonlight is penetrating the waves of the lake.” This may not be enlightenment, but it is the best the Propositional Calculus has to offer.

Playing around with the system

Now, let us apply these rules to a previous theorem, ands see what we get: For instance, take the theorem
⊃
~~P>
:

⊃
~~P>
:

old theorem

<~~~P
⊃
~P>
:

contrapositive

<~P
⊃
~P>

double-tilde

∨
~P>

switcheroo

This new theorem, when interpreted, says:

Either this mind is Buddha, or this mind is not Buddha

Once again, the interpreted theorem, though perhaps less than mind boggling, is at least true.

Semi-Interpretations

It is natural, when one reads theorems of the Propositional Calculus out loud, to interpret everything but the atoms. I call this semi-interpreting. For example, the semi-interpretation of
∨
~P>
:: would be

P
or not
P
.

Despite the fact that P is not a sentence, the above semisentence still sounds true, because you can very easily imagine sticking any sentence in for P – and the form of the semi-interpreted theorem assures you that however you make your choice, the resulting sentence will be true. And that is the key idea of the Propositional Calculus: it produces theorems which, when semi-interpreted, are seen to be “universally true semisaentences”, by which is meant that no matter how you complete the interpretation, the final result will be a true statement.

Ganto’s Ax

Now we can do a more advanced exercise, based on a Zen koan called “Ganto’s Ax”.

Here is how it began.

One day Tokusan told his student Ganto, “I have two monks who have been here for many years. Go and examine them.” Ganto picked up an ax and went to the hut where the two monks were meditating. He raised the ax, saying “If you say a word, I will cut off your heads; and if you do not say a word, I will also cut off your heads.”1

If you say a word I will cut off this koan, and if you do not say a word, I will also cut off this koan – because I want you to translate some of it into our notation. Let us symbolize

“you say a word” by
P
and “I will cut off your heads” by
Q
. Then Ganto’s ax threat is symbolized by the string
<⊃
Q>
∧
<~`P
⊃
Q>>
. What if this ax threat were an axiom?

Here is a fantasy to answer that question.

(1) [

push

(2)
<⊃
Q>
∧
<~`P
⊃
Q>>
.

Ganto’s axiom

(3)
⊃
Q>

separation

(4)
<~Q
⊃
~P>
.

contrapositive

(5) <~
P
⊃
Q>

separation

(6)
<~Q
⊃
~~P>
.

contrapositive

(7) ]

push again

(8) ~
Q

premise

(9)
<~Q
⊃
~P>
.

carry-over of line 4

(10)
~P

detachment

(11)
<~Q
⊃
~~P>
.

carry-over of line 6

(12)
~~P

detachment (lines 8 and 11)

(13) <
~P
∧
~~P>

joining

(14) <
~P
∨
~~P>

De Morgan

(15) ]

pop once

(16)
<~Q
⊃
~∨
~P>>
.

fantasy rule

(17)
<~P
∨
~P>
⊃
Q>
.

contrapositive

(18) [

push

(19) .
~P

premise (also outcome)

(20) ]

pop

(21)
<~P
⊃
~P>
.

fantasy rule

(22)
∨
~P>
.

switcheroo

(23)
Q

detachment (lines 22 and 17)

(24) ]

pop out

The power of the Propositional Calculus is shown in this example. Why, in but two dozen steps, we have deduced Q: that the heads will be cut off! (Ominously, the rule last invoked was "detachment" ...) It might seem superfluous to continue the koan now, since we know what must ensue ... However, I shall drop my resolve to cut the koan off; it is a true Zen koan, after all. The rest of the incident is here related: Both monks continued their meditation as if he had not spoken. Ganto dropped the ax and said, "You are true Zen students." He returned to Tokusan and related the incident. "I see your side well," Tokusan agreed, "but tell me, how is their side?"

"Tõzan may admit them," replied Ganto, "but they should not be admitted under Tokusan."2

Do you see my side well? How is the Zen side?

Is There a Decision Procedure for Theorems?

The Propositional Calculus gives us a set of rules for producing statements which would be true in all conceivable worlds. That is why all of its theorems sound so simple-minded; it seems that they have absolutely no content! Looked at this way, the Propositional Calculus might seem to be a waste of time, since what it tells us is absolutely trivial. On the other hand, it does it by specifying the
form
of statements that are universally true, and this throws a new kind of light onto the core truths of the universe: they are not only fundamental, but also
regular
: they can be produced by one set of typographical rules. To put it another way, they are all "cut from the same cloth". You might consider whether the same could be said about Zen koans: could they all be produced by one set of typographical rules?

It is quite relevant here to bring up the question of a decision procedure. That is, does there exist any mechanical method to tell nontheorems from theorems? If so, that would tell us that the set of theorems of the

Propositional Calculus is not only r.e., but also recursive. It turns out that there is an interesting decision procedure-the method of truth u would take us a bit afield to present it here; you can find it in almost any standard book on logic. And what about Zen koans?

Could there conceivably be a mechanical decision procedure which distinguishes genuine Zen koans from other things?

Do We Know the System Is Consistent?

Up till now, we have only
presumed
that all theorems, when interpreted as indicated, are true statements. But do we
know
that that is the case' we prove it to be? This is just another way of asking whether the intended interpretations ('and' for `∧', etc.) merit being called the "passive meanings” of the symbols. One can look at this issue from two very different points of view, which might be called the "prudent" and "imprudent" points I will now present those two sides as I see them, personifying their as "Prudence" and

"Imprudence".

Prudence: We will only KNOW that all theorems come out true un intended interpretation if we manage to PROVE it. That is the c: thoughtful way to proceed.

Imprudence: On the contrary. It is OBVIOUS that all theorems will come out true. If you doubt me, look again at the rules of the system. You will find that each rule makes a symbol act exactly as the word it represents ought to be used. For instance, the joining rule makes the symbol ‘∧’ act as ànd' ought to act; the rule of detachment makes `⊃'

act as it ought to, if it is to stand for 'implies', or 'if-then'; and so on. Unless you are like the Tortoise, you will recognize in each rule a codification of a pattern you use in your own thought patterns. So if you trust your own thought patterns, then you HAVE

to believe that all theorems come out true! That's the way I see it. I don't need any further proof. If you think that some theorem comes out false, then presumably you think that some rule must be wrong. Show me which one.

Prudence: I'm not sure that there is any faulty rule, so I can't point one out to you. Still, I can imagine the following kind of scenario. You, following the rules, come up with a theorem -- say x. Meanwhile I, also following the rules, come up with another theorem-it happens to be ~x. Can't you force yourself to conceive of that?

Imprudence: All right; let's suppose it happened. Why would it bother you? Or let me put it another way. Suppose that in playing with the
MIU
-system, I came up with a theorem x, and you came up with xU Can you force yourself to conceive of that?

Prudence: Of course-in fact both
MI
and
MIU
are theorems.

Imprudence: Doesn't that bother you?

Prudence: Of course not. Your example is ridiculous, because
MI
and
MIU
are not CONTRADICTORY, whereas two strings x and ~x in the Propositional Calculus ARE contradictory.

Imprudence: Well, yes -- provided you wish to interpret `~' as `not'. But what would lead you to think that '~' should be interpreted as `not'?

Prudence: The rules themselves. When you look at them, you realize that the only conceivable interpretation for '~' is 'not'-and likewise, the only conceivable interpretation for `∧' is ànd', etc.

Imprudence: In other words, you are convinced that the rules capture the meanings of those words?

Prudence: Precisely.

Imprudence: And yet you are still willing to entertain the thought that both x and ~x could be theorems? Why not also entertain the notion that hedgehogs are frogs, or that 1 equals 2, or that the moon is made of green cheese? I for one am not prepared even to consider whether such basic ingredients of my thought processes are wrong --

because if I entertained that notion, then I would also have to consider whether my modes of analyzing the entire question are also wrong, and I would wind up in a total tangle.

Prudence: Your arguments are forceful ... Yet I would still like to see a PROOF that all theorems come out true, or that x and ~x can never both be theorems.

Imprudence: You want a proof. I guess that means that you want to be more convinced that the Propositional Calculus is consistent than you are convinced of your own sanity. Any proof I could think of would involve mental operations of a greater complexity than anything in the Propositional Calculus itself. So what would it prove?

Your desire for a proof of consistency of the Propositional Calculus makes me think of someone who is learning English and insists on being given a dictionary which definers all the simple words in terms of complicated ones...