= Solution
Apply the <negation introduction rule> to an assumed existential statement and the <existential quantifier elimination rule> with a fresh witness $u$:
$$
\begin{array}{rll}
1&\forall x\,\neg P(x)&\text{premise}\\
2&[\exists x\,P(x)]^a&\text{assumption}\\
3&\quad[P(u)]^b&\text{fresh witness assumption}\\
4&\qquad\neg P(u)&\forall E\ 1\\
5&\qquad\bot&\neg E\ 3,4\\
6&\quad\bot&\exists E\ 2,(3\text{--}5)\\
7&\neg\exists x\,P(x)&\neg I\ (2\text{--}6).
\end{array}
$$
The <eigenvariable condition> holds: $u$ is absent from the surrounding premise, the existential assumption and the exported conclusion $\bot$. Its local assumption is discharged before the final <negation introduction rule>.
$$
\boxed{\forall x\,\neg P(x)\vdash\neg\exists x\,P(x).}
$$
Back to article page
