= Solution
Take a fresh arbitrary variable $a$. Assuming $R(a)$ would provide precisely the witness forbidden by the premise; discharge that assumption before <universal introduction>.
``
1. ¬∃x R(x) premise
2. R(a) assumption [i], a fresh
3. ∃x R(x) ∃I, 2
4. ⊥ ¬E, 1, 3
5. ¬R(a) ¬I, 2–4, discharging [i]
6. ∀y ¬R(y) ∀I, 5
``
At line 6, $a$ is free in no undischarged assumption: line 2 has already been discharged. The change of bound variable name is part of the universal-introduction instance.
Back to article page
