Vtgyjfy

The following is from Fundamentals of Mathematics, Volume 1 Foundations
of Mathematics: The Real Number System and Algebra, Edited by H. Behnke, F. Bachmann, K. Fladt, W. Süss and H. Kunle.

It's part of the development of the theory of natural numbers. Their
version of Peano's axioms begins with 1, not 0. My question pertains to the proof of rule (15).

If for the numbers $a,b$ there exists a number $c$ with $a+c=b,$
we write $a<b$ ($a$ is less than $b$), or alternatively $b>a$
($b$ is greater than $a$). For the relation $<$ defined in this
way we have the following theorems:

(12) if $a<b,$ then $ane b$ (antireflexivity);

(13) if $a<b$ and $b<c,$ then $a<c$ (transitivity);

(14) if $a<b,$ then $left(a+dright)<left(b+dright)$(monotonicity
of addition);

(15) if $ane b,$ then $a<b$ or $b<a.$

Rule (12), which states that $a+cne a$ for all $a,c,$ is proved
by complete induction on $a,$ for we have $1+cne1$ by (1) [$a+1=a^{prime}$],
(7) [$a+b=b+a$] and axiom IV [$a^{prime}ne1$ for every number
$a$]; and if we had $a^{prime}+c=a^{prime},$ it would follow
that $left(a+cright)^{prime}=a^{prime},$ and thus $a+c=a.$ For
the proof of (13), (14) we set $a+u=b,b+v=c$ and thus get

$c=left(a+uright)+v=a+left(u+vright),$

$b+d=left(a+uright)+d=a+left(u+dright)=left(a+dright)+u.$

Complete induction on $a$ is again used to prove (15), as follows.

The case $a=1$ is first dealt with by complete induction on $b:$
[footnote: In this case the induction hypothesis is not used at
all, a fact which may make the proof somewhat harder to follow.]

$1=1;$

$1<1+b=b+1=b^{prime}.$

Then from (15) (for all $b$) the same statement with $a^{prime}$instead
of $a$ (thus for all $b:$ $a^{prime}<b$ or $a^{prime}=b$ or
$b<a^{prime}$) is derived by complete induction on $b:$

$1<a^{prime};$

$a^{prime}<b^{prime}$ or $a^{prime}=b^{prime}$or $b^{prime}<a^{prime}$
by (15) and (14);

here again the induction hypothesis ($a^{prime}<b$ or $a^{prime}=b$
or $b<a^{prime}$) is not used.

The following is a literal outline of the steps stated in the quoted text:

1. 
   

   $text{Case}left[a=1right]$

   
   
   

   (a) $text{Case}left[a=1,b=1right]$

   
   
   

   (b) $text{Case}left[a=1,b+1=b^{prime}right]$

   
   


2. 
   

   $text{Case}left[a^{prime},bright]$

   
   
   

   (a) $text{Case}left[a^{prime},b<a^{prime}right]$

   
   
   

   (b) $text{Case}left[a^{prime},b=a^{prime}right]$

   
   
   

   (c) $text{Case}left[a^{prime},b>a^{prime}right]$

   
   


3. 
   

   $text{Case}left[a^{prime},b^{prime}right]$

   
   
   

   (a) $text{Case}left[a^{prime},b^{prime}<a^{prime}right]$

   
   
   

   (b) $text{Case}left[a^{prime},b^{prime}=a^{prime}right]$

   
   
   

   (c) $text{Case}left[a^{prime},b^{prime}>a^{prime}right]$

   
   

It is not clear to me whether the case of, say, $a^prime=1^prime$ is expected to be explicitly treated.

Here's what I originally came up with:

Before proving (15) we show

$$
underset{a,c}{forall}a<cimpliesunderset{x}{nexists}c+x=aiffunderset{a,c}{forall}a<cimplies angtr c.tag{A}
$$

First observe that

$$
a<cimpliesunderset{b}{exists}a+b=c.
$$

Now assume $c+x=a,$ implying $c+x+b=c,$ contradicting (12).

My proof of (15) uses (12) and (A):

$$
text{Case}left[a,b<aright]implies aneq bland a>bimplies anless b.
$$

$$
text{Case}left[a,b=aright]implies b=aimplies anless bland bnless a.
$$

$$
text{Case}left[a,b>aright]implies aneq bland b>aimplies bnless a.
$$

This is applicable to all cases, including $a=1$ and $a=1^prime$. I don't see the need for induction. Unless pointing out that it applies to the initial case as well as the general case constitutes induction.

