Constructive proof that any two natural numbers are either equal or not equal

constructive-mathematicsintuitionistic-logicnatural numbers

I've been reading a bit about constructive mathematics and one of the first challenges I've found is to prove that any two natural numbers are either equal or not equal assuming only intuitionistic logic and the Peano axioms. I am dividing my proof into two steps; my doubts are about the second one I will point them out. Any help is appreciated!

My procedure is the following:

  1. Any natural number is either equal to zero or different from zero.

    • To prove the base case, suppose that $n=0$. Then, of course, it's true that $n=0$ or $n\neq 0$.
    • Assume now that either $n=0$ or $n\neq 0$. Then, in either case, $n+1\neq 0$. So it's true that $n+1=0$ or $n+1\neq 0$, concluding our proof by induction.

  2. Any two natural numbers are either equal or not equal.

    • Let $m\in \mathbb{N}$ and work inductively on $n$. We already have the base case, since $m=0$ or $m\neq 0$.
    • Suppose inductively that either $m=n$ or $m\neq n$. If $m=n$, then $m\neq n+1$ (this may sound ridiculous, but I am not sure how to prove this). Otherwise if $m\neq n$, either $m=n+1$ or $m\neq n+1$ (again, not even sure if I have the right to state this directly or if I should prove it).

P.S.: How the hell do you prove trichotomy? That might be a topic for another question though.

Best Answer

Unfortunately it does seem you are using $\mathsf{LEM}$ in step $2.$ As you mention yourself:

Otherwise if $m \neq n$, either $m = n+1$ or $m \neq n+1$ [...]

is not justified by anything. (It would of course hold if we had $\mathsf{LEM}$, but we don't have it at our disposal)

There is indeed something critical happening at step $2$ and it's worth pointing out. Let's illustrate this by carefully giving this proof a failed attempt.

(I will be using the notation using the successor function $Sn = n +1$)

Proof Attempt

Let $m$ be given. We will try to show $m = n ~\lor~ m \neq n$ by induction on $x$.

  • Base Case: Show $m = 0 ~\lor~ m \neq 0$. Just as you did, one can do the case distinction $m = 0 ~\lor \exists x : m = S x~$. In the first case obviously $m = 0$ and in the second case we indeed have $m = S x \neq 0$ by an axiom of $\mathsf{PA}$.

  • Induction Step: The induction hypothesis is $$m = n ~\lor m \neq n~ \text{ and we need to show } m = S n ~\lor m \neq S n.$$ Again we do the case distinction $m = 0 ~\lor \exists x : m = S x~$ and in the case $m = 0$ we have $m = 0 \neq S n$.

Now in the second case we have $m = S x$ and what remains to show is $S x = S n ~\lor S x \neq S n~$. Now it's time to remember that the induction hypothesis is $S x = n ~\lor S x \neq n~$ and with this, we are stuck. The induction hypothesis is not strong enough to finish the proof. And this hopefully becomes clearer as we try to fix it:

Fixed Proof

This time we try to show the statement $\forall m: m = n ~\lor~ m \neq n$ by induction on $n$.

  • Base Case: Show $\forall m : ~m = 0 ~\lor~ m \neq 0$. This works the same way as before.

  • Induction Step: This time the induction hypothesis is stronger! It is $$\forall m : m = n ~\lor m \neq n~ \text{ and we need to show } \forall m : ~m = S n ~\lor m \neq S n.$$ So for given $m$ we need to show $m = S n ~\lor m \neq S n~$. As previously we do the case distinction $m = 0 ~\lor \exists x : m = S x~$ and in the case $m = 0$ we have $m = 0 \neq S n$.

But unlike previously, we now have $m = S x$ with induction hypothesis $\forall m : m = n ~\lor m \neq n$, which allows us to conclude $x = n ~\lor x \neq n$. Then we are left with two cases:

  • If $x = n$ we have $S n = S x = m$.
  • Now for $x \neq n$. Assume we had $S n = m = S x$. Then by the injectivity of $S$ (an axiom of $\mathsf{PA}$) we get $n = x$, a contradiction! Therefore $m \neq S n$.

So indeed we were able to show $m = S n ~\lor m \neq S n~$. $~~\Box$

The above proof is constructively valid and hopefully showcased that the crucial part is that we do the induction on the statement which still has $y$ quantified.

Related Question