Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Digital systems, linear algebra, introduction to formal proof / 8 / a / ii / 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:

HenceAt 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.