Natural deduction proof of $(A \to \lnot B \lor C), ((\lnot D \land A) \to B), (\lnot E \to A) \vdash D \lor (C \lor E)$

Question

I'm struggling to proof this both if I use or introduction rule $\lor_{I_1}$ (to work on $D$) or or introduction rule $\lor_{I_2}$ (to work on $C \lor E$). Could you help me?

Answer 1

We will work by contradicition, starting assuming :

1) $\lnot [D \lor (C \lor E)]$ --- assumed [a]

2) $\lnot D$ --- assumed [b]

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

4) $A$ --- from 3) and premise-3

5) $\lnot D \land A$ --- from 2) and 4)

6) $B$ --- from 5) and premise-2

7) $\lnot B \lor C$ --- from 4) and premise-1

Now we need $\lor$-elim on 7)

8) $\lnot B$ --- assumed [d1] from 7)

9) $\bot$ --- contradiction ! with 6) and 8)

10) $C$ --- assumed [d2] from 7)

11) $C \lor E$ --- from 10)

12) $D \lor (C \lor E)$ --- from 11)

13) $\bot$ --- contradiction ! with 1) and 12)

We have derived $\bot$ in both cases of the $\lor$-elim; thus we have :

14) $\bot$ --- from 8)-9) and 10)-13) and 7) by $\lor$-elim, discharging assumptions [d1] and [d2]

15) $E$ --- from 3) and 14) by RAA and DN, discharging [c]

16) $C \lor E$ --- from 15)

17) $D \lor (C \lor E)$ --- from 16)

18) $\bot$ --- contradiction ! with 1) and 17)

19) $D$ --- from 2) and 18) by RAA and DN, discharging [b]

20) $D \lor (C \lor E)$ --- from 19)

21) $\bot$ --- contradiction ! with 1) and 20)

22) $D \lor (C \lor E)$ --- from 1) and 21) by RAA and DN, discharging [a].

Answer 2

$A \implies \lnot B \lor C$ is equivalent to $\lnot B\lor C$ or $\lnot A$

$\lnot D \land A \implies B $ is equivalent to $B$ or $D\lor \lnot A$

$\lnot E \implies A$ is equivalent to $A$ or $E$

So you want to prove that $\lnot A \lor \lnot B\lor C$, $\lnot A\lor B\lor D$, $A\lor E$ gives you $C\lor D\lor E$. Can you show this last step?

Answer 3

Natural deduction proof of $(A \to \lnot B \lor C), ((\lnot D \land A) \to B), (\lnot E \to A) \vdash D \lor (C \lor E)$

Here is a skeleton; just flesh it out.   The subproofs are mostly proofs by reduction to absurdity, and a proof by cases.

$$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{(A \to \lnot B \lor C)\\ ((\lnot D \land A) \to B)\\ (\lnot E \to A) }{\fitch{\lnot(D\lor (C\lor E))}{\fitch{~}{~\\~\\\fitch{~}{\fitch{~}{~\\~\\\bot}\\~\\~\\D\lor(B\lor E)\\\bot}\\~\\\fitch{~}{~\\D\lor(C\lor E)\\\bot}\\~\\\bot}\\~\\~\\~\\D\lor(C\lor E)\\\bot}\\~\\D\lor (C\lor E)}$$

Answer 4

Here is a proof using the Law of Excluded Middle (LEM). Links to the text explaining the terms and the proof checker are at the bottom.

---

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/