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

Answer 2

Suppose $\neg\neg p$ as well as $p\to\bot$ (where $\bot$ is "False"). Assume $p$. Then by the $\to$-elimination rule, we deduce $\bot$. This is a contradiction, so we discard the assumption $p$ and by the $\neg$-introduction rule, we deduce $\neg p$. However, we originally supposed $\neg\neg p$, so by the $\neg$-elimination rule, we deduce $\bot$. Then by the $\bot$-elimination rule, we deduce $p$. So discard the assumption $p\to\bot$ and by the $\to$-introduction rule, we have $(p\to\bot)\to p$. However, by Pierce's Law, we know $((p\to\bot)\to p)\to p$. So by the $\to$-elimination rule, we deduce $p$. Hence, $\neg\neg p\vdash p$.

If the English explanation is unintelligible, then I will consider trying to write a proof tree. This proof could have been shortened slightly by using the transitivity of $\vdash$ as you suggested, but I opted not to for the sake of self-containment.

Answer 3

The answer is given, with some additional explanatory chat, as the answer to (b*) in these answers to exercises for my Intro to Formal Logic: you might find this useful.

https://www.logicmatters.net/wp-content/uploads/2020/03/Exercises_solutions_23.pdf