Is ¬¬(¬¬P → P) provable in intuitionistic logic?

Question

I have a feeling it's not, because ¬¬P → P is not provable. If it is, I'm not sure what kind of reductio I'd need to negate ¬(¬¬P → P). I believe a textbook somewhere said it was provable in intuitionistic logic, so am I missing something or is the textbook wrong?

Answer 1

If is a propositional statement $\varphi$ is provable in classical logic, its double negation $\neg\neg\varphi$ is provable in intuitionistic logic. This fact is known as Glivenko's theorem (see e.g. here: https://en.wikipedia.org/wiki/Double-negation_translation).

The consequence is that your statement is provable in intuitionistic logic.

Answer 2

The way to see this intuitively is: assume $\neg(\neg\neg P\implies P)$. Then assume $P$, by which $\neg\neg P \implies P$, a contradiction. Therefore $\neg P$. Then, if $\neg\neg P$, by ex falso $P$, so $\neg\neg P \implies P$, again a contradiction. Therefore $\neg\neg(\neg\neg P \implies P)$.