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

  1. |SameRow(b,f)

  2. | ⊥ Ana Con 3,5

  3. |~Cube(f) ⊥Elim 6

(end subproof)

  1. |SameRow(c,f)

  2. | ⊥ ⊥Intro 2,8

  3. |~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.

  • $\begingroup$ Thanks! Hopefully it's clearer now. $\endgroup$
    – Alonninos
    Oct 3, 2014 at 18:24
  • $\begingroup$ I don't understand what the premises are. In any case the end of your proof is your goal, so it seems you proved what you wanted. $\endgroup$
    – Git Gud
    Oct 3, 2014 at 18:26
  • $\begingroup$ The proof's actually not done - I'm stuck in the middle. The premises are sentences 1-4 and then I've written the first two subproofs for the disjunct in premise 1. I'm a little stuck figuring out how to get ~Cube(f) for the SameRow(d,f) disjunct. $\endgroup$
    – Alonninos
    Oct 3, 2014 at 18:27
  • $\begingroup$ For that bit, assume $\text{Cube}(f)$, then you get $\text{SameRow}(d,f)\land \text{Cube}(f)$. $\endgroup$
    – Git Gud
    Oct 3, 2014 at 18:30
  • $\begingroup$ Ah, I see! Sometimes it's hard to know what to assume, but that makes so much sense. Thank you! $\endgroup$
    – Alonninos
    Oct 3, 2014 at 18:34

1 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)
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


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .