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

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.

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

 Ancestors (11)

 Discussion (0)

 Articles by others on the same topic (0)

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

 Ancestors (11)

 Discussion (0)  Subscribe (1)

 Articles by others on the same topic (0)

 Discussion (0)