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

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

ii

Extract the universally quantified logical implication and the existentially quantified logical conjunction from the premise. Use one fresh witness

a

for both conjuncts of the latter, so that the resulting

R (a)

and

\neg S (a)

concern the same object:

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