= Solution
The two proofs differ in whether <existential elimination> is outside or inside <negation introduction>. For the first proof, choose fresh $a$, derive the negation inside the witness subproof, and then discharge the witness:
$$
\begin{array}{rll}
1&\exists x\,\neg P(x)&\text{premise}\\
2&\quad\neg P(a)&\text{fresh witness assumption}\\
3&\qquad\forall y\,P(y)&\text{assumption}\\
4&\qquad P(a)&\forall E\ 3\\
5&\qquad\bot&\neg E\ 4,2\\
6&\quad\neg\forall y\,P(y)&\neg I\ 3\text{--}5\\
7&\neg\forall y\,P(y)&\exists E\ 1,2\text{--}6
\end{array}
$$
The conclusion at line 6 contains no free $a$. For the second proof, open the universal assumption first, eliminate the existential to derive falsity, and then discharge the universal assumption:
$$
\begin{array}{rll}
1&\exists x\,\neg P(x)&\text{premise}\\
2&\quad\forall y\,P(y)&\text{assumption}\\
3&\qquad\neg P(a)&\text{fresh witness assumption}\\
4&\qquad P(a)&\forall E\ 2\\
5&\qquad\bot&\neg E\ 4,3\\
6&\quad\bot&\exists E\ 1,3\text{--}5\\
7&\neg\forall y\,P(y)&\neg I\ 2\text{--}6
\end{array}
$$
At line 6 of the second proof, neither the exported conclusion $\bot$ nor the other open assumptions contains $a$ free, satisfying the <eigenvariable condition>. Neither proof needs RAA or <double-negation elimination>.
Back to article page
