I am currently doing questions for my course from LPL Chapter 13.11. I have posted the screenshot of what I am trying to do. I am quite stuck and I can not think of a way to get to ~Tet(a). Any hint and help would be really appreciated.
When you introduce a new term
a, don't use a completely different term
b. You introduced it for a reason.
You appear to be trying rules at random hoping to hit on something. Examing the premises and target conclusions.
| Ax (Cube(x) v Tet(x)) Premise |_ Ex ~Cube(x) Premise | : | Ex Tet(x) Somehow
[Note: presumably the target should be
Ex Tet(x) because
Ex ~Tet(x) is not entailed by the premises. ]
Your premises are an existential and a universal of a disjunction and your target is another existential. That suggests some of the rules of inference you might need are Existential Elimination, Universal Elimination, Disjunction Elimination, and Existential Introduction.
| Ax (Cube(x) v Tet(x)) Premise |_ Ex ~Cube(x) Premise | |_ [a] ~Cube(a) Assumption | | Cube(a) v Tet(a) Universal Elimination | | : | | Tet(a) Disjunction Elimination | | Ex Tet(x) Existential Introduction | Ex Tet(x) Existential Elimination
Disjunction Elimination is a Proof by Cases: You require two subproofs, assuming in turn the left and right cases of the disjunction, and deriving the conclusion in each. In the right case it is trivial (the desired conclusion is the assumption). In the left case the assumption contradicts an earlier assumption, so you may use the principle of explosion (what your proof checker names "contradiction elimination").
1.| Ax (Cube(x) v Tet(x)) Premise 2.|_ Ex ~Cube(x) Premise 3.| |_ [a] ~Cube(a) Assumption 4.| | Cube(a) v Tet(a) Universal Elimination (1) 5.| | |_ Cube(a) Assumption 6.| | | # Contradiction Introduction (3,5) 7.| | | Tet(a) Contradiction Elimination (6) (ex falso quodlibet) 8.| | + 9.| | |_ Tet(a) Assumption 10.| | Tet(a) Disjunction Elimination (4,5-7,9-9) 11.| | Ex Tet(x) Existential Introduction (10) 12.| Ex Tet(x) Existential Elimination (2,3-11)
[ You should notice that the original conclusion
Ex ~Tet(x) just could not be reached from this point. If you assume Tet(a) and have no active contradictions, then ~Tet(a) cannot be derived. ]
So ends the lesson.