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.
    – user15247
    Aug 11, 2015 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, 2015 at 4:17
  • @hellyale I see someone created a tag for fitch! I was thinking a tag for LPL would be good.
    – user15247
    Aug 12, 2015 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, 2015 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.
    – user15247
    Aug 13, 2015 at 6:31

1 Answer 1


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.
    – user15247
    Aug 12, 2015 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, 2015 at 12:58
  • I cited the "~Tet(c) & ~Dodec(x)" line.
    – user15247
    Aug 13, 2015 at 6:32

You must log in to answer this question.