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

Va:-Sa=O

3b:Va:-Sa=b

aXiom

existence

You might now try to shunt symbols, according to rules so far given, to

produce the theorem -Vb:3a:Sa=b.

Rules of Equality and Successorship

We have given rules for manipulating quantifiers, but so far none for the

symbols '=' and'S'. We rectify that situation now. In what follows, r, 5, and

t all stand for arbitrary terms.

RULES OF EQUALITY:

SYMMETRY: If r = 5 is a theorem, then so is 5 = r.

TRANSITIVITY: If r = 5 and 5 = t are theorems, then so is r = t.

RULES OF SUCCESSORSHIP:

ADD S: If r = t is a theorem, then Sr = St is a theorem.

DROP S: If Sr = St is a theorem, then r = t is a theorem.

Now we are equipped with rules that can give us a fantastic variety of

theorems. For example, the following derivations yield theorems which are

pretty fundamental:

(1) Va:Vb:(a+Sb)=S(a+b)

(2) Vb:(SO+Sb)=S(SO+b)

(3) (SO+SO)=S(SO+O)

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

(5) (SO+O)=SO

(6) S(SO+O)=SSO

(7) (SO+SO)=SSO

axiom 3

specification (SO for a)

specification (0 for b)

axiom 2

specification (SO for a)

add S

transitivity (lines 3,6)

* * * * *

(1) Va:Vb:(a'Sb)=((a'b)+a)

(2) Vb:(SO'Sb)=((SO'b)+SO)

(3) (SO·SO)=((SO·O)+SO)

(4) Va:Vb:(a+Sb)=S(a+b)

(5) Vb:((SO'O)+Sb)=S((SO'O)+b)

(6) ((SO' O)+SO)=S((SO· 0) +0)

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

(8) ((SO·O)+O)=(SO·O)

(9) Va:(a'O)==O

(10) (SO'O)=O

(11) ((SO'O)+O)=O

(12) S((SO'O)+O)=SO

(13) ((SO'O)+SO)=SO

(14) (SO'SO)==SO

Typographical Number Theory

axiom 5

specification (SO for a)

specification (0 for b)

axiom 3

specification ((SO' 0) for a)

specification (0 for b)

axiom 2

specification ((SO.O) for a)

axiom 4

specification (SO for a)

transitivity (lines 8,10)

add S

transitivity (lines 6,12)

transitivity (lines 3,13)

219