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

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.

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.}$$

• @DanChristensen: No, as I explain in this very answer, that is not proof by contradiction. – Henning Makholm Sep 22 '18 at 20:25
• @DanChristensen: Some texts might describe it as such, because in classical logic there is no urgent need to distinguish between negation introduction and RAA. – Henning Makholm Sep 22 '18 at 20:38
• @DanChristensen: I would not say “stuck”; just “not able to get from there to $P$”. – Arturo Magidin Sep 22 '18 at 20:49
• @DanChristensen You also want to be careful about the term “proof by contradiction”; if you are talking at the level of basic logic, then it has a precise meaning that is more restrictive than the common usage, as indicated correctly by Henning Makholm. Generally, we think of “proof by contradiction” as anything in which we assume the negation of what we want to prove and deduce a contradiction. But formally, it generally refers to a proof of the form $\Bigl( (\Gamma,\neg P)\to (Q\wedge \neg Q)\Bigr)\implies P$, and this argument is not of that type. – Arturo Magidin Sep 22 '18 at 21:01
• @DanChristensen This post by Andrej Bauer and this one by Bob Harper both discuss the mistaken abuse of the term "proof by contradiction" in connection with intuitionistic logic. – MJD Sep 23 '18 at 0:30