Constructive proof that only zero is less than one

Question

Based on intuitionistic number theory as defined in https://plato.stanford.edu/entries/logic-intuitionistic/#IntNumTheHeyAri, I'm trying to prove that if $x < 1 \Rightarrow x = 0$ (with $1 = S(0)$ being the successor of $0$).

By the definition of comparison, I get $\exists z: (S(z) + x = S(0))$, which allows me to easily prove that $\neg\neg(x = 0)$ using the characterization of $0$ as the least natural number. But I can't seem to find a proof for the positive form of the conclusion.

Since it cannot be proven by contradiction, I assume I would have construct a proof of being equal to $0$ for any number that fits.

Any ideas?

Answer 1

One way you could go about it is to prove that addition is commutative. (Hint: Show that $0+y=y$ for all $y$ by induction, so that $0+y=y+0$ for all $y.$ Then, suppose that there is some $x$ such that $x+y=y+x$ for all $y,$ and show that $S(x)+y=y+S(x)$ for all $y.$ Conclude by induction.)

Next, you could show that the relation given by $$x\le y\iff\exists z:(z+x=y)$$ is antisymmetric using the comparative law $$\forall x\forall y,(x<y\vee x=y\vee y<x).$$ Then by commutativity, you have $$x+S(z)=S(0),$$ so that $$S(x+z)=S(0)$$ by the recursive definition, so that $$x+z=0$$ by one-to-one, so $$z+x=0$$ by commutativity, and so $$x\le 0,$$ and since $$0\le x$$ is readily provable, then antisymmetry of $\le$ gives $$x=0.$$

---

Added: I'm not sure whether we can prove antisymmetry of $\le$ without the Law of the Excluded Middle, but at any rate, there's another way we can go.

First, I will prove a logical form that holds in constructive logic. I will use Modus Ponens and the axioms $$\neg A\to(A\to B)\tag{1}$$ and $$(A\to C)\to\Bigl((B\to C)\to\bigl((A\vee B)\to C\bigr)\Bigr)\tag{2}$$ from section 2.1 of the link you posted, together with the result $$A\to A\tag{3}$$ from section 2.2.

Lemma $1$: $\bigl((A\vee B)\wedge\neg B)\to A$

Proof:

• Assume $A\vee B$ and assume $\neg B.$

• By $(3),$ we have $$A\to A.$$

• By $(1),$ we have $$\neg B\to(B\to A),$$ so since $\neg B,$ then by Modus Ponens, we have $$B\to A.$$

• By $(2),$ we have $$(A\to A)\to\Bigl((B\to A)\to\bigl((A\vee B)\to A\bigr)\Bigr),$$ so since $A\to A,$ then by Modus Ponens, we have $$(B\to A)\to\bigl((A\vee B)\to A\bigr),$$ so since $B\to A,$ then by Modus Ponens, we have $$(A\vee B)\to A,$$ so since we have $A\vee B,$ then by Modus Ponens, we have $A.$ $\Box$

Next, consider the following statement of Heyting Arithmetic:

$$A(z):=(z=0)\vee\Bigl(\exists y:\bigl(S(y)=z\bigr)\Bigr).$$

Lemma $2$: $\forall z,A(z)$

Proof: Clearly, $A(0).$

Given any $z,$ it is also clear that $A\bigl(S(z)\bigr).$ Thus, by the axiom $$A\to(B\to A),$$ we see that $$A(z)\to A\bigl(S(z)\bigr).$$ We conclude by induction. $\Box$

Finally, we conclude the desired result.

Claim: $(x<1)\to(x=0).$

Proof:

• Assume that $x<1,$ meaning that the following (equivalent) conditions hold: $$\exists z:S(z)+x=1\\\exists z:S(z)+x=S(0)\\\exists z:x+S(z)=S(0)\\\exists z:S(x+z)=S(0)\\\exists z:x+z=0$$

• Applying Lemma $2$, we conclude that the following equivalent conditions hold: $$(x+0=0)\vee\Bigl(\exists y:\bigl(x+S(y)=0\bigr)\Bigr)\\(x=0)\vee\Bigl(\exists y:\bigl(x+S(y)=0\bigr)\Bigr)\\(x=0)\vee\Bigl(\exists y:\bigl(S(x+y)=0\bigr)\Bigr).$$

• Since $\neg\bigl(S(x)=0\bigr),$ then $\neg\Bigl(\exists y:\bigl(S(x+y)=0\bigr)\Bigr),$ and so by Lemma $1$, we conclude that $x=0.$ $\Box$

Answer 2

You can trivially prove $\forall n.n=0\lor\exists m.n=S(m)$ with induction.

You then want to prove that $(\exists n.S(n)+x=S(0))\to x=0$. Equivalently, $\forall n. S(n)+x=S(0)\to x=0$. We do a case analysis on the above lemma instantiated to $x$ to get either $x=0$, in which case we're done, or $\forall n.S(n)+S(m)=S(0)\to S(m)=0$. By definition of addition, the premise is equivalent to $S(S(n)+m)=S(0)$ and, by injectivity and extensionality of $S$, this is equivalent to $S(n)+m=0$. (The remainder of this is essentially a proof that $\forall n.n\not<0$.) We can apply our lemma again to $m$ to get either $m=0$ producing $S(n)=0$ (via the definition of addition) which is a contradiction with $0$ being the least natural, or we get $S(n)+S(m')=0$ where we again use the definition of addition to get $S(S(n)+m')=0$ which is also a contradiction for the same reason, and we're done.