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?
Best Answer
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.