Typographical Number Theory (TNT)

Douglas Hofstadter introduces his "Typographical Number Theory" in Chapter VIII of his book "GÖDEL, ESCHER, BACH". I was surprised how little there was of this online, and how bad is what there is out there. The Wikipedia entry, https://en.wikipedia.org/wiki/Typographical_Number_Theory, does not even list the axioms of TNT, and has erroneous extraneous restrictions for the Compounds. There is also a page which seems to be part of a professor's class at Loyola Marymount University and which is better, https://cs.lmu.edu/~ray/notes/tnt/, but it also has extraneous restrictions and is missing one of the rules, the Rule of Existence!

So I wanted to put out some TNT derivations in a logical order and in a more complete way than in the book, ending with a version of the commutativity-of-addition derivation that I think is more logical than the one in the book.

First for some bookkeeping. Here are the axioms and the names of the rules of TNT with the abbreviations that I'll be using for them in the derivations:

• Axiom 1:    ∀a:∼Sa=0                        (A1)
• Axiom 2:    ∀a:(a+0)=a                      (A2)
• Axiom 3:    ∀a:∀b:(a+Sb)=S(a+b)    (A3)
• Axiom 4:    ∀a:(a∙0)=0                    (A4)
• Axiom 5:    ∀a:∀b:(a∙Sb)=((a∙b)+a)  (A5)
• Rule of Specification      (spec)
• Rule of Generalization   (gen)
• Rule of Interchange       (inter)
• Rule of Existence           (exist)
• Symmetry                       (sym)
• Transitivity                     (tran)
• Add S                              (addS)
• Drop S                            (dropS)
• Rule of Induction           (ind)

Rules from Propositional Calculus:

• Joining Rule               (join)
• Separation Rule          (sep)
• Double-tilde Rule       (doub)
• Fantasy Rule               (fant)
• Carry-over Rule         (carry)
• Rule of Detachment   (detach)
• Contrapositive Rule   (contra)
• De Morgan's Rule      (demorg)
• Switcheroo Rule         (switch)

I see no reason for putting push and pop for fantasies on their own lines as Hofstadter does, so I combine push with premise and pop with conclusion. I also see no reason for using the carry-over rule except in the case a carry-over is needed verbatim as a conclusion. And the same for copying axioms into derivations.

The first significant derivation that Hofstadter gives is of identity -- all numbers are equal to themselves. But he gives it as an erroneous derivation and leaves it to the reader to correct, so here it is:

(1)  (a+0)=a   spec A2 a/a

(2)  a=(a+0)   sym (1)

(3)  a=a   tran (2,1)

(4)  ∀a:a=a   gen (3)

The next derivation he gives is the proof that zero is a left identity for addition, as a demonstration of the need for the Rule of Induction. (The axioms, namely A2, only give zero as a right identity.) Unfortunately, the derivation is spread out over his explanation of Induction, so here it is all together:

(5)  (0+0)=0   spec A2 0/a

(6)  ∀b:(0+Sb)=S(0+b)   spec A3 0/a

(7)  (0+Sa)=S(0+a)   spec (6) a/b

(8)    [ (0+a)=a   premise

(9)      S(0+a)=Sa   addS (8)

(10)     (0+Sa)=Sa ]   tran (7,9)

(11)  <(0+a)=a⊃(0+Sa)=Sa>   fant

(12)  ∀a:<(0+a)=a⊃(0+Sa)=Sa>   gen (11)

(13)  ∀a:(0+a)=a   ind (5,12)

Here, Hofstadter jumps right into the commutativity of addition proof, but there are some interesting theorems that he seems to skip over. Like, what about zero being a left null for multiplication? And one being the left and right identity for multiplication? Maybe those can be postponed until we try a commutativity-of-multiplication proof. But there's one that he uses in commutativity-of-addition that should probably stand alone -- "add one" being the same as the successor operator:

(14)  ∀b:(a+Sb)=S(a+b)   spec A3 a/a

(15)  (a+S0)=S(a+0)   spec (14) 0/b

(16)  S(a+0)=Sa   addS (1)

