Is there anyone who could explain to me why these errors occur? It seems to me the rule was used properly.
1 Answer
Existential Elimination requires that the witness (a
) does not occur in the conclusion or in any undischarged assumptions.
At those points, you have an undischarged assumption that includes a
on line 2.
Suggestion: Place the negation introduction subproofs inside each case of the v-elimination subproofs.
| |_ Ex -Px
| | |_ -Pa
| | | |_ Pa & Qa
| | | | :