# How to derive ( E v C ) using sentential derivations?

I'm having a really hard time trying to derive (E v C) from {~A > ~B, A > C, B v D, D > E}. Where '>' is the material conditional, so that 'A > C' is read as "If A then C".

I used negation elimination (A/~E) to assume ~A, and from that got ~B from conditional elimination.

In order to get B, I'm trying to use Disjunction Elimination, but I'm having trouble getting D to yield B.

How do I solve this problem?

With Natural Deduction :

1) ¬A → ¬B --- premise

2) A → C --- premise

3) B ∨ D --- premise

4) D → E --- premise

5) ¬A --- assumed [a]

6) B --- assumed [b]

7) ¬B --- from 1) and 5) by →-elimination (modus ponens)

8) --- from 6) and 7)

9) A --- from 5) and 8) by ¬-introduction and Double Negation, discharging [a]

10) C --- from 2) and 9) by →-elimination (modus ponens)

11) E ∨ C from 6) by ∨-introduction

12) D --- assumed [c]

13) E --- from 4) and 12) by →-elimination

14) E ∨ C from 13) by ∨-introduction

We have derived E ∨ C both under assumption B and under assumption D; thus, we can apply ∨-elimination, with premise 3) B ∨ D :

15) E ∨ C from 3), 5)-11) and 12)-14) by ∨-elimination, discharging assumptions [b] and [c].

I won't give you a complete answer as this looks like homework, but I'll give you a hint:

You need to look at the possible values of A. What is implied when A is true? And what happens when A is false?

{~A > ~B, A > C, B v D, D > E}

We want to show that (E v C) is true.

Now, suppose E is true. Then we're done

So, suppose E is false. Since D > E, D must be false.

Since B v D is true and D is false, B must be true.

Since B is true, ~B is false.

Since ~A > ~B and ~B is false, ~A must be false and A must be true.

Since A > C and A is true, C must be true.

So either E is true, or else C is.

QED. Or as I learned in a MOOC with a lot of French students, CQFD, ce qu'il fallait démontrer.

This proof is similar to that provided by user4894 except I presented it in the Fitch-style notation using Klement's proof checker:

The proof uses the following rules: disjunction introduction (vI), modus tollens (MT), disjunctive syllogism (DS), contradiction introduction (⊥I), negation introduction (¬I), double negative elimination (DNE), conditional elimination (→E) and the law of the excluded middle (LEM).

Details about these rules may be found in forall x: Calgary Remix.

References

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/

You have B v D as a premise so why not use it? Assuming the case is D, derive C v E from D > E . Assuming the case is B, derive C v E from ~A > ~B and A > C. Eliminate that disjunction.

`````` 1|  ~A > ~B
2|  A > C
3|  B v D
4|_ D > E
5|  |_ B       Assume
6|  |  |_ ~A   Assume                :
7|  |  |  ~B   > elimination 1,6     :
8|  |  |  #    ~ elimination 5,7     :
9|  |  ~~A     ~ introduction 6-8    or Modus Tolens 1,5
10|  |  A       ~~ elimination 9
11|  |  C       > elimination 2,10
12|  |  C v E   v introduction 11
/  /
13|  |_ D       Assume
14|  |  E       > elimination 4,13
15|  |  C v E   v introduction 14
16|  C v E      v elimination 3,5-12,13-15
``````