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

The Carroll Dialogue Again

This little debate shows the difficulty of trying to use logic and reasoning to defend themselves. At some point, you reach rock bottom, and there is no defense except loudly shouting, "I know I'm right!" Once again, we are up against the issue which Lewis Carroll so sharply set forth in his Dialogue: you can't go on defending your patterns of reasoning forever. There comes a point where faith takes over.

A system of reasoning can be compared to an egg. An egg has a shell which protects its insides. If you want to ship an egg somewhere, though, you don't rely on the shell. You pack the egg in some sort of container, chosen according to how rough you expect the egg's voyage to be. To be extra careful, you may put the egg inside several nested boxes. However, no matter how many layers of boxes you pack your egg in, you can imagine some cataclysm which could break the egg. But that doesn't mean that you'll never risk transporting your egg. Similarly, one can never give an ultimate, absolute proof that a proof in some system is correct. Of course,

one can give a proof of a proof, or a proof of a proof of a proof – but the validity of the outermost system always remains an unproven assumption, accepted on faith. One can always imagine that some unsuspected subtlety will invalidate every single level of proof down to the bottom, and tI "proven" result will be seen not to be correct after all. But that doesn’t mean that mathematicians and logicians are constantly worrying that the whole edifice of mathematics might be wrong. On the other hand, unorthodox proofs are proposed, or extremely lengthy proofs, or proofs generated by computers, then people do stop to think a bit about what they really mean by that quasi-sacred word "proven".

An excellent exercise for you at this point would be to go back Carroll Dialogue, and code the various stages of the debate into our notation -- beginning with the original bone of contention:

Achilles: If you have
<∧
B>
⊃
Z>,
and you also have
∧
B>,
then surely you have Z.

Tortoise: Oh! You mean:
<<<∧
B>
⊃
Z>
∧
∧
B>>
⊃
Z>,
: don't you?

(Hint: Whatever Achilles considers a rule of inference, the Tortoise immediately flattens into a mere string of the system. If you use or letters
A, B
, and
Z
, you will get a recursive pattern of longer and strings.)

Shortcuts and Derived Rules

When carrying out derivations in the Propositional Calculus, one quickly invents various types of shortcut, which are not strictly part of the system For instance, if the string

∨
~Q>
were needed at some point, and
∨
~P>
had been derived earlier, many people would proceed as if
∨
~Q>
had been derived, since they know that its derivation is an exact parallel to that of
∨
~P>.
The derived theorem is treated as a "theorem schema" --

a mold for other theorems. This turns out to be a perfect valid procedure, in that it always leads you to new theorems, but it is not a rule of the Propositional Calculus as we presented it. It is, rather, a
derived rule
, It is part of the knowledge which we have
about
the system. That this rule keeps you within the space of theorems needs proof, of course-but such a proof is not like a derivation inside the system. It is a proof in the ordinary, intuitive sense -- a chain of reasoning carried out in the I-mode. The theory about the Propositional Calculus is a "metatheory", and results in it can be called "metatheorems" -

Theorems about theorems. (Incidentally, note the peculiar capitalization in the phrase

"Theorems about theorems". It is a consequence of our convention: metatheorems are Theorems (proven results) concerning theorems (derivable strings).) In the Propositional Calculus, one could discover many metatheorems, or derived rules of inference. For instance, there is a De Morgan's Rule:

<~x∨~y> and ~ are interchangeable.

If this were a rule of the system, it could speed up many derivations considerably. But if we
prove
that it is correct, isn't that good enough? Can't we use it just like a rule of inference, from then on?

There is no reason to doubt the correctness of this particular derived rule. But once you start admitting derived rules as part of your procedure in the Propositional Calculus, you have lost the formality of the system, since derived rules are derived informally-outside the system. Now formal systems were proposed as a way to exhibit every step of a proof explicitly, within one single, rigid framework, so that any mathematician could check another's work mechanically. But if you are willing to step outside of that framework at the drop of a hat, you might as well never have created it at all. Therefore, there is a drawback to using such shortcuts.

Formalizing Higher Levels

On the other hand, there is an alternative way out. Why not formalize the metatheory, too? That way, derived rules (metatheorems) would be theorems of a larger formal system, and it would be legitimate to look for shortcuts and derive them as theorems-that is, theorems of the formalized metatheory-which could then be used to speed up the derivations of theorems of the Propositional Calculus. This is an interesting idea, but as soon as it is suggested, one jumps ahead to think of metametatheories, and so on. It is clear that no matter how many levels you formalize, someone will eventually want to make shortcuts in the top level.

It might even be suggested that a theory of reasoning could be identical to its own metatheory, if it were worked out carefully. Then, it might seem, all levels would collapse into one, and thinking
about
the system would be just one way of working in the system! But it is not that easy. Even if a system can "think about itself", it still is not
outside
itself. You, outside the system, perceive it differently from the way it perceives itself. So there still is a metatheory-a view from outside-even for a theory which can

"think about itself" inside itself. We will find that there are theories which can "think about themselves". In fact, we will soon see a system in which this happens completely accidentally, without our even intending it! And we will see what kinds of effects this produces. But for our study of the Propositional Calculus, we will stick with the simplest ideas-no mixing of levels.

