Is my proof correct that $a < b \implies S(a) \leq b$?

Question

Proof 1.1: $a < b \iff b = a + d$ for some positive natural number $d$

First we prove that $a < b \implies b = a + d$ for positive $d$. We will prove it by contradiction. Suppose that $d$ is not positive, i.e. $d=0$. Then $b = a + 0 = a$. This is a contradiction, since $a < b \implies a \neq b$ by definition. Therefore $d$ must be positive.

Next we prove that $b = a + d \implies a < b$ for positive $d$. We already have $b = a + d \implies a \leq b$ by definition, but to show that it also implies $a < b$, it suffices to show that $a \neq b$. We can prove this by contradiction. Suppose $a = b$. Then $b = a = a + d$, or $a + 0 = a + d$ by additive identity, or $0 = d$ by cancellation law. However, this is a contradiction, since $d$ must be positive. Therefore $a \neq b$.

Proof 1.2: $a < b \iff S(a) \leq b$

First we prove that $a < b \implies S(a) \leq b$. By proof 1.1 we have $b = a + d$ for some positive $d$. Since $d \neq 0$ we can write $S(k) = d$ for some $k$ without violating Peano's 3rd axiom.

\begin{align} b &= a + d \\ &= a + S(k) \tag{substitution} \\ &= S(a + k) \tag{definition of addition} \\ &= S(a) + k \tag{definition of addition} \\ \end{align}

Next we prove that $S(a) \leq b \implies a < b$. We have $b = S(a) + d$ for some $d$. By definition of addition, $b = S(a+d) = a + S(d)$. By Peano's 3rd axiom, $S(d) \neq 0$, which means $S(d)$ is positive. By proof 1.1 this implies $a < b$.

Answer 1

A couple of comments:

First: With these kinds of elementary results, the key is to spell out exactly what axioms you have, and any theorems you can use that you already have proven from those axioms. It looks like you're working with Peano arithmetic, I assume you have the following axioms:

$\forall x \ s(x) \not = 0$

$\forall x \forall y (s(x) = s(y) \rightarrow x = y)$

$\forall x \ x+0=x$

$\forall x \forall y \ x + s(y) = s(x+y)$

plus induction scheme

You also use the following definitions:

$\forall x \forall y (x \le y \leftrightarrow \exists z \ y = x + z)$

$\forall x \forall y (x < y \leftrightarrow (x \le y \land x \not = y))$

Your proof also needs the following lemma's:

$\forall x \forall y \ s(x) + y = s(x+y)$ (which requires induction to be proven)

$\forall x \forall y \forall z (x + z = y+z \rightarrow x = y)$ (also requires induction)

Second: you'll want to be more clear on what you mean by '$d$ is positive' ... I suggest $0 < d$

Third: In proof 1.2 you write:

Since $d \neq 0$ we can write $S(k) = d$ for some $k$ without violating Peano's 3rd axiom.

That's not a valid step in a proof. You can't say: "this is true, because it doesn't violate any of the axioms". For example, if your axiom is $P$, you can't say: "Hey, $Q$ doesn't violate $P$, so $Q$ is true".

So, you'll need to actually prove the following lemma:

$\forall x (x \not = 0 \rightarrow \exists y \ x = s(y))$

(Hint: requires induction)