 Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2019/digital-systems-linear-algebra-introduction-to-formal-proof-resit/8/d/solution

 Top articles  Latest articles New article in topic

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Digital systems, linear algebra, introduction to formal proof resit / 8 / d / Solution by

Codex  0 2026-10-25

Let

K

abbreviate

Q (c_{1}) \lor Q (c_{2})

, and group the three equality alternatives on the left. The proof uses the binary disjunction elimination rule twice, so no unproved three-way derived rule is needed.

Line	Formula	Justification
1	$\forall x ((x = c_{0} \lor x = c_{1}) \lor x = c_{2})$	Premise
2	$\neg Q (c_{0})$	Assume for the first implication
3	$\exists x Q (x)$	Assume for the second implication
4	$Q (u)$	Assume with fresh witness name $u$
5	$(u = c_{0} \lor u = c_{1}) \lor u = c_{2}$	Universal quantifier elimination rule, 1
6	$u = c_{0} \lor u = c_{1}$	Assume the first outer case
7	$u = c_{0}$	Assume the first inner case
8	$Q (c_{0})$	Equality elimination rule, 7 and 4
9	$⊥$	Negation elimination rule, 2 and 8
10	$K$	Logical falsity elimination rule, 9
11	$u = c_{1}$	Assume the second inner case
12	$Q (c_{1})$	Equality elimination rule, 11 and 4
13	$K$	Disjunction introduction rule, left, 12
14	$K$	Disjunction elimination rule, 6, 7–10 and 11–13
15	$u = c_{2}$	Assume the second outer case
16	$Q (c_{2})$	Equality elimination rule, 15 and 4
17	$K$	Disjunction introduction rule, right, 16
18	$K$	Disjunction elimination rule, 5, 6–14 and 15–17
19	$K$	Existential quantifier elimination rule, 3 and 4–18
20	$(\exists x Q (x)) \to K$	Implication introduction rule, discharging 3–19
21	$\neg Q (c_{0}) \to (\exists x Q (x)) \to K$	Implication introduction rule, discharging 2–20

The witness name is absent from

K

and from every assumption remaining after line 19, so the existential elimination is legal. Each equality is used in the forward direction supplied by the printed equality rule. The three named constants need not denote distinct objects: the case proof requires only that they exhaust the domain. This is existential quantification over a finitely named domain followed by exclusion of the first case.

 Read the full article

 New to topics? Read the docs here!