MHB Stuck on Derivation (Natural Deduction)

[DragonPoopa]

1. ((N ⊃ P) ⊃ (I ⊃ P)) ⊃ ((P ⊃ I) ⊃ P) P

2. (I v X) ≡ (R ⊃ P) P

3. R ⊃ (I ⊃ (N ^ V)) P

4. R A

5. Reiteration of 3

6. I ⊃ (N ^ V) 3,4 ⊃E

7. I A
8. I v X 7, vI
9. Reiteration of 2
10. R ⊃ P 8,9 ≡E
11. R 4R
12. P 10,11 ⊃E
13. I ⊃ P 7-12 ⊃I

14. N ⊃ P A
15. I ⊃ P 13 R
16. (N ⊃ P) ⊃ (I ⊃ P) 14-15 ⊃I

17. Reiteration of 1

18. (P ⊃ I) ⊃ P 16, 17 ⊃E

Conclusion: R ⊃ (X v V)

Hello!

I got up to this point in my work. I realized that I have to somehow get I v V out to the scope line of R, but I am not sure how to go about this. I am thinking of (P -> I) or (R -> P), but I don't know how from there.

 

[Evgeny.Makarov]

Welcome to the forum.

Apparently, this requires a proof by contradiction or the law of excluded middle. So we assume that R and ~(X v V). The latter implies ~X and ~V. From ~V follows ~(N /\ V), and I -> N /\ V gives ~I. Together with ~X this implies ~(I \/ X), which by the second premise gives R /\ ~P. ~I implies I -> P and (N -> P) -> (I -> P), so from the first premise we have (P -> I) -> P. Then ~P proves P -> I, and we have P and ~P, a contradiction.

I am not sure if there is a shorter proof. I generated a formal proof in a proof assistant program, but it is also not very short.