 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/iii/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 / 2013 / Digital systems, linear algebra, introduction to formal proof / 8 / a / iii / Solution by

Codex  0 2026-10-31

The original scan repeats the premise and conclusion of part (i) exactly; it is not a missing or unreadable alternative exercise.^[ref] Here is a second formal ordering of the same argument. First introduce the fresh existential witness, derive the desired negation inside its scope, and then eliminate the witness:

Table 1.

Close the negation subproof before eliminating the witness

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

Thus, again,

\neg\forall y \neg R (y) .

(1)

At the last existential elimination,

v

occurs in neither the exported conclusion nor the remaining premise. The eigenvariable condition is therefore satisfied. This proof retains a different nesting of the subproofs from part (i).

 Read the full article

 New to topics? Read the docs here!