Typographical Number Theory #3

Following on from the previous posts in the series, now it's time to prove that subtracting from both sides of an equation and that multiplying both sides of an equation preserve equality -- more proofs in the algebra series. Also below I'll discuss the difficulty of proving that dividing both sides of an equation preserves equality and start on some helper proofs in that regard.

First, as before, a section in which I copy in any theorems from the previous posts that are used in this post's derivations:

 

[in progress]

Typographical Number Theory, continued, #2

See the previous post for background on Douglas Hofstadter's "Typographical Number Theory":

https://youngjeff2.blogspot.com/2024/01/typographical-number-theory-tnt.html

In this second post, I want to look at some derivations that seem like they should be simple but seemingly aren't, starting with: All numbers are either zero or the successor of another number. Sort of the complement to Axiom 1: zero is not the successor of any number, but all other numbers are.

First, a section in which I copy in any theorems from the previous post that are used in this post's derivations:

(2)  a=(a+0)

(3)  a=a  

(4)  ∀a:a=a

(14)  ∀b:(a+Sb)=S(a+b

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

(35)  ∀b:∀a:(Sa+b)=S(a+b)

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

(90)  (a∙0)=0

(156)  (b+a)=(a+b)

(224)  ∀b:∀a:(a∙b)=(b∙a)

To prove: ∀a:<∼a=0⊃∃b:a=Sb> and ∀a:<∃b:a=Sb⊃∼a=0>

I have only found derivations that make use of "vacuously true" fantasies, and I wonder if there are better ways.

(225)  0=0   spec (4) 0/a

(226)    [ ∼∃b:0=Sb   premise

(227)      0=0 ]   carry (225)

(228)  <∼∃b:0=Sb⊃0=0>   fant

(229)  <∼0=0⊃∼∼∃b:0=Sb>   contra (228)

(230)  <∼0=0⊃∃b:0=Sb>   doub (229)

(231)  Sa=Sa   addS (3)

(232)  ∃b:Sa=Sb   exist (231) b/a

(233)    [ <∼a=0⊃∃b:a=Sb>   premise

(234)      [ ∼Sa=0   premise

(235)        ∃b:Sa=Sb ]   carry (232)

(236)      <∼Sa=0⊃∃b:Sa=Sb> ]   fant

(237)  <<∼a=0⊃∃b:a=Sb>⊃<∼Sa=0⊃∃b:Sa=Sb>> ]   fant

(238)  ∀a:<<∼a=0⊃∃b:a=Sb>⊃<∼Sa=0⊃∃b:Sa=Sb>>   gen (237)

(239)  ∀a:<∼a=0⊃∃b:a=Sb>   ind (230,238)

 

To prove: ∀a:<∃b:a=Sb⊃∼a=0>

(240)    [ 0=Sb   premise

(241)      Sb=0 ]   sym (240)

(242)  <0=Sb⊃Sb=0>   fant

(243)  <∼Sb=0⊃∼0=Sb>   contra (242)

(244)  ∼Sb=0   spec A1 b/a

(245)  ∼0=Sb   detach (244,243)

(246)  ∀b:∼0=Sb   gen (245)

(247)  ∼∃b:0=Sb   inter (246)

(248)    [ 0=0   premise

(249)      ∼∃b:0=Sb ]   carry (247)

(250)  <0=0⊃∼∃b:0=Sb>   fant

(251)  <∼∼∃b:0=Sb⊃∼0=0>   contra (250)

(252)  <∃b:0=Sb⊃∼0=0>   doub (251)

(253)    [ ∃b:Sa=Sb   premise

(254)      ∼Sa=0 ]   spec A1 a/a

(255)  <∃b:Sa=Sb⊃∼Sa=0>   fant

(256)    [ <∃b:a=Sb⊃∼a=0>   premise

(257)      <∃b:Sa=Sb⊃∼Sa=0> ]   carry (255)

(258)  <<∃b:a=Sb⊃∼a=0>⊃<∃b:Sa=Sb⊃∼Sa=0>>   fant

(259)  ∀a:<<∃b:a=Sb⊃∼a=0>⊃<∃b:Sa=Sb⊃∼Sa=0>>   gen (258)

(260)  ∀a:<∃b:a=Sb⊃∼a=0>   ind (252,259)

 

Another proof that seems harder than it ought to be: ∀a:∀c:<(a+c)=0⊃a=0>

There seem to be two different ways to prove it, induction on a and induction on c.

 

But after doing both induction proofs, I realized that the first result above allows a shorter proof, without induction and without "vacuous" fantasies, for formulas where the expression is true for zero and for Sa outright, independent of its truth for a. In other words, because all numbers are either zero or a successor, (239) allows a "shortcut" version of induction to be used for such expressions.

I left the induction proofs in below with numbers prefixed with X, for comparison with the simpler proof, since I had already done the work.

To prove: ∀a:∀c:<(a+c)=0⊃a=0>

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

