= Solution
Choose $v$ fresh. Here <double-negation elimination> is necessary to turn the <negation> of a possible counterexample into the positive statement:
$$
\begin{array}{rll}
1&\neg\exists x\,\neg R(x)&\text{premise}\\
2&\vert\ \neg R(v)&\text{assumption; }v\text{ fresh}\\
3&\vert\ \exists x\,\neg R(x)&\exists\text{-intro }2\\
4&\vert\ \bot&\neg\text{-elim }3,1\\
5&\neg\neg R(v)&\neg\text{-intro }2\text{--}4\\
6&R(v)&\neg\neg\text{-elim }5\\
7&\forall y\,R(y)&\forall\text{-intro }6
\end{array}
$$
The remaining context at line 7 contains no free $v$. The <universal quantifier introduction rule> therefore gives
$$
\boxed{\neg\exists x\,\neg R(x)\ \vdash\ \forall y\,R(y).}
$$
Back to article page
