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:


Doing this as a fitch style proof is very tedious, but I get:

enter image description here

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.


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

  • The 'short circuit method' you give is very helpful to understand why I have to start with assuming A at line 4., before assuming B. etc, in order to get to my conclusion. Thank you – 35308 Oct 30 '18 at 14:25

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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.