How does one prove ‘(B→C)→¬A’ from ‘(A→B)∨C’ and ‘(A→¬C)’ in Fitch?

Question

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.

First attempt:

Second attempt:

Answer 1

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,

1. the conclusion is false when the left hand-side of (B -> C) -> ~A is TRUE but the right hand side is FALSE
2. So that means A would have be true TRUE for the conclusion to wind up false.
3. If A is true, then the first premise can only be true when C is FALSE.
4. If C is false, then the B must be FALSE for the left side of the conclusion to be TRUE.
5. If B is FALSE, then premise two turns into: ( TRUE -> FALSE) v FALSE --> FALSE or FALSE, so we cannot make both premises true and the conclusion false.

References

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

Answer 2

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.