Double negation

Question

Prove using intuitionistic logic and Pierce’s Law that $\neg\neg p\vdash p$.

I tried doing so, but I couldn’t make much progress. In particular, I couldn’t show that $\neg\neg p \vdash (p\to \neg\neg p) \to p$. I think the transitivity property of deductibility might be useful.

Answer 1

First note that $(\neg P \to P) \equiv \neg \neg P $ can be (intuitionistically) proven.

Let one have $\neg P \to P$, i.e. $(P \to \bot)\to P$ as premise. Hypothesis $(P \to \bot)$ yields $P$, and with hypothesis we have $\bot$. so by removing hypothesis we have $(P \to \bot)\to \bot$, i.e. $\neg \neg P$.

Let one have $\neg \neg P$. This is $\neg P \to \bot$. Hypothesis $\neg P$ yields $\bot$, and $\bot$ proves everything, for example $P$, so we have $\neg P \to P$ by removing hypothesis.

Let $x = P$, $y = \bot$ then Peirce law gives $$((x \to y) \to x ) \to x$$ $$((P\to \bot)\to P)\to P $$ $$(\neg P \to P)\to P $$ which is $ \neg \neg P \to P$.