Делать это в качестве доказательства в стиле fitch очень утомительно, но я получаю:

На самом деле было бы быстрее доказать, используя метод короткого замыкания или таблицу истинности.

Используя метод короткого замыкания,

1. заключение ложно, когда левая часть (B -> C) -> ~A ИСТИНА, а правая часть ЛОЖЬ
2. Таким образом, это означает, что А должно быть ИСТИННЫМ, чтобы вывод оказался ложным.
3. Если А истинно, то первая посылка может быть истинна только тогда, когда С ЛОЖНО.
4. Если C ложно, то B должно быть ЛОЖНО, чтобы левая часть вывода была ИСТИНА.
5. Если B ЛОЖЬ, то посылка два превращается в: (ИСТИНА -> ЛОЖЬ) v ЛОЖЬ --> ЛОЖЬ или ЛОЖЬ, поэтому мы не можем сделать обе посылки истинными, а вывод ложным.

использованная литература

Редактор и средство проверки естественной дедукции Кевина Клемента на JavaScript/PHP в стиле Fitch http://proofs.openlogicproject.org/

Твоя первая попытка самая лучшая.

Вы правильно использовали условное доказательство и начали с предположения B->C. Однако следует заметить, что для получения следствия необходимо ввести отрицание. В самом деле, я вижу, что вы это поняли, но почему вы не заметили, что следующей вещью, которую нужно было принять, было А с намерением вывести противоречие?

|  (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

Теперь одна из ваших посылок — это А->~С, поэтому мы можем немедленно вывести ~С в контексте и получим противоречие, если другая посылка влечет за собой С при обоих предположениях.

Ну, а другая посылка есть дизъюнкция, которая устраняется с помощью доказательства по падежам. Это действительно приведет к получению C в каждом случае (действительно, в одном случае это тривиально).

Таким образом, вы должны встроить доказательство по случаям внутри доказательства отрицания внутри условного доказательства. И вы будете сделаны.

|  (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 Всякий раз, когда вы предвидите, что вам нужно будет устранить дизъюнктуру, отложите это до максимально возможного количества выдвинутых предположений. Попробуйте построить гору с двумя вершинами, а не с двумя целыми горами.