Read Gödel, Escher, Bach: An Eternal Golden Braid Online
Authors: Douglas R. Hofstadter
Tags: #Computers, #Art, #Classical, #Symmetry, #Bach; Johann Sebastian, #Individual Artists, #Science, #Science & Technology, #Philosophy, #General, #Metamathematics, #Intelligence (AI) & Semantics, #G'odel; Kurt, #Music, #Logic, #Biography & Autobiography, #Mathematics, #Genres & Styles, #Artificial Intelligence, #Escher; M. C
Well-Formed Strings
There will be several other rules of inference, and they will all be pres shortly-but first, it is important to define a subset of all strings, namely the
well formed
strings. They will be defined in a recursive way. We begin with the ATOMS:
P, Q,
and
R
are called atoms.. New atoms are formed by appending primes onto the right of old atoms-thus,
R', Q", P
"', etc. This gives an endless supply of atoms.
All atoms are well-formed.
Then we have four recursive
FORMATION RULES: If x and y are well-formed, then the following four strings are also well-formed:
(1)
~x
(2)
< x∧y>
(3)
< x∨y>
(4)
< x⊃y>
For example, all of the following are well-formed:
P
atom
~P
by (1)
~~P
by (1)
Q´
atom
~Q1
by (1)
∧
by (2)
~
∧by (1)
~~
⊃by (4)
<~
∧The last one may look quite formidable, but it is built up straightforwardly from two components-namely the two lines just above it. Each of them is in turn built up from previous lines ... and so on. Every well-formed string can in this way be traced back to its elementary constituents-that is, atoms. You simply run the formation rules backwards until you can no more. This process is guaranteed to terminate, since each formation rule (when run forwards) is a
lengthening
rule, so that running it backwards always drives you towards atoms.
This method of decomposing strings thus serves as a check on the wellformedness of any string. It is a
top-down decision procedure
for wellformedness. You can test your understanding of this decision procedure by checking which of the following strings are well-formed:
(1)
(2) (2) <~P>
(3)
∧(4)
∧(5) <
∧(6)
∧(7) <
∨(Answer: Those whose numbers are Fibonacci numbers are not formed. The rest are wellformed.)
More Rules of Inference
Now we come to the rest of the rules by which theorems of this system constructed. A few rules of inference follow. In all of them, the symbols ´xánd 'y' are always to be understood as restricted to
well formed
strings
RULE OF SEPARATION: If < x∧y> is a theorem, then both x and theorems.
Incidentally, you should have a pretty good guess by now as to concept the symbol À'
stands for. (Hint: it is the troublesome word the preceding Dialogue.) From the following rule, you should be a figure out what concept the
tilde
('~') represents: DOUBLE-TILDE RULE: The string '~~' can be deleted from any theorem. It can also be inserted into any theorem, provided that the rest string is itself well-formed.
The Fantasy Rule
Now a special feature of this system is that it has
no axioms
-only rule you think back to the previous formal systems we've seen, you may w( how there can be any theorems, then. How does everything get started? The answer is that there is one rule which manufactures theorems from out of thin air-it doesn't need an "old theorem" as input.
(The rest of the do require input.) This special rule is called the
fantasy rule
. The reason I call it that is quite simple.
To use the fantasy rule, the first thing you do is to write down an well-formed string x you like, and then "fantasize" by asking, "
What if
string x were an axiom, or a theorem?" And then, you let the system give an answer. That is, you go ahead and make a derivation with x ; opening line; let us suppose y is the last line. (Of course the derivation must strictly follow the rules of the system.) Everything from x to y (inclusive) is the
fantasy
; x is the
premise
of the fantasy, and y is its
outcome
. The next step is to jump out of the fantasy, having learned from it that out.
If x were a theorem, y would be a theorem.
Still, you might wonder, where is the
real
theorem? The real theorem is the string
Notice the resemblance of this string to the sentence printed above To signal the entry into, and emergence from, a fantasy, one uses the square brackets `[' and ']', respectively. Thus, whenever you see a left square bracket, you know you are "pushing" into a fantasy, and the
next
line will contain the fantasy's
premise
. Whenever you see a right square bracket, you know you are "popping" back out, and the
preceding
line was the outcome. It is helpful (though not necessary) to indent those lines of a derivation which take place in fantasies.
Here is an illustration of the fantasy rule, in which the string P is taken as a premise. (It so happens that P is not a theorem, but that is of no import; we are merely inquiring, "What if it were?") We make the following fantasy:
[
push into fantasy
P
premise
~~~P
outcome (by double tilde rule)
]
pop out of fantasy
The fantasy shows that:
If
P
were a theorem, so would
~~P
be one.
We now "squeeze" this sentence of English (the metalanguage) into the formal notation (the object language):
. This, our first theorem of the Propositional Calculus, should reveal to you the intended interpretation of the symbol `⊃'.
Here is another derivation using the fantasy rule:
[
push
∧
premise
P
separation
Q
separation
∧
P>
joining
]
pop
<
∧fantasy rule
It is important to understand that only the last line is a genuine theorem, here-everything else is in the fantasy.
Recursion and the Fantasy Rule
As you might guess from the recursion terminology "push" and "pop", the fantasy rule can be used recursively-thus, there can be fantasies within fantasies, thrice-nested fantasies, and so on. This means that there are all sorts of "levels of reality", just as in nested stories or movies. When you pop out of a movie-within-a-movie, you feel for a moment as if you had reached the real world, though you are still one level away from the top. Similarly, when you pop out of a fantasy-within-a-fantasy, you are in a "realer"
world than you had been, but you are still one level away from the top.
Now a "No Smoking" sign inside a movie theater does not apply to the characters in the movie-there is no carry-over from the real world in fantasy world, in movies. But in the Propositional Calculus, then carry-over from the real world into the fantasies; there is even carry from a fantasy to fantasies inside it. This is formalized by the following rule:
CARRY-OVER RULE: Inside a fantasy, any theorem from the "reality level higher can be brought in and used.
It is as if a "No Smoking" sign in a theater applied not only to a moviegoers, but also to all the actors in the movie, and, by repetition of the same idea, to anyone inside multiply nested movies! (Warning: There carry-over in the reverse direction: theorems inside fantasies cannot be exported to the exterior! If it weren't for this fact, you could write any as the first line of a fantasy, and then lift it out into the real world as a theorem.) To show how carry-over works, and to show how the fantasy rule can be used recursively, we present the following derivation:
[
push
P
premise of outer fantasy
[
push again
Q
premise of inner fantasy
P
carry-over of P into inner fantasy
∧
joining
]
pop out of inner fantasy, regain outer fantasy
⊃
fantasy rule
]
pop out of outer fantasy, reach real world!
⊃
fantasy rule
Note that I've indented the outer fantasy once, and the inner fantasy twice, to emphasize the nature of these nested "levels of reality". One to look at the fantasy rule is to say that an observation made
about
the system is inserted
into
the system. Namely, the theorem < x⊃y> which gets produced can be thought of as a representation inside the system of the statement about the system "If x is a theorem, then y is too". To be specific, the intended interpretation for
The Converse of the Fantasy Rule
Now Lewis Carroll's Dialogue was all about "if-then" statements. In particular, Achilles had a lot of trouble in persuading the Tortoise to accept the second clause of an "if-then"
statement, even when the "if-then" state itself was accepted, as well as its first clause. The next rule allows y infer the second "clause" of a'⊃'-string, provided that thè⊃'-string it a theorem, and that its first "clause" is also a theorem.
RULE OF DETACHMENT: If x and < x⊃y> are both theorems, then y is a theorem.
Incidentally, this rule is often called "Modus Ponens", and the fantasy rule is often called the "Deduction Theorem".
The Intended Interpretation of the Symbols
We might as well let the cat out of the bag at this point, and reveal the "meanings" of the rest of the symbols of our new system. In case it is not yet apparent, the symbol À' is meant to be acting isomorphically to the normal, everyday word ànd'. The symbol '-'
represents the word 'not'-it is a formal sort of negation. The angle brackets '<' and `>' are groupers-their function being very similar to that of parentheses in ordinary algebra. The main difference is that in algebra, you have the freedom to insert parentheses or to leave them out, according to taste and style, whereas in a formal system, such anarchic freedom is not tolerated. The symbol '∨' represents the word òr' ('vel' is a Latin word for òr'). The òr' that is meant is the so-called
inclusive
òr', which means that the interpretation of
The only symbols we have not interpreted are the atoms. An atom has no single interpretation-it may be interpreted by any sentence of English (it must continue to be interpreted by the same sentence if it occurs multiply within a string or derivation). Thus, for example, the well-formed string <
P
∧~
P
> could be interpreted by the compound sentence
This mind is Buddha, and this mind is not Buddha.
Now let us look at each of the theorems so far derived, and interpret them. The first one was <
P
⊃
~~P
>. If we keep the same interpretation for
P
, we have the following interpretation:
If this mind is Buddha,
then it is not the case that this mind is not Buddha.
Note how I rendered the double negation. It is awkward to repeat a negation in any natural language, so one gets around it by using two different ways of expressing negation. The second theorem we derived was
<
If this mind is Buddha and this flax weighs three pounds,
then this flax weighs three pounds and this mind is Buddha.
The third theorem was <
P
⊃<
Q
⊃<
P
∧
Q
>>>. This one goes into the following nested "if-then" sentence:
If this mind is Buddha,
then, if this flax weighs three pounds,
then this mind is Buddha and this flax weighs three pounds.
You probably have noticed that each theorem, when interpreted, something absolutely trivial and self-evident. (Sometimes they are so s evident that they sound vacuous and-paradoxically enough-confusing or even wrong!) This may not be very impressive, but just remember there are plenty of falsities out there which could have been produced they weren't. This system-the Propositional Calculus-steps neatly ft truth to truth, carefully avoiding all falsities, just as a person who is concerned with staying dry will step carefully from one stepping-stone creek to the next, following the layout of stepping-stones no matter I twisted and tricky it might be. What is impressive is that-in the Propositional Calculus-the whole thing is done purely
typographically
. There is nobody down "in there", thinking about the
meaning
of the strings. It i! done mechanically, thoughtlessly, rigidly, even stupidly.