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

Illegal Shortcuts

Now here is an interesting question: "How can we make a derivation for the

string O=O?" It seems that the obvious route to go would be first to derive

the string Va:a=a, and then to use specification. So, what about the follow-

ing "derivation" of Va:a=a ... What is wrong with it? Can you fix it up?

(1) Va:(a+O)=a

(2) Va:a=(a+O)

(3) Va:a=a

axiom 2

symmetry

transiti vity (lines 2,1)

I gave this mini-exercise to point out one simple fact: that one should not
jump too fast in manipulating symbols (such as '=') which are familiar. One
must follow the rules, and not one's knowledge of the passive meanings of
the symbols. Of course, this latter type of knowledge is invaluable in
guiding the route of a derivation.

Why Specification and Generalization Are Restricted

Now let us see why there are restrictions necessary on both specification

and generalization. Here are two derivations. In each of them, one of the

restrictions is violated. Look at the disastrous results they produce:

(1) [

(2) a=O

(3) Va:a=O

(4) Sa=O

(5) ]

(6) <a=O~Sa=O>

(7) Va:<a=O~Sa=O>

(8) <O=O~SO=O>

(9) 0=0

(0) SO=O

push

premise

generalization (Wrong!)

specification

pop

fantasy rule

generalization

specification

previous theorem

detachment (lines 9,8)

This is the first disaster. The other one is via faulty specification.

(1) Va:a=a

(2) Sa=Sa

(3) 3b:b=Sa

(4) Va:3b:b=Sa

(5) 3b:b=Sb

previous theorem

specification

existence

generalization

specification (Wrong!)

So now you can see why those restrictions are needed.

Here is a simple puzzle: translate (if you have not already done so)

Peano's fourth postulate into TNT-notation, and then derive that string as

a theorem.

(^220) Typographical Number Theory