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

enter image description here

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


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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.