I'm working on an assignment and I'm stuck on this proof. I feel like I'm on the right track but I can't find the way to prove the goal.

A ^ B

(A ^ ~C) --> ~D

A -> ~C

(B ^ E) --> (C v D)


I started by ^elim for A and B, then I started a subproof to start eliminating the conditionals, but how could I prove ~E when ~E is not in the premises? Only E is.

I imagined that I would have to eliminate the disjunction on the 4th premise and that I would be able to get to ~E on both of those subproofs but I can't find the logical way to do that. Any help would be appreciated -- Thanks

2 Answers 2


Since one has to derive ¬E one place to start would be E as an assumption. That strategy would attempt to derive a contradiction somewhere after the assumption and then derive ¬E which is the goal.

The rest of the steps I think you are aware of. I am including the results of the proof checker. The proof checker you are using is likely different and you will need to add whatever justification is required by your proof checker.

The disjunctive syllogism (DS) rule on line 11 could be replaced with disjunction elimination by considering separately C and D from the disjunction on line 8 and deriving D from both.

enter image description here

View the proof as verification that the hint to start with E as an assumption should work.

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/

  • What does DS mean on line 11? Commented May 2, 2019 at 19:16
  • @fitch-is-killing-me DS is disjunctive syllogism. Since ~C and C v D are true, then one can derive D. Alternatively one could go through cases. First consider C, but since we have ~C that leads to a contradiction. Then consider D and derive ~D, a contradiction. The going through cases would be disjunctive elimination.when both cases, both disjuncts, lead to the same result. Commented May 2, 2019 at 19:32
  • Thanks for letting me know that! My proof checker is Fitch and it doesn't allow for DS, only proof by cases. I did try the proof by cases, and I was able to get the contradiction in both of those cases. However, when I cite the entire subproof to introduce ~, it tells me it's not a valid application of the rule. Any ideas why? Commented May 3, 2019 at 21:53
  • Never mind, I figured that out. It was telling me it was invalid because the v elim rule was only citing the 2 disjuncts and not the disjunction. But it's all checked now. Thanks so much fo ryour help! Commented May 3, 2019 at 22:05

@FrankHubney's proof is perfectly fine and well done. Using ~I is a common sense approach in many proofs.

But I'll offer a second proof using a different method because seeing a proof from multiple approaches can be instructive.

Just looking at the list of assumptions it was easy to see that you could get ~C from A and then ~D would follow from the combination. Having ~C ^ ~D quickly gets us ~E form Modus Tollens. The following proof verifies the insight gleamed from such visual intuition: enter image description here

You must log in to answer this question.

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