# Disjunctive Syllogism in a Fitch Style System

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.

• 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]. 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. 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. Oct 10 '13 at 22:57
• +1 Shows research effort, is clear, and might even be useful to others. No less importantly, it has the appropriate tags. 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.

• 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. 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! 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 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).

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 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
``````