(262)  <a=Sb⊃∀e:(a+e)=(Sb+e)>   spec (261) Sb/d

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

(264)  (Sb+c)=S(b+c)   spec (263) b/a

(265)  ∼S(b+c)=0   spec A1 (b+c)/a

(266)  <∼a=0⊃∃b:a=Sb>   spec (239) a/a

(267)    [ ∼a=0   premise

(268)      ∃b:a=Sb   detach (267,266)

(269)      [ (a+c)=0   premise

(270)        [ a=Sb   premise

(271)          ∀e:(a+e)=(Sb+e)   detach (270,262)

(272)          (a+c)=(Sb+c)   spec (271) c/e

(273)          (a+c)=S(b+c)   tran (272,264)

(274)          S(b+c)=(a+c)   sym (273)

(275)          S(b+c)=0 ]   tran (274,269)

(276)        <a=Sb⊃S(b+c)=0>   fant

(277)        <∼S(b+c)=0⊃∼a=Sb>   contra (276)

(278)        ∼a=Sb   detach (265,277)

(279)        ∀b:∼a=Sb   gen (278)

(280)        ∼∃b:a=Sb ]   inter (279)

(281)      <(a+c)=0⊃∼∃b:a=Sb>   fant

(282)      <∼∼∃b:a=Sb⊃∼(a+c)=0>   contra (281)

(283)      <∃b:a=Sb⊃∼(a+c)=0>   doub (282)

(284)      ∼(a+c)=0 ]   detach (268,283)

(285)  <∼a=0⊃∼(a+c)=0>   fant

(286)  <(a+c)=0⊃a=0>   contra (285)

(287)  ∀c:<(a+c)=0⊃a=0>   gen (286)

(288)  ∀a:∀c:<(a+c)=0⊃a=0>   gen (287)

 

Huh, maybe not so simple. 28 steps (vs. 18 or 20 below), fantasy nested 3 deep, and reliance on 3 previous results. A fair price for avoiding induction and "meaningless" fantasies? Who knows. Here are the "direct" proofs:

 

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

(X262)      a=0 ]   tran (2,X261)

(X263)  <(a+0)=0⊃a=0>   fant

(X264)    [ (a+Sb)=0   premise

(X265)      S(a+b)=0 ]   tran (24,X264)

(X266)  <(a+Sb)=0⊃S(a+b)=0>   fant

(X267)  <∼S(a+b)=0⊃∼(a+Sb)=0>   contra (X266)

(X268)  ∼S(a+b)=0   spec A1 (a+b)/a

(X269)  ∼(a+Sb)=0   detach (X268,X267)

(X270)    [ ∼a=0   premise

(X271)      ∼(a+Sb)=0 ]   carry (X269)

(X272)  <∼a=0⊃∼(a+Sb)=0>   fant

(X273)  <(a+Sb)=0⊃a=0>   contra (X272)

(X274)    [ <(a+b)=0⊃a=0>   premise

(X275)      <(a+Sb)=0⊃a=0> ]   carry (X273)

(X276)  <<(a+b)=0⊃a=0>⊃<(a+Sb)=0⊃a=0>>   fant

(X277)  ∀b:<<(a+b)=0⊃a=0>⊃<(a+Sb)=0⊃a=0>>   gen (X276)

(X278)  ∀b:<(a+b)=0⊃a=0>   ind (X263,X277)

Via induction on a instead:

(X279)    [ (0+b)=0   premise

(X280)      0=0 ]   carry (225)

(X281)  <(0+b)=0⊃0=0>   fant

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

(X283)  (Sa+b)=S(a+b)   spec (X282) a/a

(X284)  S(a+b)=(Sa+b)   sym (X283)

(X285)    [ (Sa+b)=0   premise

(X286)      S(a+b)=0 ]   tran (X284,X285)

(X287)  <(Sa+b)=0⊃S(a+b)=0>   fant

(X288)  <∼S(a+b)=0⊃∼(Sa+b)=0>   contra (X266)

(X289)  ∼(Sa+b)=0   detach (X268,X288)

(X290)    [ ∼Sa=0   premise

(X291)      ∼(Sa+b)=0 ]   carry (X289)

(X292)  <∼Sa=0⊃∼(Sa+b)=0>   fant

(X293)  <(Sa+b)=0⊃Sa=0>   contra (X292)

(X294)    [ <(a+b)=0⊃a=0>   premise

(X295)      <(Sa+b)=0⊃Sa=0> ]   carry (X293)

(X296)  <<(a+b)=0⊃a=0>⊃<(Sa+b)=0⊃Sa=0>>   fant

(X297)  ∀a:<<(a+b)=0⊃a=0>⊃<(Sa+b)=0⊃Sa=0>>   gen (X296)

(X298)  ∀a:<(a+b)=0⊃a=0>   ind (X281,X297)

 

Now we should prove that (a+c)=0 also ⊃c=0. As above this can be done both in a "simple" way making use of commutativity of addition, or in a "direct" way using a variation of the "direct" proofs above. Let's compare:

