Stuck on First-Order Logic

Question

I'm taking a first-order logic class and I keep finding myself stuck on proofs that ask for disjunction elimination and then supply additional premises with conjunctions. How can I eliminate negations and conjunctions to get the premises I need to get consistent conclusions in disjunction elimination subproofs? Here's an example of something I'm working on:

(Goal: ~Cube(f))

1.| SameRow(b,f) v SameRow(c,f) v SameRow(d,f)

2.| ~SameRow(c,f)

3.| FrontOf(b,f)

4.| ~(SameRow(d,f) ∧ Cube(f))

5. |SameRow(b,f)

6. | ⊥ Ana Con 3,5

7. |~Cube(f) ⊥Elim 6

(end subproof)

8. |SameRow(c,f)

9. | ⊥ ⊥Intro 2,8

10. |~Cube(f) ⊥Elim 9

At this point I'm not sure what to do about the SameRow(d,f) part of the disjunct in premise 1. How do I use ~(SameRow(d,f) ∧ Cube(f)) to derive anything that I can use to reach ~Cube(f) in the last subproof? I get that the sentence is equivalent to ~SameRow(d,f) ∧ ~Cube(f), but I can't see how to get a contradiction from that.

Any help about this problem/strategy in general would be much appreciated! Thank you.

Answer 1

Thank you to Git Gud for the pointers! I needed to introduce a subproof assuming Cube(f) within the subproof for SameRow(d,f). The complete proof looks like this:

Goal: ~Cube(f)

1.|SameRow(b,f) v SameRow(c,f) v SameRow(d,f)
2.|~SameRow(c,f)
3.|FrontOf(b,f)
4.|~(SameRow(d,f) ^ Cube(f))
5.   |SameRow(b,f)
6.   |⊥   Ana Con 3,5
7.   |~Cube(f)   ⊥Elim 6
(end subproof)
8.   |SameRow(c,f)
9.   |⊥   ⊥Intro 2,8
10.  |~Cube(f)   ⊥Elim 9
(end subproof)
11.   |SameRow(d,f)
12.    |Cube(f)
13.    |SameRow(d,f) ^ Cube(f)   ^Intro 11, 12
14.    |⊥   ⊥Intro 4, 13
15.   |~Cube(f)   ~Intro 11-14
16.|~Cube(f)   VElim 1,5-7,8-10,11-14