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?

  • 1
    $\begingroup$ $D \lor (C \land E)$ or $D \lor (C \lor E)$ ? $\endgroup$ – Mauro ALLEGRANZA Jan 2 at 12:33
  • $\begingroup$ Second one, sorry. $\endgroup$ – 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].

  • $\begingroup$ thanks a lot. I m not used to this notation where can I find a little example of it use? $\endgroup$ – Maicake Jan 2 at 13:06
  • $\begingroup$ You are welcome :-) $\endgroup$ – Mauro ALLEGRANZA Jan 2 at 14:40
  • $\begingroup$ @Maicake - do you mean the $\bot$ i.e. false symbol ? It means a proposition that is alway false, i.e. a contradiction. $\endgroup$ – Mauro ALLEGRANZA Jan 2 at 14:41
  • $\begingroup$ 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? $\endgroup$ – Maicake Jan 2 at 14:49
  • 1
    $\begingroup$ @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. $\endgroup$ – 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.

enter image description here

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/


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.