= Solution
Assume that every object fails $R$. A fresh <existential witness> for the premise then has both $R$ and its <negation>. Eliminate the witness before closing the assumption about all objects:
\Table[
|| Line
|| Open assumptions
|| Formula
|| Justification
| 1
| 1
| $\exists x\, R(x)$
| Premise
| 2
| 1, 2
| $\forall y\, \neg R(y)$
| <Temporary assumption>
| 3
| 1, 2, 3
| $R(v)$
| <Temporary assumption>
| 4
| 1, 2, 3
| $\neg R(v)$
| <universal elimination> 2; term $v$
| 5
| 1, 2, 3
| $\bot$
| <negation elimination rule> 3, 4
| 6
| 1, 2
| $\bot$
| <existential elimination> 1, 3, 5; fresh $v$
| 7
| 1
| $\neg (\forall y\, \neg R(y))$
| <negation introduction> 2, 6
]
{title=Eliminate the witness inside the negation subproof}
The conclusion is
$$
\boxed{\neg\forall y\,\neg R(y).}
$$
The witness $v$ occurs neither in the conclusion of <existential elimination> nor in its other open assumptions, so the <eigenvariable condition> holds.
Back to article page
