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

(26) (d+SO)=(Sd+O)

(27) Vd:(d+SO)=(Sd+O)

(28) Vc:Vd:(d+Sc)=(Sd+c)

transitivity

(lines 23,25)

generalization

induction

(lines 18,27)

[S can be slipped back and forth in an addition.]

(29) Vb:(c+Sb)=S(c+b)

(30) (c+Sd)=S(c+d)

(31) Vb:(d+Sb)=S(d+b)

(32) (d+Sc)=S(d+c)

(33) S(d+c)=(d+Sc)

(34) Vd:(d+Sc)=(Sd+c)

specification

(line 1)

specification

specification

(line 1)

specification

symmetry

specification

(line 28)

(35) (d+Sc)=(Sd+c) specification

(36) [ push

(37) Vc:(c+d)=(d+c) premise

(38) (c+d)=(d+c) specification

(39) S(c+d)=S(d+c) add S

(40) (c+Sd)=S(c+d) carryover 30

(41) (c+Sd)=S(d+c) transitivity

(42) S(d+c)=(d+Sc) carryover 33

(43) (c+Sd)=(d+Sc) transitivity

(44) (d+Sc)=(Sd+c) carryover 35

(45) (c +Sd) =(Sd +c) transitivity

(46) Vc:(c+Sd)=(Sd+c) generalization

(47) ] pop

(48) <Vc:(c+d)=(d+cPVc:(c+Sd)=(Sd+c» fantasy rule

(49) Vd:<Ve:(c+d)=(d+cPVc:(c+Sd)=(Sd+c» generalization

[If d commutes with every c, then Sd does too.]

(50) (c+O)=c

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

(52) (O+c)=c
(53) c=(O+c)

226

specification

(line 20)

previous

theorem

specification

symmetry

Typographical Number Theory