First order logic (is gay)

I'm doing exercise 6.12 in Language Proof and Logic, Barwise and Etchemendy and basically, I dunno how to do it. I have to prove "Dodec(f)" from the premises at the top. My problem is where I've used "taut con" - basically that's cheating, but I duno what other rule to use.

Basically, I should be able to prove any statement once I have a contradiction, but I don't know what rule to use for this. I need Dodec(f) at the end of my three subproofs, as that seems to be the only way to eliminate a disjunction.

Reply 1

Kolya

17

Hathlan

.

Your attachment is broken (at least for me).

OP

Does this work?

Apologies for crashing into this thread .. but could you please tell me what this interesting-looking software is, and why 'Fitch'?

Reply 4

Kolya

17

Hathlan

Does this work?

Yep.

If you want to avoid using 'Taut con', you can use negation_introduction instead. i.e. in your subproof which starts "¬Dodec(e)", introduce another subproof with the premise "¬Dodec(f)", do the same contradiction_introduction as before, and then exit the subproof and use negation introduction to give you "¬¬Dodec(f)".

That process is what "Taut Con" packs up. If you have a contradiction and want to derive anything, say P, just stick the contradiction in a subproof with the premise ¬P and s'all good.

Reply 5

Hathlan

OP

2

Kolya

Yep.

If you want to avoid using 'Taut con', you can use negation_introduction instead. i.e. in your subproof which starts "¬Dodec(e)", introduce another subproof with the premise "¬Dodec(f)", do the same contradiction_introduction as before, and then exit the subproof and use negation introduction to give you "¬¬Dodec(f)".

That process is what "Taut Con" packs up. If you have a contradiction and want to derive anything, say P, just stick the contradiction in a subproof with the premise ¬P and s'all good.