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

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