prove $( \lnot \lnot p \Rightarrow p) \Rightarrow (((p \Rightarrow q ) \Rightarrow p ) \Rightarrow p )$ with intuitionistic natural deduction

Question

I'm trying to prove this statement with intuitionistic natural deduction using inference rules like this example :

this is the statement I'm trying to solve :

$$( \lnot \lnot p \Rightarrow p) \Rightarrow (((p \Rightarrow q ) \Rightarrow p) \Rightarrow p)$$

i know how to prove this with the classic method the problem that I'm stuck when i try to solve it using inference rules in bindery tree

Answer 1

This is a proof with Natural Deduction, using only intuitionistically valid rules, that Double Negation implies Peirce's law :

1) $\lnot \lnot p \rightarrow p$ --- assumed [a]

2) $(p \rightarrow q) \rightarrow p$ --- assumed [b]

3) $\lnot p$ --- assumed [c]

4) $p$ --- assumed [d]

5) $\bot$ --- from 3) and 4) by $\rightarrow$-elimination

6) $q$ --- from 5) by $\bot$-rule : from $\bot$, infer $\varphi$

7) $p \rightarrow q$ --- from 4) and 6) by $\rightarrow$-introduction, discharging [d]

8) $p$ --- from 7) and 2) by $\rightarrow$-elimination

9) $\bot$ --- from 3) and 8) by $\rightarrow$-elimination

10) $\lnot \lnot p$ --- from 3) and 9) by $\lnot$-introduction, discharging [c]

11) $p$ --- from 1) and 10) by $\rightarrow$-elimination

The proof, up to now, amounts to : $\lnot \lnot p \rightarrow p, (p \rightarrow q) \rightarrow p \vdash p$

12) $((p \rightarrow q) \rightarrow p) \rightarrow p$ --- from 2) and 11) by $\rightarrow$-introduction, discharging [b], i.e. : $\lnot \lnot p \rightarrow p \vdash ((p \rightarrow q) \rightarrow p) \rightarrow p$

13) $\vdash (\lnot \lnot p \rightarrow p) \rightarrow (((p \rightarrow q) \rightarrow p) \rightarrow p)$ --- from 12) by $\rightarrow$-introduction.

Note : with classical logic, we can avoid the premise : $(\lnot \lnot p \rightarrow p)$ and prove : $\vdash ((p \rightarrow q) \rightarrow p) \rightarrow p$ using Double Negation (which is not intuitionistically valid) in step 11).