Is my proof correct? Due to the comment this question received, I believe my proof is likely insufficient. If its validity can be shown, it is still lacking in exposition. I was also looking at (15) incorrectly as an exclusive or statement.

A question I have regarding the outline of proof in the quoted text is this:

Should a case $a$ ever be explicitly produced, other than in the initial case of $a=1$?

Apparently the proof is some kind of "leapfrog" or "crab-walk", "bootstrapping" from the base case.

Another question I have is whether the result I have tagged (A) is needed for the proof.

My version of the proof from BBFS tests more cases and conditions than does the proof outlined in the book. I left the additional steps in for the sake of introductory clarity. Ideally the proof should be optimized to use the minimum number of essential steps and to test for the minimum number of conditions.

Rule (12) which says $a<bimplies ane b$ tells us that
$$left(a<blor{a>b}right)implies ane b,text{ and }$$
$$a=bimplies left(anless bland{angtr b}right).$$

We also have
$$
underset{a,c}{forall}a<cimpliesunderset{x}{nexists}c+x=aiffunderset{a,c}{forall}a<cimplies angtr c.
$$

First observe that

$$
a<cimpliesunderset{b}{exists}a+b=c.
$$

Now assume $c+x=a,$ implying $c+x+b=c,$ contradicting (12).

The mutual exclusivity of the cases $a<b,a=b,a>b$ has thus been shown.

The following pseudo-code illustrates how the proof described in the book works for the first three values of $a$. For any larger values, the TestLoop runs through all cases for which $b^prime<a$. The subsequent comparison tests render the same results for every value of $a>1$

The STATE constants should be interpreted as
$$Lpequiv{a^prime{<b}}; Ltequiv{a<b}; Etequiv{a=b}; Gtequiv{a>b}; Gpequiv{a>b^prime}.$$

I will be stunned if all of this is correct, but I'm pretty sure it sufficiently represents the intent of the authors of my book.

STATE={Lp,Lt,Et,Gt,Gp};

Cmp[a,b]{

  Case[a<b]:{

    Case[a+1<b ]:Return@Lp;

    Case[a+1==b]:Return@Lt;

  };

  Case[a==b]:Return@Et;

  Case[a>b]:{

    Case[a==b+1]:Return@Gt;

    Case[a>b+1 ]:Return@Gp;

  };

  Case:Throw@Error;

};



TestLoop[a]:=For[i=1;Cmp[a,i++]==Gp;]{b=i};

a=1; b=1;

TestLoop[a]; //no loops; b==1;

Cmp[a  ,b  ]==Et;Cmp[a  ,b+1]==Lt;Cmp[a  ,b+2]==Lp;Cmp[a  ,b+3]==Lp;

Cmp[a+1,b  ]==Gt;Cmp[a+1,b+1]==Et;Cmp[a+1,b+2]==Lt;Cmp[a+1,b+3]==Lp;

Cmp[a+1,b+1]==Et;Cmp[a+1,b+2]==Lt;Cmp[a+1,b+3]==Lp;Cmp[a+1,b+4]==Lp;



++a==2; b=1;

TestLoop[a]; //no loops; b==1;

Cmp[a  ,b  ]==Gt;Cmp[a  ,b+1]==Et;Cmp[a  ,b+2]==Lt;Cmp[a  ,b+3]==Lp;

Cmp[a+1,b  ]==Gp;Cmp[a+1,b+1]==Gt;Cmp[a+1,b+2]==Et;Cmp[a+1,b+3]==Lt;

Cmp[a+1,b+1]==Gt;Cmp[a+1,b+2]==Et;Cmp[a+1,b+3]==Lt;Cmp[a+1,b+4]==Lp;



++a==3; b=1;

TestLoop[a]; //1 loop; b==2;

Cmp[a  ,b  ]==Gt;Cmp[a  ,b+1]==Et;Cmp[a  ,b+2]==Lt;Cmp[a,b+3  ]==Lp;

Cmp[a+1,b  ]==Gp;Cmp[a+1,b+1]==Gt;Cmp[a+1,b+2]==Et;Cmp[a+1,b+3]==Lt;

Cmp[a+1,b+1]==Gt;Cmp[a+1,b+2]==Et;Cmp[a+1,b+3]==Lt;Cmp[a+1,b+4]==Lp;

The question was originally why is induction needed? The answer to that is represented by the TestLoop. Basically, it proves there is a contiguous sequence of numbers between the $n^{th}$ step and the non-successor number (that number is $1$ in my universe).