 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/c/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 / c / Solution by

Codex  0 2026-10-25

For readability write

R (s, t)

for the uninterpreted relation

s ∋ t

. In the first proof, introduce the universal quantifier inside the existential witness scope:

Line	Formula	Justification
1	$\exists y \forall x R (x, y)$	Premise
2	$\forall x R (x, w)$	Assume with fresh witness name $w$
3	$R (u, w)$	Universal quantifier elimination rule, 2; choose fresh arbitrary $u$
4	$\exists y R (u, y)$	Existential quantifier introduction rule, 3
5	$\forall x \exists y R (x, y)$	Universal quantifier introduction rule, 4; $u$ is absent from open assumptions
6	$\forall x \exists y R (x, y)$	Existential quantifier elimination rule, 1 and 2–5

In the second proof, first close the witness scope and then generalize the arbitrary object:

Line	Formula	Justification
1	$\exists y \forall x R (x, y)$	Premise; choose $u$ arbitrary and fresh for this premise
2	$\forall x R (x, w)$	Assume with fresh $w$ , also different from $u$
3	$R (u, w)$	Universal quantifier elimination rule, 2
4	$\exists y R (u, y)$	Existential quantifier introduction rule, 3
5	$\exists y R (u, y)$	Existential quantifier elimination rule, 1 and 2–4
6	$\forall x \exists y R (x, y)$	Universal quantifier introduction rule, 5

These are distinct proof trees: the final two rule applications are interchanged, and their freshness conditions have been checked in their respective contexts. They express the quantifier order and uniform witness principle: a single witness working for every object also supplies a witness for each object individually.

The converse is not valid. In a domain

{0, 1}

interpret

R (s, t)

as equality of its arguments. Every object has a witness, namely itself, but no one object equals both 0 and 1. The premise of the converse is true and its conclusion false. The symbol

∋

is an arbitrary binary relation here; no set-membership axioms may be imposed on it without an additional premise.

 Read the full article

 New to topics? Read the docs here!