(17)  (a+S0)=Sa   tran (15,16)

(18)  ∀a:(a+S0)=Sa   gen (17)

 

And examining Hofstadter's commutativity proof, it looks like he may have "proved too much" in the process of getting to the result. I suspect his "lemma", line 28, is not needed, and that only a "left" version of Axiom 3 is needed instead. Let's see:

 

(19)  (Sa+0)=Sa   spec A2 Sa/a

(20)  Sa=S(a+0)   sym (16)

(21)  (Sa+0)=S(a+0)   tran (19,20)

(22)  ∀a:(Sa+0)=S(a+0)   gen (21)

(23)  (a+Sb)=S(a+b)   spec (14) b/b

(24)  S(a+b)=(a+Sb)   sym (23)

(25)  ∀b:(Sa+Sb)=S(Sa+b)   spec A3 Sa/a

(26)  (Sa+Sb)=S(Sa+b)   spec (25) b/b

(27)    [ ∀a:(Sa+b)=S(a+b)   premise

(28)      (Sa+b)=S(a+b)   spec (27) a/a

(29)      (Sa+b)=(a+Sb)   tran (28,24)

(30)      S(Sa+b)=S(a+Sb)   addS (29)

(31)      (Sa+Sb)=S(a+Sb)   tran (26,30)

(32)      ∀a:(Sa+Sb)=S(a+Sb) ]   gen (31)

(33)  <∀a:(Sa+b)=S(a+b)⊃∀a:(Sa+Sb)=S(a+Sb)>   fant

(34)  ∀b:<∀a:(Sa+b)=S(a+b)⊃∀a:(Sa+Sb)=S(a+Sb)>   gen (33)

(35)  ∀b:∀a:(Sa+b)=S(a+b)   ind (22,34)

 

So let's see if these last three results are enough to give a simpler proof of commutativity of addition. As you can see above, I prefer to prove the base case of an induction first, opposite of Hofstadter. So my version will start at something like Hofstadter's line (50), and then continue at something like Hofstadter's line (29). I was also going to try to introduce only a single additional variable, c. But unless I want to take 4 lines just to reverse the quantification order on (35), it looks like I have to go with Hofstadter's two, c and d. I have put Hofstadter's line numbers as the last column, where there are matches, for comparison.

(36)  (c+0)=c   spec A2 c/a   (H50)

(37)  (0+c)=c   spec (13) c/a   (H52)

(38)  c=(0+c)   sym (37)   (H53)

(39)  (c+0)=(0+c)   tran (36,38)   (H54)

(40)  ∀c:(c+0)=(0+c)   gen (39)   (H55)

(41)  ∀b:(c+Sb)=S(c+b)   spec A3 c/a   (H29)

(42)  (c+Sd)=S(c+d)   spec (41) d/b   (H30,H40)

(43)  ∀a:(Sa+c)=S(a+c)   spec (35) c/b

(44)  (Sd+c)=S(d+c)   spec (43) d/a

(45)  S(d+c)=(Sd+c)   sym (44)

(46)    [ ∀c:(c+d)=(d+c)   premise   (H37)

(47)      (c+d)=(d+c)   spec (46) c/c   (H38)

(48)      S(c+d)=S(d+c)   addS (47)   (H39)

(49)      (c+Sd)=S(d+c)   tran (42,48)   (H41) 

(50)      (c+Sd)=(Sd+c)   tran (49,45)   (H45)

(51)      ∀c:(c+Sd)=(Sd+c) ]   gen (50)   (H46)

(52)  <∀c:(c+d)=(d+c)⊃∀c:(c+Sd)=(Sd+c)>   fant   (H48)

(53)  ∀d:<∀c:(c+d)=(d+c)⊃∀c:(c+Sd)=(Sd+c)>   gen (52)   (H49)

(54)  ∀d:∀c:(c+d)=(d+c)   ind (40,53)   (H56)

So yes, this appears to be a more efficient way to do it. Now we can use this to prove Hofstadter's lemma instead of the other way around, in just a few steps:

(55)  ∀b:(d+Sb)=S(d+b)   spec A3 d/a

