$\neg \neg A \supset A$ in intuitionistic logic

Question

I read that the formula $\neg \neg A \supset A$ is not intuitionistically valid. Why is that? If someone can explain me I would be glad.

Answer 1

Remember that : $\lnot \lnot A \supset A$ is : $((A \supset \bot) \supset \bot) \supset A$.

According to the BHK-interpretation, a proof of $A \supset \bot$ is a procedure $\gamma_0$ that transform a proof of $A$ into a proof of $\bot$.

A proof of $(A \supset \bot) \supset \bot$ is a procedure $\gamma_1$ that, when "applied" to $\gamma_0$, extract a proof of $\bot$.

Thus, a proof of $((A \supset \bot) \supset \bot)$ must be a procedure $\gamma_2$ that, when "applied" to $\gamma_1$, extract a proof of $A$.

But then, having extracted it, we can use it with $\gamma_0$ to get a proof of $\bot$, and this is impossible : the calculus must be sound, i.e. $\bot$ (the absurdity) has no proof.