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.

  • 2
    $\begingroup$ Double negation translation isn't just a matter of sticking $\lnot \lnot$ in front of the formula, though... $\endgroup$ – Zhen Lin Oct 23 '15 at 22:27
  • $\begingroup$ @ZhenLin: Ok, strictly speaking you are right. What I really had in mind was Glivenko's theorem. Fixed it! Thanks for your comment. $\endgroup$ – russoo Oct 23 '15 at 22:34
  • $\begingroup$ 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. $\endgroup$ – debstack Oct 23 '15 at 23:37
  • $\begingroup$ 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. $\endgroup$ – russoo Oct 23 '15 at 23:50
  • $\begingroup$ 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...). $\endgroup$ – 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)$.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.