Prove $n<m{++}\leq n{++}\iff m=n$ from Peano Axioms

The problem is,

Prove that $n<m{++}\leq n{++}\iff m=n$.

Using only the followings,

1. Peano Axioms (see the axioms here).

2. Definition of Addition: Let $m$ be a natural number. We define, $0 + m = m$ and suppose we have inductively defined the addtion $n + m$ then we define, $(n{++})+m=(n+m){++}$. Where $n{++}$ is the successor of $n$.

3. Commutativity, Associativity and Cancellation Laws of Addition.

4. Definition of Positivity: A natural number $n$ is said to be positive if $n\neq 0$.

5. Definition of $\ge$ and $>$: Let $m$ and $n$ be two natural numbers. We say $n\ge m$ or $m\le n$ if there exists some natural number $a$ such that $n=m+a$. We say $n>m$ or $m<n$ if $n\ge m$ (or $m\le n$) but $n\ne m$.

While trying to prove that for natural numbers $a$ and $b$ if $a<b$ then $a{++}\le b$ I found out that to prove that proposition I had to assume the fact that (speaking loosely) there exists no natural number between any natural number and its successor. I thought that this should be an axiom because even if it weren't true it wouldn't contradict the Peano Axioms. However, I am skeptic of my assertion and so I decided to post it as a problem. I will be glad if someone can show me a proof of this assertion using only the statements I have given.

Note that, this question mainly focuses on the fact that whether the Peano Axioms are sufficient to let us conclude that, loosely speaking,

There exists no natural number in between a natural number and its successor.

And so we can claim that the natural number that the axioms are sufficient to construct our "wanted" natural numbers.

• This is best proved by induction. – Thomas Andrews Dec 25 '14 at 13:11
• @ThomasAndrews: I tried but couldn't. Can you give a proof? – user 170039 Dec 25 '14 at 13:13
• @drhab: If $n=1$ then $n{++}=2$. – user 170039 Dec 25 '14 at 13:34
• No, $n++=2$ and it is not true that $n<m++$. @drhab $m++=m+1$, not $m+1+1$, a slight confusion. $++$ is used in some programming languages to indicate a single increment. – Thomas Andrews Dec 25 '14 at 13:34
• @user170039 Are you sure? If $n=1$ then $n+=2$ and $n++=3$. – drhab Dec 25 '14 at 13:35

First prove by induction: $$\begin{array}{ll}(1) && \forall n :n=0 \lor n=1 \lor n>1\\ (2) &&\forall n : n= 0 \lor \exists z : z++=n \end{array}$$

Let $P(n,m):= n<m++\leq n++ \Rightarrow m=n$

Now show the statement $\forall n\forall m P(n,m)$ by induction on $n$:

Base Case $(n=0)$: $\forall m P(0,m)$

Let $m$ be arbitrary and assume $0<m++\leq 0++=1$

By (1) $m++=1$ so $m=0$

Inductive step: $\forall m P(n,m) \Rightarrow \forall m P(n++,m)$

By inductive assumption we have $\forall m :n < m++ \leq n++ \Rightarrow m=n$.

We have to show $\forall m :n++ < m++ \leq (n++)++ \Rightarrow m=n++$

For that let m be arbitrary and assume $n++ < m++ \leq (n++)++$

By commutativity of addition/cancellation laws: $n < m \leq n++$

By (2) pick $z$ such that $z++=m$ (it is easily shown that $m \neq 0$)

But by inductive assumption $n < z++ \leq n++$ implies $z = n$

Therefore $m=z++=n++$

• I don't understand the sixth line. Instead of $m{++}$, I think it should be $(m{++}){++}$. – user 170039 Dec 28 '14 at 12:46
• @user170039 No, Let $P(n,m) = n < m++ \leq n++ \Rightarrow m=n$, you want to show $\forall m \forall n P(n,m)$ I did this by showing $\forall m P(n,m)$ by induction over n. So the base case is $\forall m P(0,m)$ and the inductice step is $\forall m P(n,m) \Rightarrow \forall m P(n++,m)$ – Achilles Dec 28 '14 at 14:55
• If you apply induction on $n$ then $m$ must be fixed. Then the transition from $P(n,m)$ to $P(n{++},m)$ isn't very clear to me. It will be good if you can explain every step a bit elaborately. – user 170039 Dec 29 '14 at 4:25
• @user170039 the transition goes from $\forall m P(n,m)$ to $\forall m P(n++,m)$ see edits – Achilles Dec 29 '14 at 5:00
• Just one more question. How do you prove the base case of $(1)$? Let me elaborate what I have done. Basically $(1)$ equivalent to $\forall n: n=0\lor n\geq 0{++}$. "We apply induction on $n$. We let, $P(n):n=0\lor n\ge 0{++}$. Now note that $P(0)$ holds since in this case $n=0$. So now we inductively assume $P(n)$ to be true, i.e., $n=0\lor n\ge 0{++}$. To prove $P(n{++})$, i.e., $n{++}=0\lor n{++}\ge 0{++}$ we note that by Axiom 1.3 $a{++} \ne 0$." After that I can't proceed. Can you help? – user 170039 Dec 29 '14 at 5:47