Is there anyone who could explain to me why these errors occur? It seems to me the rule was used properly.
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 | | | | :