(56)  (d+Sc)=S(d+c)   spec (55) c/b

(57)  (d+Sc)=(Sd+c)   tran (56,45)

(58)  ∀d:(d+Sc)=(Sd+c)   gen (57)

(59)  ∀c:∀d:(d+Sc)=(Sd+c)   gen (58)

 

Alright, now that I'm on a roll, let's do the three additional proofs mentioned above for multiplication, and then try commutativity of multiplication. Up first, zero as a left null for multiplication (the axioms, namely A4, only have it as a right null):

(60)  (0∙0)=0   spec A4 0/a

(61)  ∀b:(0∙Sb)=((0∙b)+0)   spec A5 0/a

(62)  (0∙Sa)=((0∙a)+0)   spec (61) a/b

(63)  ((0∙a)+0)=(0∙a)   spec A2 (0∙a)/a

(64)  (0∙Sa)=(0∙a)   tran (62,63)

(65)    [ (0∙a)=0   premise

(66)      (0∙Sa)=0 ]   tran (64,65)

(67)  <(0∙a)=0⊃(0∙Sa)=0>   fant 

(68)  ∀a:<(0∙a)=0⊃(0∙Sa)=0>   gen (67)

(69)  ∀a:(0∙a)=0   ind (60,68)

Well, that was relatively easy. Next up, one as a (right) identity for multiplication. It appears that I'll need another lemma first -- our first algebraic theorem, adding the same thing to both sides of an equation, and our first theorem with three variables:

(70)  (d+0)=d   spec A2 d/a

(71)  d=(d+0)   sym (70)

(72)  (c+Se)=S(c+e)   spec (41)  e/b

(73)  (d+Se)=S(d+e)   spec (55) e/b

(74)  S(d+e)=(d+Se)   sym (73)

(75)    [ c=d   premise

(76)      (c+0)=d   tran (36,75)

(77)      (c+0)=(d+0)   tran (76,71)

(78)      [ (c+e)=(d+e)   premise

(79)        S(c+e)=S(d+e)   addS (78)

(80)        (c+Se)=S(d+e)   tran (72,79)

(81)         (c+Se)=(d+Se) ]   tran (80,74)

(82)     <(c+e)=(d+e)⊃(c+Se)=(d+Se)>   fant

(83)     ∀e:<(c+e)=(d+e)⊃(c+Se)=(d+Se)>   gen (82)

(84)     ∀e:(c+e)=(d+e) ]   ind (77,83)

(85)  <c=d⊃∀e:(c+e)=(d+e)>   fant

(86)  ∀d:<c=d⊃∀e:(c+e)=(d+e)>   gen (85)

(87)  ∀c:∀d:<c=d⊃∀e:(c+e)=(d+e)>   gen (86)

Ok let's see if that is enough to prove that one is a right identity for multiplication:

(88)  ∀b:(a∙Sb)=((a∙b)+a)   spec A5 a/a

(89)  (a∙S0)=((a∙0)+a)   spec (88) 0/b

(90)  (a∙0)=0   spec A4 a/a

(91)  ∀d:<(a∙0)=d⊃∀e:((a∙0)+e)=(d+e)>   spec (87) (a∙0)/c

(92)  <(a∙0)=0⊃∀e:((a∙0)+e)=(0+e)>   spec (91) 0/d

(93)  ∀e:((a∙0)+e)=(0+e)   detach (90,92)

(94)  ((a∙0)+a)=(0+a)   spec (93) a/e

(95)  (a∙S0)=(0+a)   tran (89,94)

(96)  (0+a)=a   spec (13) a/a

(97)  (a∙S0)=a   tran (95,96)

(98)  ∀a:(a∙S0)=a   gen (97)

Next up, prove that one is also a left identity for multiplication:

(99)  (S0∙0)=0   spec A4 S0/a

(100)  ∀b:(S0∙Sb)=((S0∙b)+S0)   spec A5 S0/a 

(101)  (S0∙Sa)=((S0∙a)+S0)   spec (100) a/b

(102)  ((S0∙a)+S0)=S(S0∙a)   spec (18) (S0∙a)/a

