# Intuitionistic proof of $\neg\neg(\neg\neg P \rightarrow P)$

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

• @avid19 Better? Btw, this question is not a duplicate of the one linked, as my edit shows. Dec 21, 2015 at 3:50
• 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. Dec 21, 2015 at 3:58
• I also voted to reopen.
– user223391
Dec 21, 2015 at 4:04

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