Premise: (Tet(a) ^ Tet(b)) v (Cube(c) ^ Cube(d))

Cube(c) -> Dodec(e)

Goal: ~Tet(a) -> Dodec(e)

Anyone have a clue on where to start with this?


I agree with Graham Kemp's "skeleton for the proof".

Rather than provide a skeleton, I will provide a completed proof but using a different proof checker. To make this work in the proof checker I renamed the statements.

enter image description here

You may not be able to use all of the inference rules as they are used here. I used conjunction elimination (∧E), contradiction introduction (⊥I), explosion (X), conditional introduction (→I), and disjunction elimination (∨E).

Klement's proof checker and information about the rules I used can be found in forall x referenced below.


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

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/

  • Thanks, I managed to understand what was going on and able to apply it! – user35766 Nov 14 '18 at 8:53

Clearly you want a Conditional Proof to prove that conditional. Assume ~Tet(a) aiming to derive Dodec(e).

Now look at the to premises and the assumption and ask: how may I derive Dodec(e) from that disjunction, conditional, and negation?

|  (Tet(a) ^ Tet(b)) v (Cube(c) ^ Cube(d))  Premise
|_ Cube(c) -> Dodec(e)                      Premise
|  |_ ~Tet(a)                               Assume
|  |  :
|  |  Dodec(e)                         
|  ~Tet(a) -> Dodec(e)                      Conditional Introduction

Your Answer

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