(103)  (S0∙Sa)=S(S0∙a)   tran (101,102)

(104)    [ (S0∙a)=a   premise

(105)      S(S0∙a)=Sa   addS (104)

(106)      (S0∙Sa)=Sa ]   tran (103,105)

(107)  <(S0∙a)=a⊃(S0∙Sa)=Sa>   fant

(108)  ∀a:<(S0∙a)=a⊃(S0∙Sa)=Sa>   gen (107)

(109)  ∀a:(S0∙a)=a   ind (99,108)

Not too hard. Next up, commutativity of multiplication. After fiddling with it, it looks like it's going to need associativity of addition proved first. And after looking at that, it looks like it may need a "left" version of (87) proved first to avoid a lot of extra applications of (54). So:

(110)  ∀c:(c+a)=(a+c)   spec (54) a/d

(111)  (e+a)=(a+e)   spec (110) e/c

(112)  ∀c:(c+e)=(e+c)   spec (54) e/d

(113)  (b+e)=(e+b)   spec (112) b/c

(114)  ∀d:<a=d⊃∀e:(a+e)=(d+e)>   spec (87) a/c

(115)  <a=b⊃∀e:(a+e)=(b+e)>   spec (114) b/d

(116)    [ a=b   premise

(117)      ∀e:(a+e)=(b+e)   detach (116,115)

(118)      (a+e)=(b+e)   spec (117) e/e

(119)      (e+a)=(b+e)   tran (111,118)

(120)      (e+a)=(e+b)   tran (119,113)

(121)      ∀e:(e+a)=(e+b) ]   gen (120)

(122)  <a=b⊃∀e:(e+a)=(e+b)>   fant

(123)  ∀b:<a=b⊃∀e:(e+a)=(e+b)>   gen (122)

(124)  ∀a:∀b:<a=b⊃∀e:(e+a)=(e+b)>   gen (123)

 

Associativity of addition:

(125)  ((f+g)+0)=(f+g)   spec A2 (f+g)/a

(126)  (g+0)=g   spec A2 g/a

(127)  ∀b:<(g+0)=b⊃∀e:(e+(g+0))=(e+b)>   spec (124) (g+0)/a

(128)  <(g+0)=g⊃∀e:(e+(g+0))=(e+g)>   spec (127) g/b

(129)  ∀e:(e+(g+0))=(e+g)   detach (126,128)

(130)  (f+(g+0))=(f+g)   spec (129) f/e

(131)  (f+g)=(f+(g+0))   sym (130)

(132)  ((f+g)+0)=(f+(g+0))   tran (125,131)

(133)  ∀b:((f+g)+Sb)=S((f+g)+b)   spec A3 (f+g)/a

(134)  ((f+g)+Sh)=S((f+g)+h)   spec (133) h/b

(135)  ∀b:(f+Sb)=S(f+b)   spec A3 f/a

(136)  (f+S(g+h))=S(f+(g+h))   spec (135) (g+h)/b

(137)  S(f+(g+h))=(f+S(g+h))   sym (136)

(138)  ∀b:(g+Sb)=S(g+b)   spec A3 g/a

(139)  (g+Sh)=S(g+h)   spec (138) h/b

(140)  S(g+h)=(g+Sh)   sym (139)

(141)  ∀b:<S(g+h)=b⊃∀e:(e+S(g+h))=(e+b)>   spec (124) S(g+h)/a

(142)  <S(g+h)=(g+Sh)⊃∀e:(e+S(g+h))=(e+(g+Sh))>   spec (141) (g+Sh)/b

(143)  ∀e:(e+S(g+h))=(e+(g+Sh))   detach (140,142)

(144)  (f+S(g+h))=(f+(g+Sh))   spec (143) f/e

(145)  S(f+(g+h))=(f+(g+Sh))   tran (137,144)

(146)    [ ((f+g)+h)=(f+(g+h))   premise

(147)      S((f+g)+h)=S(f+(g+h))   addS (146)

(148)      ((f+g)+Sh)=S(f+(g+h))   tran (134,147)

(149)      ((f+g)+Sh)=(f+(g+Sh)) ]   tran (148,145)

