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 '14 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 '14 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 '14 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 '14 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 '14 at 18:34

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.