= Solution
Choose an arbitrary fresh <eigenvariable> $v$. If $\neg R(v)$ held, <existential quantifier introduction rule> would contradict the premise. Derive $R(v)$ by <double-negation elimination>, then generalize:
\Table[
|| Line
|| Open assumptions
|| Formula
|| Justification
| 1
| 1
| $\neg (\exists x\, \neg R(x))$
| Premise
| 2
| 1, 2
| $\neg R(v)$
| <Temporary assumption>
| 3
| 1, 2
| $\exists x\, \neg R(x)$
| <existential quantifier introduction rule> 2; term $v$
| 4
| 1, 2
| $\bot$
| <negation elimination rule> 3, 1
| 5
| 1
| $\neg \neg R(v)$
| <negation introduction> 2, 4
| 6
| 1
| $R(v)$
| <double-negation elimination> 5
| 7
| 1
| $\forall y\, R(y)$
| <universal introduction> 6; fresh $v$
]
{title=An arbitrary object satisfies the relation}
Hence
$$
\boxed{\forall y\,R(y).}
$$
At the final <universal introduction>, $v$ is free in no open assumption: the only remaining premise is the closed <first-order formula> $\neg\exists x\,\neg R(x)$. Thus the <eigenvariable condition> is satisfied. The passage from double <negation> to the positive relation uses the paper's classical rule.
Back to article page
