¿Podemos demostrar $1\neq 2$ utilizando métodos intuicionistas?

Question

¿Podemos demostrar $1\neq 2$ utilizando métodos intuicionistas? Es trivial de demostrar convencionalmente a partir de los axiomas de Peano, pero parece requerir una prueba por contradicción.

Answer 1

Supongamos que $S(0)=S(S(0))$ .

Uno de los axiomas de Peano dice que $S(x)=S(y) \to x=y$ por lo que concluimos inmediatamente $0=S(0)$ . Pero esto contradice el axioma $\forall x(0\ne S(x))$ .

Así $S(0)\ne S(S(0))$ .

Este razonamiento es intuitivamente válido. Es no prueba por contradicción sino simplemente la regla de introducción de la negación que es permitidos en la lógica intuicionista:

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

La prueba real por contradicción (que no está permitida en la lógica intuicionista) sería $$\frac{\Gamma, \neg P\vdash \bot}{\Gamma\vdash P}\;\text{r.a.a.}$$