I'm trying to prove an argument of the form:

  1. B
  2. ~(C & B)

Therefore: ~C.

I can expand out ~(C & B) into ~C OR ~B, and with the premise B, it is clear that ~C is the case.

However, I'm having trouble proving this using a Fitch style system. I've tried disjunctive elimination, but I can't see how to get to ~C from an assumption of ~B, so I'm wondering whether or not this is the correct way to go.

If anyone knows how to show the equivalent of a disjunctive syllogism in Fitch, or at least somewhere to find out how, some direction would be greatly appreciated.

  • 2
    Assume C. Conjoin C and B to get (C & B), which contradicts premise 2. Conclude ~C. [the only rules used here are: &-Intro, Bottom/Absurd-Intro, ~-Elim]. – Hunan Rostomyan Oct 10 '13 at 22:50
  • Indeed, thank you. I just figured that out. I was making it much harder than it was by focusing on disjunctive elimination. – Sinthet Oct 10 '13 at 22:53
  • Here's one with De Morgan & v-Elim: Push the negation in premise (2) to get (~C v ~B). Assume ~C. Reiterate to get ~C. Assume ~B to get a contradiction with premise (1) and conclude ~C. Since ~C follows from both cases, it follows by v-Elim that ~C. – Hunan Rostomyan Oct 10 '13 at 22:57
  • 1
    +1 Shows research effort, is clear, and might even be useful to others. No less importantly, it has the appropriate tags. – Hunan Rostomyan Oct 11 '13 at 0:11

Here are a couple options:

  • If you have a double negation rule, you can turn B into ~~B. Then you can use a disjunctive syllogism rule together with (~C v ~B) to get ~C.

  • You can try an indirect proof, where you assume C, and then conjoin it with B to get (C & B), which yields a contradiction with line 2, entailing ~C.

| improve this answer | |
  • Hey, thanks for replying! The problem I'm having is due to the absence of a disjunctive syllogism rule. The only way to do an v elimination in Fitch is via Proof by Cases (where the cases are sub-proofs). If I go with an indirect proof and get (C & B), then all I can do within Fitch is introduce a contradiction, from which I can derive ~(C & D), but then I'm back where I started again. An overview of the system Im working in. – Sinthet Oct 10 '13 at 22:42
  • And.... Disregard that :). I indeed solved it with an indirect proof, not quite sure how I overlooked that possibility. I was so focused on using DeMorgan's Laws in my proof that I forced myself into thinking disjunctive elimination had to be the way to proceed. Thank you! – Sinthet Oct 10 '13 at 22:52

Here is an approach that uses disjunctive elimination. Given the following I assume the DeMorgan rules are available:

I can expand out ~(C & B) into ~C OR ~B

enter image description here

On line 3, I used DeMorgan rules (DeM) to get a disjunction which I will then need to eliminate to reach the goal.

To eliminate the disjunction, I have to consider both disjuncts, "¬C" and "¬B".

The first disjunct is the easiest, but it may be confusing because it is so easy. The assumption, "¬C", for that subproof is precisely what I want to show. There is nothing more to do (at least for this proof checker).

The second disjunct uses explosion based on the observation that lines 1 and 5 are contradictory. This proof checker allows me to state the contradiction (⊥) on line 6 and use explosion (X) on line 7 to reach the conclusion that I want "¬C". The one you are using may require something different.

Since I have the same conclusion for each disjunct I can discharge the two assumptions on lines 4 and 5 by citing the rule of disjunction elimination (∨E). In this proof checker I have to reference the disjunction itself (3), the first subproof (which is only line 4 but written as a range 4-4), and the second subproof (5-7).


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/

| improve this answer | |

You have been promised B and ~(C ^ B). Should you assume C you may derive C ^ B from the first premise, contradicting the second premise, enabling you to discharge the assumption using negation introduction and thus deduce ~C as required. That is all.

|  B           Premise
|_ ~(C ^ B)    Premise
|  |_ C        Assumption
|  |  C ^ B    Conjunction Introduction
|  |  #        Negation Elimination
|  ~C          Negation Introduction

Well, the version of negation introduction rule which your system employs may vary, but that is basically it.

|  B           Premise
|_ ~(C ^ B)    Premise
|  |_ C        Assumption
|  |  C ^ B    Conjunction Introduction
|  C->(C ^ B)  Conditional Introduction
|  |_ C        Assumption
|  |  ~(C ^ B) Reiteration
|  C->~(C ^ B) Conditional Introduction
|  ~C          Negation Introduction
| improve this answer | |

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.