 Solution

ID: 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/i/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:

Eliminate the witness inside the negation subproof

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	$⊥$	negation elimination rule 3, 4
6	1, 2	$⊥$	existential elimination 1, 3, 5; fresh $v$
7	1	$\neg (\forall y \neg R (y))$	negation introduction 2, 6

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

 New to topics? Read the docs here!