Disjunctive Syllogism in a Fitch Style System

Question

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.

Answer 1

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.

Answer 2

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/

Answer 3

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