Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Digital systems, linear algebra, introduction to formal proof / 8 / b / i

The existential premise is

\exists x (Q (x) \to R (x))

, with the logical implication inside the existential quantifier. Eliminate it using a fresh witness

a

, specialize

\forall x Q (x)

to that same witness, and introduce the required existential quantifier before closing the witness subproof:

Line	Context	Formula	Justification
1	${1}$	$\exists x (Q (x) \to R (x))$	Premise
2	${1, 2}$	$\forall x Q (x)$	Premise
3	${1, 2, 3}$	$Q (a) \to R (a)$	Temporary assumption
4	${1, 2, 3}$	$Q (a)$	universal elimination $\forall -elim$ on 2; instantiate at $a$
5	${1, 2, 3}$	$R (a)$	implication elimination rule $\to -elim$ on 3, 4
6	${1, 2, 3}$	$\exists x R (x)$	existential quantifier introduction rule $\exists -intro$ on 5; witness $a$
7	${1, 2}$	$\exists x R (x)$	existential quantifier elimination rule $\exists -elim$ on 1, 6; discharge 3; $a$ fresh