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 / 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