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?

up vote 0 down vote accepted

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

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.

  • Thanks, I managed to understand what was going on and able to apply it! – J. Martinez Nov 14 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 acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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