I am working on proving the following question:

| ∀x [Dodec(x) → LeftOf(x, a)]
| ∀x [Tet(x) → RightOf(x, a)]
| ∀x [SameCol(x, a) → Cube(x)]

The question has the following rules:

[…] give a proof that uses Ana Con but only where the premises and conclusions of the citation are literals (including ⊥). You may use Taut Con but do not use FO Con in any of the proofs.

I have completed the following two proofs, but neither are accepted by the program, because it is being very picky on Ana Con:

Proof 1: Attempt 1

Proof 2: Attempt 2

However, I can't think of any other way to prove this that would make the program happy. What other methods could I try?

  • Ana Con refers to at most 1 other line. The first two, in both proofs, refer only to the corresponding row with [c]. The 3rd Ana Con, in the first proof, refers to nothing. The very last one, Cube(c), refers only to the line above it.
    – zagadka314
    Aug 11 '15 at 20:49
  • Use V Intro on the line ~Tet(c) ^ ~Dodec(c) to make it ~Tet(c) ^ ~Dodec(c) V Cube(c) then Ana Con will work I think. Fitch can be tricky though, if that doesn't work can you host your proof file? I still have fitch from years ago.
    – hellyale
    Aug 12 '15 at 4:17
  • @hellyale I see someone created a tag for fitch! I was thinking a tag for LPL would be good.
    – zagadka314
    Aug 12 '15 at 8:14
  • The fitch tag already existed. I'd add a LPL tag but I haven't really seen a lot of LPL questions on here.
    – hellyale
    Aug 12 '15 at 13:00
  • @hellyale Someone added the fitch tag after I requested it in a previous question. If you click on the tag, only my questions have that tag.
    – zagadka314
    Aug 13 '15 at 6:31

These are the rules you need to cite, ignore my comment, a disjunction introduction is not necessary. I was thinking it was of the form A V B not A ^ B. enter image description here

  • 1
    Worked perfectly. Fitch is very very picky. It rejected another question because I used [b] and the book wanted me to use [c], even though it really didn't matter. All the premises contained only variables.
    – zagadka314
    Aug 12 '15 at 8:12
  • @zagadka314 yes it also doesn't like b ^ a when it expects a ^ b. Curious, what steps did you have cited originally?
    – hellyale
    Aug 12 '15 at 12:58
  • I cited the "~Tet(c) & ~Dodec(x)" line.
    – zagadka314
    Aug 13 '15 at 6:32

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.