(150)  <((f+g)+h)=(f+(g+h))⊃((f+g)+Sh)=(f+(g+Sh))>   fant

(151)  ∀h:<((f+g)+h)=(f+(g+h))⊃((f+g)+Sh)=(f+(g+Sh))>   gen (150)

(152)  ∀h:((f+g)+h)=(f+(g+h))   ind (132,151)

(153)  ∀g:∀h:((f+g)+h)=(f+(g+h))   gen (152)

(154)  ∀f:∀g:∀h:((f+g)+h)=(f+(g+h))   gen (153)

 

Phew, not a particularly easy one. I wonder if there is an easier way to do it. And finally, it appears we need a "left" version of  Axiom 5 as well -- ∀a:∀b:(Sa∙b)=((a∙b)+b). First, another little helper theorem:

(155)  ∀c:(c+a)=(a+c)   spec (54) a/d

(156)  (b+a)=(a+b)   spec (155) b/c

(157)  S(b+a)=S(a+b)   addS (156)

(158)  (c+Sa)=S(c+a)   spec (41) a/b

(159)  ∀c:(c+Sa)=S(c+a)   gen (158)

(160)  (b+Sa)=S(b+a)   spec (159) b/c

(161)  (b+Sa)=S(a+b)   tran (160,157)

(162)  (b+Sa)=(a+Sb)   tran (161,24)

Now the main proof:

(163)  (Sa∙0)=0   spec A4 Sa/a

(164)  ((a∙0)+0)=(a∙0)   spec A2 (a∙0)/a

(165)  ((a∙0)+0)=0   tran (164,90)

(166)  0=((a∙0)+0)   sym (165)

(167)  (Sa∙0)=((a∙0)+0)   tran (163,166)

(168)  ∀a:(Sa∙0)=((a∙0)+0)   gen (167)

(169)  ∀b:(Sa∙Sb)=((Sa∙b)+Sa)   spec A5 Sa/a

(170)  (Sa∙Sb)=((Sa∙b)+Sa)   spec (169) b/b

(171)  (a∙Sb)=((a∙b)+a)   spec (88) b/b

(172)    [ ∀a:(Sa∙b)=((a∙b)+b)   premise

(173)      (Sa∙b)=((a∙b)+b)   spec (172) a/a

(174)      ∀d:<(Sa∙b)=d⊃∀e:((Sa∙b)+e)=(d+e)>   spec (87) (Sa∙b)/c

(175)      <(Sa∙b)=((a∙b)+b)⊃∀e:((Sa∙b)+e)=(((a∙b)+b)+e)>   spec (174) ((a∙b)+b)/d

(176)      ∀e:((Sa∙b)+e)=(((a∙b)+b)+e)   detach (173,175)

(177)      ((Sa∙b)+Sa)=(((a∙b)+b)+Sa)   spec (176) Sa/e

(178)      (Sa∙Sb)=(((a∙b)+b)+Sa)   tran (170,177)

(179)      ∀g:∀h:(((a∙b)+g)+h)=((a∙b)+(g+h))   spec (154) (a∙b)/f

(180)      ∀h:(((a∙b)+b)+h)=((a∙b)+(b+h))   spec (179) b/g

(181)      (((a∙b)+b)+Sa)=((a∙b)+(b+Sa))   spec (180) Sa/h

(182)      (Sa∙Sb)=((a∙b)+(b+Sa))   tran (178,181)

(183)      ∀b:<c=b⊃∀e:(e+c)=(e+b)>   spec (124) c/a

(184)      <c=(a+Sb)⊃∀e:(e+c)=(e+(a+Sb))>   spec (183) (a+Sb)/b

(185)      ∀c:<c=(a+Sb)⊃∀e:(e+c)=(e+(a+Sb))>   gen (184)
(186)      <(b+Sa)=(a+Sb)⊃∀e:(e+(b+Sa))=(e+(a+Sb))>   spec (185) (b+Sa)/c

(187)      ∀e:(e+(b+Sa))=(e+(a+Sb))   detach (162,186)

(188)      ((a∙b)+(b+Sa))=((a∙b)+(a+Sb))   spec (187) (a∙b)/e

(189)      (Sa∙Sb)=((a∙b)+(a+Sb))   tran (182,188)

(190)      ∀h:(((a∙b)+a)+h)=((a∙b)+(a+h))   spec (179) a/g

(191)      (((a∙b)+a)+Sb)=((a∙b)+(a+Sb))   spec (190) Sb/h

(192)      ((a∙b)+(a+Sb))=(((a∙b)+a)+Sb)   sym (191)

(193)      (Sa∙Sb)=(((a∙b)+a)+Sb)   tran (189,192)

(194)      ∀d:<(a∙Sb)=d⊃∀e:((a∙Sb)+e)=(d+e)>   spec (87) (a∙Sb)/c

(195)      <(a∙Sb)=((a∙b)+a)⊃∀e:((a∙Sb)+e)=(((a∙b)+a)+e)>   spec (194) ((a∙b)+a)/d

(196)      ∀e:((a∙Sb)+e)=(((a∙b)+a)+e)   detach (171,195)

(197)      ((a∙Sb)+Sb)=(((a∙b)+a)+Sb)   spec (196) Sb/e

(198)      (((a∙b)+a)+Sb)=((a∙Sb)+Sb)   sym (197)

(199)      (Sa∙Sb)=((a∙Sb)+Sb)   tran (192,198)

(200)      ∀a:(Sa∙Sb)=((a∙Sb)+Sb) ]   gen (199)

