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.
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.
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/
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