= Solution
Use a fresh <existential witness> $v$. Within the assumption of the forbidden <universal quantification>, eliminate the original <existential quantification> to obtain <logical falsity>:
$$
\begin{array}{rll}
1&\exists x\,R(x)&\text{premise}\\
2&\vert\ \forall y\,\neg R(y)&\text{assumption}\\
3&\vert\ \vert\ R(v)&\text{witness assumption; }v\text{ fresh}\\
4&\vert\ \vert\ \neg R(v)&\forall\text{-elim }2\\
5&\vert\ \vert\ \bot&\neg\text{-elim }3,4\\
6&\vert\ \bot&\exists\text{-elim }1,3\text{--}5\\
7&\neg\forall y\,\neg R(y)&\neg\text{-intro }2\text{--}6
\end{array}
$$
The witness $v$ appears neither in the exported conclusion $\bot$ at line 6 nor in the other undischarged assumptions. The <existential quantifier elimination rule> is therefore valid, and
$$
\boxed{\exists x\,R(x)\ \vdash\ \neg\forall y\,\neg R(y).}
$$
Back to article page
