Fitch Proof Exercise 6.20

Question

I am working on a proof and am stuck on a step. I am not sure why I cannot assume the negation of B. Is it not allowed or am I missing something? Thank you]1

Answer 1

I am not sure why I cannot assume the negation of B.

You can assume it; it just will not do anything for you. You do not have the disjunction ~B v C derived anywhere to "eliminate".

Disjunction elimination is the "Proof By Cases" structure. Building it requires a disjunction, and two subproofs. In each subproof you derive the same conclusion from the assumption of either from the two cases of the disjunction.

You have built subproof for the so called "elimination" of premise A v B. You need to build subproofs for the "elimination" of A v C; so one assumes A and the other assumes C.

Well, you have basically already done everything you need. You just have to copy the first subproof.

 1.|  A v B             premise
 2.|_ A v C             premise
 3.|  |_ A              assumption
 4.|  |  A v (B & C)    v-intro 3
   |  +
 5.|  |_ B              assumption
 6.|  |  |_ A           assumption
 7.|  |  |  A v (B & C) v-intro 6
   |  |  + 
 8.|  |  |_ C           assumption
 9.|  |  |  B & C       &-introduction 5,8
10.|  |  |  A v (B & C) v-introduction 9
11.|  |  A v (B & C)    v-elimination 2,6-7,8-10
12.|  A v (B & C)       v-elimination 1,3-4,5-11

---

Note: Some proof checkers do allow you to reference subproofs in parent contexts rather than repeating the work (the same as referencing statements). I am not sure about yours, but it is worth a try.

 1.|  A v B             premise
 2.|_ A v C             premise
 3.|  |_ A              assumption
 4.|  |  A v (B & C)    v-intro 3
   |  +
 5.|  |_ B              assumption
 6.|  |  |_ C           assumption
 7.|  |  |  B & C       &-introduction 5,6
 8.|  |  |  A v (B & C) v-introduction 7
 9.|  |  A v (B & C)    v-elimination 2,3-4,6-8
10.|  A v (B & C)       v-elimination 1,3-4,5-9

Answer 2

Inside the subproof for B: Instead of doing a subproof with ~B, do one with A, so that you set up a v Elim on A v C

Also: I note that the last line does not check out ... did you forget to select A v B as the statement on which to apply the v Elim? It's a common mistake to only point to the subproofs, and forget to point to the v statement that is actually being eliminated. Indeed, for the line that you are currently at, I see that you are doing exactly that: you are pointing to two subproofs, but not to any v statement.

In sum: I urge you to review the v Elim rule.