(201)  <∀a:(Sa∙b)=((a∙b)+b)⊃∀a:(Sa∙Sb)=((a∙Sb)+Sb)>   fant

(202)  ∀b:<∀a:(Sa∙b)=((a∙b)+b)⊃∀a:(Sa∙Sb)=((a∙Sb)+Sb)>   gen (201)

(203)  ∀b:∀a:(Sa∙b)=((a∙b)+b)   ind (168,202)

 

Finally, are we ready for commutativity of multiplication after all that? Let's see:

(204)  (0∙a)=0   spec (69) a/a

(205)  0=(0∙a)   sym (204)

(206)  (a∙0)=(0∙a)   tran (90,205)

(207)  ∀a:(a∙0)=(0∙a)   gen (206)

(208)    [ ∀a:(a∙b)=(b∙a)   premise

(209)      (a∙b)=(b∙a)   spec (208) a/a

(210)      ∀d:<(a∙b)=d⊃∀e:((a∙b)+e)=(d+e)>   spec (87) (a∙b)/c

(211)      <(a∙b)=(b∙a)⊃∀e:((a∙b)+e)=((b∙a)+e)>   spec (210) (b∙a)/d

(212)      ∀e:((a∙b)+e)=((b∙a)+e)   detach (209,211)

(213)      ((a∙b)+a)=((b∙a)+a)   spec (212) a/e

(214)      (a∙Sb)=((b∙a)+a)   tran (171,213)

(215)      ∀a:(Sa∙c)=((a∙c)+c)   spec (203) c/b

(216)      (Sb∙c)=((b∙c)+c)   spec (215) b/a

(217)      ∀c:(Sb∙c)=((b∙c)+c)   gen (216)

(218)      (Sb∙a)=((b∙a)+a)   spec (217) a/c
(219)      ((b∙a)+a)=(Sb∙a)   sym (218)

(220)      (a∙Sb)=(Sb∙a)   tran (214,219)

(221)      ∀a:(a∙Sb)=(Sb∙a) ]   gen (220)

(222)  <∀a:(a∙b)=(b∙a)⊃∀a:(a∙Sb)=(Sb∙a)>   fant

(223)  ∀b:<∀a:(a∙b)=(b∙a)⊃∀a:(a∙Sb)=(Sb∙a)>   gen (222)

(224)  ∀b:∀a:(a∙b)=(b∙a)   ind (207,223)

Voila! It seems the bulk of the work was done in the prior proofs.

Some additional proofs I'd like to do: multiplying both sides of an equation, subtracting both sides of an equation, dividing both sides of an equation. That'll be another post...