Gödel, Escher, Bach An Eternal Golden Braid by Douglas R. Hofstadter

characters in the movie-there is no carry-over from the real world into the

fantasy world, in movies. But in the Propositional Calculus, there is a

carry-over from the real world into the fantasies; there is even carry-over

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" one

level higher can be brought in and used.

It is as if a "No Smoking" sign in a theater applied not only to all the

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 is no

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 anything

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:

[

]

P

[

]

Q

P

<PAQ>

<Q:::><PAQ>>

<P:::><Q:::><PAQ»>

push

premise of outer fantasy

push again

premise of inner fantasy

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 way

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 more

specific, the intended interpretation for <P:::>Q> is "if P, then Q", or

equivalently, "P implies Q".

The Converse of the Fantasy Rule

Now Lewis Carroll's Dialogue was all about "if-then" statements. In particu-

lar, 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" statement

itself was accepted, as well as its first clause. The next rule allows you to

infer the second "clause" of a ':::>'-string, provided that the ':::>' -string itself is

a theorem, and that its first "clause" is also a theorem.

The Propositional Calculus 185