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?

5 Answers 5


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:

enter image description here

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.


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

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .