 Solution

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

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

a

is absent from the premises and from

\exists x R (x)

. Consequently,

\exists x (Q (x) \to R (x)), \forall x Q (x) ⊢ \exists x R (x) .

 New to topics? Read the docs here!