Equivalence between $\neg\neg\bot$ and $\bot$ in intuitionistic logic.

Question

As the title says, why are those two equivalent? I can find a simple derivation (using natural deduction) of $\bot$ from $\neg\neg\bot$, but i fail at proving the other implication.

Answer 1

(a) One of the rules of inference in standard natural deduction systems for intuitionistic logic is ex falso quodlibet, i.e.

From $\bot$ infer $\varphi$ for any $\varphi$.

So, as a particular application, we have a one-step derivation of, in particular, $\neg\neg\bot$ from $\bot$.

(b) As you say the other direction is also intuitionistically provable. Thus $\bot$ trivially entails $\bot$ so (by the intuitionistically acceptable version of reductio that if you can infer $\bot$ from $\psi$, then that gives you $\neg\psi$), $\neg\bot$ is a theorem. But then $\neg\neg\bot$ as an assumption, combined with this theorem (so a pair of the form $\neg\psi$, $\psi$) gives you $\bot$ (by the introduction rule for $\bot$).

Answer 2

The $\bot \to \neg\neg\bot$ implication is a special case of $\forall \alpha.\ \forall \beta.\ \alpha \to (\beta \to \alpha)$.
Below there are both derivations using Curry-Howard isomorphism.

Formula $$((\bot \to \bot) \to \bot) \to \bot$$ is a special case of $$\forall \beta.\ \forall \alpha.\ ((\alpha \to \alpha) \to \beta) \to \beta $$ which can be proved by $\lambda$-term $$\lambda f.\ f\ (\lambda x.\ x)$$

The other implication

$$\bot \to ((\bot \to \bot) \to \bot)$$

is a special case of

$$\forall \beta.\ \forall \alpha.\ \beta \to (\alpha \to \beta)$$

which can be proved by $\lambda$-term

$$\lambda x. \lambda f.\ x$$

I hope this helps $\ddot\smile$