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

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