I am trying to work my way through this Fitch proof, and I am not sure what I am doing wrong, but I keep getting stuck no matter what I try.
Doing this as a fitch style proof is very tedious, but I get:
It would actually be faster to prove using the short-circuit method or a truth table.
Using the short circuit method,
Your first attempt is the best.
You were correct to use a conditional proof, and beginning with the assumption B->C. However it should be noticable that to derive the consequent you must introduce a negation. Indeed I can see you realised that, but why did you not see that the next thing to assume was A with intent to derive a contradiction?
| (A -> B) v C premise I |_ A -> ~C premise II | |_ B -> C assumed (for conditional proof) | | |_ A assumed (for negational proof) : : : : | | | # negation eliminated (hopefully) | | ~A negation introduced | (B -> C) -> ~A conditional introduced
Now one of your premises is A->~C, so we may immediately derive ~C in the context, and will have our contradiction if the other premise entails C under both assumptions.
Well, that other premise is a disjunction, which is eliminated using a proof by cases. Doing so will indeed derive C under each case (indeed it is trivial in one case).
So you must embed a proof by cases inside a proof of negation inside a conditional proof. And you will be done.
| (A -> B) v C premise I |_ A -> ~C premise II | |_ B -> C assumed (for conditional proof) | | |_ A assumed (for negational proof) | | | ~C conditional eliminated | | | |_ A -> B left case assumed : : : : : ... (It should be clear, what you need to do here.) | | | | C derived (hopefully) | | | (A -> B) -> C conditional introduced | | | |_ C right case assumed | | | C -> C conditional introduced | | | C disjunction eliminated | | | # negation eliminated | | ~A negation introduced | (B -> C) -> ~A conditional introduced
TL;DR Whenever you foresee that you will need to eliminate a disjunction, delay doing so for as many raised assumptions as you can. Try to build a mountain with two summits rather than two whole mountains.