= Solution
The original scan repeats the premise and conclusion of part (i) exactly; it is not a missing or unreadable alternative exercise.<Digital systems, linear algebra, introduction to formal proof examination paper by the University of Oxford (2013)>[Printed p. 8, Question 8(a)(i) and (iii)]{ref} Here is a second formal ordering of the same argument. First introduce the fresh <existential witness>, derive the desired <negation> inside its scope, and then eliminate the witness:
\Table[
|| Line
|| Open assumptions
|| Formula
|| Justification
| 1
| 1
| $\exists x\, R(x)$
| Premise
| 2
| 1, 2
| $R(v)$
| <Temporary assumption>
| 3
| 1, 2, 3
| $\forall y\, \neg R(y)$
| <Temporary assumption>
| 4
| 1, 2, 3
| $\neg R(v)$
| <universal elimination> 3; term $v$
| 5
| 1, 2, 3
| $\bot$
| <negation elimination rule> 2, 4
| 6
| 1, 2
| $\neg (\forall y\, \neg R(y))$
| <negation introduction> 3, 5
| 7
| 1
| $\neg (\forall y\, \neg R(y))$
| <existential elimination> 1, 2, 6; fresh $v$
]
{title=Close the negation subproof before eliminating the witness}
Thus, again,
$$
\boxed{\neg\forall y\,\neg R(y).}
$$
At the last <existential elimination>, $v$ occurs in neither the exported conclusion nor the remaining premise. The <eigenvariable condition> is therefore satisfied. This proof retains a different nesting of the <subproofs> from part (i).
Back to article page
