= Solution
Choose an <eigenvariable> $v$ fresh for the premise. Use the <existential quantifier introduction rule> to contradict the premise under a <temporary assumption> $R(v)$:
$$
\begin{array}{rll}
1&\neg\exists x\,R(x)&\text{premise}\\
2&\vert\ R(v)&\text{assumption; }v\text{ fresh}\\
3&\vert\ \exists x\,R(x)&\exists\text{-intro }2\\
4&\vert\ \bot&\neg\text{-elim }3,1\\
5&\neg R(v)&\neg\text{-intro }2\text{--}4\\
6&\forall y\,\neg R(y)&\forall\text{-intro }5
\end{array}
$$
At line 6 the assumption $R(v)$ has been discharged and the sole remaining premise has no free $v$, satisfying the <eigenvariable condition>. Thus
$$
\boxed{\neg\exists x\,R(x)\ \vdash\ \forall y\,\neg R(y).}
$$
Back to article page
