How do you prove $\neg\neg(\neg\neg P \rightarrow P)$ in intuitionistic logic?

I know this statement to be intuitionistically provable because of Glivenko's theorem. However, I wish to prove it intuitionistically.

The relevant axioms I happen to be using are: (1) $\neg P = P\rightarrow\bot$ and (2) $\bot \rightarrow P$.

  • $\begingroup$ @avid19 Better? Btw, this question is not a duplicate of the one linked, as my edit shows. $\endgroup$ Dec 21, 2015 at 3:50
  • 1
    $\begingroup$ There is a proof outline in the comments of the linked answer, but with the edit, I agree that this is no longer a duplicate, and I've voted to reopen. $\endgroup$ Dec 21, 2015 at 3:58
  • 1
    $\begingroup$ I also voted to reopen. $\endgroup$
    – user223391
    Dec 21, 2015 at 4:04

1 Answer 1


The first thing to notice is that $$(\lnot(\lnot\lnot P \to P)) \to \lnot P\qquad(\star)$$ Indeed, suppose $\lnot(\lnot\lnot P \to P)$ and $P$ ; we want to show $\bot$.

By modus ponens, it suffices to prove $\lnot\lnot P \to P$, but as you supposed $P$, the implication is clearly true.

Now, for the main result, suppose $\lnot(\lnot\lnot P \to P)$ ; you want to show $\bot$. By modus ponens, it suffices to show $\lnot\lnot P \to P$. Suppose now $\lnot\lnot P$. By $(\star)$, you also have $\lnot P$, and you know that $\lnot\lnot P \land \lnot P \to \bot$. Thus you have $\bot$, thus $P$, and the result is proved.

Edit : This proof is, on some points, similar to the proof of $\lnot\lnot(P\lor\lnot P)$, delightly explained by Phil Wadler in section 4 of http://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .