Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It only takes a minute to sign up.
Sign up to join this community
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$.
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
