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

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?

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.

• Double negation translation isn't just a matter of sticking $\lnot \lnot$ in front of the formula, though... – Zhen Lin Oct 23 '15 at 22:27
• @ZhenLin: Ok, strictly speaking you are right. What I really had in mind was Glivenko's theorem. Fixed it! Thanks for your comment. – russoo Oct 23 '15 at 22:34
• Thanks, this is just what I needed! Do you have a link somewhere where I can see the proof of Glivenko's theorem? I want to understand that first. – debstack Oct 23 '15 at 23:37
• I am not able to find a clear exposition of the proof at the moment. But you can try to prove the theorem by yourself. If you are using Hilbert-style proof systems, you can proceed as follows: First, show that for each axiom $\varphi$ of the Hilbert system for classical logic, the formula $\neg\neg \varphi$ is provable in intuitionistic logic. Then, you should show that $\vdash_I \neg\neg \varphi$ and $\vdash_I \neg\neg(\varphi \to \psi)$ implies $\vdash_I \neg\neg\psi$ where $\vdash_I$ means "provable in intuitionistic logic". The result then follows by induction on the lengths of proofs. – russoo Oct 23 '15 at 23:50
• A remark: For the above method of proof to work, it is sufficient if the classical logic is given by a Hilbert-style proof system. For the intuitionistic logic, you can use any kind of proof system you like (e.g. natural deduction for intuitionistic logic, tableaux systems for intuitionistic logic...). – russoo Oct 24 '15 at 0:04

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

• Intuitionistic does not mean intuitive. – Mark S. Nov 2 '15 at 21:41
• This, however, is an intuitionistic proof. – Graham Kemp Aug 30 '18 at 23:23