 Solution

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

Choose an arbitrary fresh eigenvariable

v

. If

\neg R (v)

held, existential quantifier introduction rule would contradict the premise. Derive

R (v)

An arbitrary object satisfies the relation

Line	Open assumptions	Formula	Justification
1	1	$\neg (\exists x \neg R (x))$	Premise
2	1, 2	$\neg R (v)$	Temporary assumption
3	1, 2	$\exists x \neg R (x)$	existential quantifier introduction rule 2; term $v$
4	1, 2	$⊥$	negation elimination rule 3, 1
5	1	$\neg\neg R (v)$	negation introduction 2, 4
6	1	$R (v)$	double-negation elimination 5
7	1	$\forall y R (y)$	universal introduction 6; fresh $v$

Hence

\forall y R (y) .

v

is free in no open assumption: the only remaining premise is the closed first-order formula

\neg\exists x \neg R (x)

. Thus the eigenvariable condition is satisfied. The passage from double negation to the positive relation uses the paper's classical rule.

 New to topics? Read the docs here!