$a < b$ iff $S(a) \leq b$

Question

I want to prove $a < b$ iff $S(a) \leq b$ but I can't figure it out for the life of me, how to even begin.

$S(a)$ is the successor of $a$ and $a < b$ is defined as $a \leq b$ with $a \neq b$. And then $a \leq b$ is defined as $b = a + d$ for some $d$ (all numbers here are natural numbers).

Since it is an iff statement I need to prove both:

$a < b \implies S(a) \leq b$

and

$S(a) \leq b \implies a < b$.

But I don't see any clear method of attack. At first I tried induction on $a$ to prove $a < b \implies S(a) \leq b$ but then the inductive step adds one to $a$ so it may no longer be true that $S(a) < b$.

So I tried inducting on $b$ instead but if we start from $0$ then $a < 0$ is always false since $0 = a + j \implies a=0, j=0$, but $a = j = 0$ isn't allowed.

I'm hopelessly stuck. :(

Answer 1

I think this is more direct than José's proposal:

Suppose that $a<b$, which is to say $a\le b$ and $a\ne b$. We have $a+d=b$ for some $d$, and we can't have $d=0$ because then $a=b$, which would be a contradiction. So $d=Se$ for some $e$ and then $a+Se=b$ implies $Sa+e=b$ by standard properties of addition. Thus $Sa\le b$.

Answer 2

If $S(a)\leqslant b$ then, since $a<S(a)$, $a<b$.

On the other hand, suppose that $a<b$. Then there is some $k\in\mathbb{N}\setminus\{0\}$ such that $a+k=b$ and, since $k\neq0$, $k=S(k')$ for some $k'\in\mathbb N$. But\begin{align}a+k=b&\iff a+S(k')=b\\&\iff S(a)+k'=b\\&\iff S(a)\leqslant b.\end{align}

Answer 3

Suppose $S(a) \le b$; then $a \le S(a)$ also, so by transitivity of $\le$, we have $a \le b$. But if $a = b$, then we would have $S(a) \le a$. We now have to prove this is a contradiction.

To see this, we prove by induction on $a$ that for all $a$, $S(a) \not\le a$. For the base case $a=0$, if $1 \le 0$, then there would be some $n$ such that $1+n = 0$. But then $S(n) = 1+n = 0$, which contradicts one of the Peano axioms. For the inductive case, suppose $S(a) \not\le a$; we need to prove $S(S(a)) \not\le S(a)$. Suppose to the contrary that we had $S(S(a)) \le S(a)$. Then for some $n$, $S(S(a)) + n = S(a) = S(S(a) + n)$. Therefore, $S(a) + n = a$, so $S(a) \le a$, contradicting the inductive hypothesis.

---

Now, for the converse, we will start out with a lemma: for all $a, b$, either $S(a) \le b$, $S(b) \le a$, or $a=b$. We prove by induction on $a$ that for all $b$, this disjunction happens. For the base case $a$, I will leave it as an exercise to prove by induction on $b$ that for all $b$, either $b=0$ or $b = S(b')$ for some $b'$; in the latter case, then $S(0) = 1 \le b$. For the inductive case, fix $a$, and suppose we know that for all $b$, the disjunction happens. Then we need to prove the same thing for $S(a)$. So, for any $b$, we know that either $b=0$ or $b=S(b')$ for some $b$. In the first case, then $S(b) \le S(a)$. In the second case, we either have $S(a) \le b'$, in which case $S(S(a)) \le S(b') = b$; or $a = b'$, in which case $S(a) = S(b') = b$; or $S(b') \le a$, in which case $S(b) = S(S(b')) \le S(a)$.

Now that we've established this lemma, suppose that $a < b$. Then by the previous paragraph, we know that either $S(a) \le b$, $a = b$, or $S(b) \le a$. However, the case $a = b$ contradicts the assumption that $a < b$. Similarly, if $S(b) \le a$, then by the assumption that $a \le b$, we know $S(a) \le S(b)$. By transitivity of $\le$, this would imply $S(a) \le a$, which contradicts what we established above. Therefore, the only remaining possibility is that $S(a) \le b$.

---

(While I was writing this, Henning Makholm's answer gave a much more succinct argument for the $a < b \implies S(a) \le b$ part. I still think the first part of my argument would be useful for pointing out a subtlety which needs to be addressed in the $S(a) \le b \implies a < b$ part.)

Answer 4

Instead of just giving a proof, like all earlier answers seem to do, let me try to show you how you could find a proof, like you asked.

I will be using a 'logical' and 'calculational' approach that may be more formal than you are used to, but which often helps me. (You can find background information in, e.g., EWD1300.)$% \require{begingroup} \begingroup \newcommand{\calc}{\begin{align} \quad &} \newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}} \newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} } \newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & } \newcommand{\endcalc}{\end{align}} \newcommand{\Ref}[1]{\text{(#1)}} \newcommand{\then}{\Rightarrow} \newcommand{\when}{\Leftarrow} %$

After expanding the definitions of $\;<\;$ and $\;\le\;$, you are asked to prove, for every $\;a,b\;,$ $$ \tag{0} \langle \exists d :: d + a = b \rangle \;\land\; a \not= b \;\equiv\; \langle \exists d :: d + S(a) = b \rangle $$ Looking at the shape of these formulas, it seems the best approach to start with the right hand side, and rewrite it working towards the LHS's $\;\langle \exists d :: d + a = b \rangle\;$.

Below is the most straightforward way I could find for that.

---

For every $\;a,b\;$,

$$\calc \tag{RHS} \langle \exists d :: d + S(a) = b \rangle \op\equiv\hint{arithmetic, see below -- working towards $\;\ldots + a = b\;$} \langle \exists d :: S(d) + a = b \rangle \op\equiv\hints{logic: introduce abbreviation $\;e := S(d)\;$, i.e., the one-point rule}\hint{in reverse -- still working towards $\;\ldots + a = b\;$} \langle \exists d,e :: e = S(d) \;\land\; e + a = b \rangle \op\equiv\hint{logic: bring all $\;d\;$'s together -- to simplify} \langle \exists e :: \langle \exists d :: e = S(d) \rangle \;\land\; e + a = b \rangle \op\equiv\hint{every $\;e\;$ is either $\;0\;$ or $\;S(\ldots)\;$, i.e., $\Ref{1}$ -- to simplify} \langle \exists e :: e \not= 0 \;\land\; e + a = b \rangle \op\equiv\hints{arithmetic: add $\;a\;$ to both sides of left part; use right part in left}\hint{-- to remove the $\;e\;$ from the left part} \langle \exists e :: b \not= a \;\land\; e + a = b \rangle \op\equiv\hints{logic: extract part not using $\;e\;$ out of $\;\exists e\;$}\hint{-- to reach our goal} \langle \exists e :: e + a = b \rangle \;\land\; a \not= b \tag{LHS} \endcalc$$

---

Note how this proof is completely 'driven' by our goal (the LHS), and by the desire to simplify.

Also note that apart from the usual rules of arithmetic ($\;+\;$ is symmetrical with identity $\;0\;$, and $\;S(a)+b = S(a+b)\;$), this proof makes clear that the only more advanced rule we used is that our domain consists of $\;0\;$ and successors: for all $\;a\;$, $$ \tag{1} a = 0 \;\not\equiv\; \langle \exists b :: a = S(b) \rangle $$

Finally, note how both directions are proved together: there was no need to have separate $\;\then\;$ and $\;\when\;$ proofs.

$% \endgroup %$