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

Assume that every object fails

R

. A fresh existential witness for the premise then has both

R

and its negation. Eliminate the witness before closing the assumption about all objects:

Table 1.

Eliminate the witness inside the negation subproof

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

The conclusion is

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

(1)

The witness

v

occurs neither in the conclusion of existential elimination nor in its other open assumptions, so the eigenvariable condition holds.

Solution

 0  0

Choose an arbitrary fresh eigenvariable

v

. If

\neg R (v)

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

R (v)

by double-negation elimination, then generalize:

Table 1.

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) .

(1)

At the final universal introduction,

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.

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).