Fallacies can result if you fail to distinguish carefully between working in the system (the
M
-mode) and thinking about the system (the
I
-mode). For example, it might seem perfectly reasonable to assume that, since
∨
~P>
(whose semi-interpretation is

"either
P
or not
P
") is a theorem, either
P
or ~
P
must be a theorem. But this is dead wrong: neither one of the latter pair is a theorem. In general, it is a dangerous practice to assume that symbols can be slipped back and forth between different levels-here, the language of the formal system and its metalanguage (English).

Reflections on the Strengths and Weaknesses of the System

You have now seen one example of a system with a purpose-to re part of the architecture of logical thought. The concepts which this handles are very few in number, and they are very simple, precise co But the simplicity and precision of the Propositional Calculus are the kinds of features which make it appealing to mathematicians. There are two reasons for this. (1) It can be studied for its own properties, ex geometry studies simple, rigid shapes. Variants can be made on it, employing different symbols, rules of inference, axioms or axiom schemata on. (Incidentally, the version of the Propositional Calculus here pr is related to one invented by G. Gentzen in the early 1930's. The other versions in which only one rule of inference is used-detachment usually-and in which there are several axioms, or axiom schemata study of ways to carry out propositional reasoning in elegant formal systems is an appealing branch of pure mathematics. (2) The Propositional Calculus can easily be extended to include other fundamental aspects of reasoning. Some of this will be shown in the next Chapter, where the Propositional Calculus is incorporated lock, stock and barrel into a much larger and deeper system in which sophisticated number-theoretical reasoning can be done.

Proofs
vs.
Derivations

The Propositional Calculus is very much like reasoning in some w one should not equate its rules with the rules of human thought. A
proof
is something informal, or in other words a product of normal thought written in a human language, for human consumption.

All sorts of complex features of thought may be used in proofs, and, though they may

“feel right", one may wonder if they can be defended logically. That is really what formalization is for. A
derivation
is an artificial counterpart of and its purpose is to reach the same goal but via a logical structure whose methods are not only all explicit, but also very simple.

If -- and this is usually the case -it happens that a formal derivation is extremely lengthy compared with the corresponding "natural" proof that is just too bad. It is the price one pays for making each step so simple. What often happens is that a derivation and a proof are "simple" in complementary senses of the word. The proof is simple in that each step sounds right", even though one may not know just why; the derivation is simple in that each of its myriad steps is considered so trivial that it is beyond reproach, and since the whole derivation consists just of such trivial steps it is supposedly error-free. Each type of simplicity, however, brings along a characteristic type of complexity.

In the case of proofs, it is the complexity of the underlying system on which they rest --

namely, human language -- and in the case of derivations, it is their astronomical size, which makes them almost impossible to grasp.

Thus, the Propositional Calculus should be thought of as part of a general method for synthesizing artificial proof-like structures. It does not, however, have much flexibility or generality. It is intended only for use in connection with mathematical concepts-which are themselves quite rigid. As a rather interesting example of this, let us make a derivation in which a very peculiar string is taken as a premise in a fantasy:

∧
~P>.
At least its semi-interpretation is peculiar. The Propositional Calculus, however, does not think about semi-interpretations; it just manipulates strings typographically-and typographically, there is really nothing peculiar about this string.

Here is a fantasy with this string as its premise:

(1)

[

push

(2)

∧
~P>

premise

(3)

P

separation

(4)

~P

separation

(5)

[

push

(6)

~Q

premise

(7)

P

carry-over line 3

(8)

~~P

double-tilde

(9)

]

pop

(10)

<~Q
⊃
~~P>

fantasy

(11)

<~P
⊃
Q>

contrapositive

(12)

Q

detachment (Lines 4,11)

(13)

]

pop

(14)

<∧
~P >
⊃
Q>

fantasy

Now this theorem has a very strange semi-interpretation:

P
and not
P
together imply
Q

Since
Q
is interpretable by any statement, we can loosely take the theorem to say that

"From a contradiction, anything follows"! Thus, in systems based on the Propositional Calculus, contradictions cannot be contained; they infect the whole system like an instantaneous global cancer.

The Handling of Contradictions

This does not sound much like human thought. If you found a contradiction in your own thoughts, it's very unlikely that your whole mentality would break down. Instead, you would probably begin to question the beliefs or modes of reasoning which you felt had led to the contradictory thoughts. In other words, to the extent you could, you would step out of the systems inside you which you felt were responsible for the contradiction, and try to repair them. One of the least likely things for you to do would be to throw up your arms and cry, "Well, I guess that shows that I believe everything now!" As a joke, yes-but not seriously.

Indeed, contradiction is a major source of clarification and progress in all domains of life-and mathematics is no exception. When in times past, a

contradiction in mathematics was found, mathematicians would immediately seek to pinpoint the system responsible for it, to jump out of it, to reason about it, and to amend it. Rather than weakening mathematics, the discovery and repair of a contradiction would strengthen it. This might take time and a number of false starts, but in the end it would yield fruit. For instance, in the Middle Ages, the value of the infinite series 1 – 1 + 1 – 1 + 1 -. ..