To prove: ∀a:∀c:<(a+c)=0⊃c=0>

(289)  ∀c:<(b+c)=0⊃b=0>   spec (288) b/a

(290)  <(b+a)=0⊃b=0>   spec (289) a/c

(291)    [ (a+b)=0   premise

(292)      (b+a)=0   tran (156,291)

(293)      b=0 ]   detach (292,290)

(294)  <(a+b)=0⊃b=0>   fant

(295)  ∀b:<(a+b)=0⊃b=0>   gen (294)

(296)  <(a+c)=0⊃c=0>   spec (295) c/b

(297)  ∀c:<(a+c)=0⊃c=0>   gen (296)

(298)  ∀a:∀c:<(a+c)=0⊃c=0>   gen (297)

 

The "direct" version:

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

(X300)      0=0 ]   carry (225)

(X301)  <(a+0)=0⊃0=0>   fant

(X302)  (a+Sc)=S(a+c)   spec (14) c/b

(X303)  S(a+c)=(a+Sc)   sym (X302)

(X304)    [ (a+Sc)=0   premise

(X305)      S(a+c)=0 ]   tran (X303,X304)

(X306)  <(a+Sc)=0⊃S(a+c)=0>   fant

(X307)  <∼S(a+c)=0⊃∼(a+Sc)=0>   contra (X306)

(X308)  ∼S(a+c)=0   spec A1 (a+c)/a

(X309)  ∼(a+Sc)=0   detach (X308,X307)

(X310)    [ ∼Sc=0   premise

(X311)      ∼(a+Sc)=0 ]   carry (X309)

(X312)  <∼Sc=0⊃∼(a+Sc)=0>   fant

(X313)  <(a+Sc)=0⊃Sc=0>   contra (X312)

(X314)    [ <(a+c)=0⊃c=0>   premise

(X315)      <(a+Sc)=0⊃Sc=0> ]   carry (X313)

(X316)  <<(a+c)=0⊃c=0>⊃<(a+Sc)=0⊃Sc=0>>   fant

(X317)  ∀c:<<(a+c)=0⊃c=0>⊃<(a+Sc)=0⊃Sc=0>>   gen (X316)

(X318)  ∀c:<(a+c)=0⊃c=0>   ind (X301,X317)

(X319)  ∀a:∀c:<(a+c)=0⊃c=0>   gen (X318)

From the above, now it should be easy to prove this next theorem:

To prove: ∀a:∀b:<(a∙Sb)=0⊃a=0>

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

(300)  (a∙Sb)=((a∙b)+a)   spec (299) b/b

(301)  ((a∙b)+a)=(a∙Sb)   sym (300)

(302)  ∀c:<((a∙b)+c)=0⊃c=0>   spec (298) (a∙b)/a

(303)  <((a∙b)+a)=0⊃a=0>   spec (302) a/c

(304)    [ (a∙Sb)=0   premise

(305)      ((a∙b)+a)=0   tran (301,304)

(306)      a=0 ]   detach (305,303)

(307)  <(a∙Sb)=0⊃a=0>   fant

(308)  ∀b:<(a∙Sb)=0⊃a=0>   gen (307)

(309)  ∀a:∀b:<(a∙Sb)=0⊃a=0>   gen (308)

For completeness I suppose we should also prove the commuted version and a generalized version of the above:

(310)  ∀a:(a∙Sb)=(Sb∙a)   spec (224) Sb/b

(311)  (a∙Sb)=(Sb∙a)   spec (310) a/a

(312)    [ (Sb∙a)=0   premise

(313)      (a∙Sb)=0   tran (311,312)

(314)      a=0 ]   detach (313,307)

(315)  <(Sb∙a)=0⊃a=0>   fant

(316)  ∀b:<(Sb∙a)=0⊃a=0>   gen (315)

(317)  ∀a:∀b:<(Sb∙a)=0⊃a=0>   gen (315)

And  the generalized version without S:

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

(319)      [ ∼a=0   premise

(320)        0=0 ]   carry (225)

(321)      <∼a=0⊃0=0>   fant

(322)      <a=0 ⋁ 0=0> ]   switch (321)

(323)  <(a∙0)=0⊃<a=0 ⋁ 0=0>>   fant

(324)    [ <b=0⊃(a∙b)=0>   premise

 

(322)     [ ∼(a∙Sb)=0

(323)       ∼Sb=0 ]   carry (244)

(324)    <∼(a∙Sb)=0⊃∼Sb=0>   fant

(325)    <Sb=0⊃(a∙Sb)=0> ]   contra (324)

(326)  <<b=0⊃(a∙b)=0>⊃<Sb=0⊃(a∙Sb)=0>>   fant

(327)  ∀b:<<b=0⊃(a∙b)=0>⊃<Sb=0⊃(a∙Sb)=0>>   gen (326)

(328)  ∀b:<b=0⊃(a∙b)=0   ind (320,327)

Ignore the below. Construction in progress...

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