Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof / 8

A variable $v$ is fresh for the surrounding context $\Gamma$ when it does not occur free in any undischarged assumption in $\Gamma$. Choose it also distinct from bound variables that would cause variable capture in the intended substitution. The universal quantifier introduction rule isIts justification is that the logical derivation of $\varphi (v)$ used no special information about $v$, so it establishes the property of an arbitrary object. Semantically, changing the assignment of $v$ preserves the truth of $\Gamma$; therefore $\varphi (v)$ holds for every possible assigned object. Without the eigenvariable condition, the assumption $R(v)$ could incorrectly be generalized to $\forall xR(x)$ in an interpretation where only one of two objects satisfies $R$.

Choose an eigenvariable $v$ fresh for the premise. Use the existential quantifier introduction rule to contradict the premise under a temporary assumption $R(v)$:At line 6 the assumption $R(v)$ has been discharged and the sole remaining premise has no free $v$, satisfying the eigenvariable condition. Thus

Choose $v$ fresh. Here double-negation elimination is necessary to turn the negation of a possible counterexample into the positive statement:The remaining context at line 7 contains no free $v$. The universal quantifier introduction rule therefore gives

Use a fresh existential witness $v$. Within the assumption of the forbidden universal quantification, eliminate the original existential quantification to obtain logical falsity:The witness $v$ appears neither in the exported conclusion $\perp$ at line 6 nor in the other undischarged assumptions. The existential quantifier elimination rule is therefore valid, and

The premise limits every possible existential witness to the objects named by $c_0,c_1$; it does not assert that these constants name distinct objects. Instantiate it at a fresh witness $v$, then apply disjunction elimination. In the first case equality elimination rule transfers $R(v)$ to $R(c_0)$; in the second it transfers $R(v)$ to $R(c_1)$, contradicting the assumed negation. The full natural deduction derivation isThe sibling case subproofs end before the witness subproof closes. At line 13, $v$ is absent from $R(c_0)$ and from all surrounding assumptions, so no witness escape occurs. The final two applications of implication introduction giveThe logical falsity elimination rule is needed to complete the contradictory second case with the same conclusion as the first case.