Can we prove $1\neq 2$ using intuitionistic methods?

Question

Can we prove $1\neq 2$ using intuitionistic methods? It is trivial to prove conventionally starting from Peano's Axioms, but it seems to require a proof by contradiction.

Answer 1

Assume $S(0)=S(S(0))$.

One of the Peano axioms say that $S(x)=S(y) \to x=y$, so we immediately conclude $0=S(0)$. But this contradicts the axiom $\forall x(0\ne S(x))$.

Thus $S(0)\ne S(S(0))$.

This reasoning is intuitionistically valid. It is not proof by contradiction, but merely the negation introduction rule which is allowed in intuitionistic logic:

$$ \frac{\Gamma, P\vdash \bot}{\Gamma \vdash \neg P}\;\neg\,\text{-intro} $$

Actual proof by contradiction (which is not allowed in intuitionistic logic) would be $$ \frac{\Gamma, \neg P\vdash \bot}{\Gamma\vdash P}\;\text{r.a.a.}$$