# 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)$

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?

• $D \lor (C \land E)$ or $D \lor (C \lor E)$ ? – Mauro ALLEGRANZA Jan 2 at 12:33
• Second one, sorry. – Maicake Jan 2 at 12:39

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

• thanks a lot. I m not used to this notation where can I find a little example of it use? – Maicake Jan 2 at 13:06
• You are welcome :-) – Mauro ALLEGRANZA Jan 2 at 14:40
• @Maicake - do you mean the $\bot$ i.e. false symbol ? It means a proposition that is alway false, i.e. a contradiction. – Mauro ALLEGRANZA Jan 2 at 14:41
• I didn't explain well . I mean I usually do this proof drawing trees. It's the first time I see a "linear proof". Also why did you choose to start with RAA? – Maicake Jan 2 at 14:49
• @Maicake - because it is cumbersome to draw a tree with the editor here... But it is easy to convert the proof above in tree form: a starting node for every assumption. – Mauro ALLEGRANZA Jan 2 at 14:50

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)}$$

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

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/