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

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:

The conclusion isThe witness $v$ occurs neither in the conclusion of existential elimination nor in its other open assumptions, so the eigenvariable condition holds.

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:

HenceAt 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:

Thus, again,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).

The equality introduction rule is reflexivity: any well-formed first-order term is equal to itself, with no premises. The equality elimination rule permits replacement of equals in a first-order formula:In the second rule, write $\varphi (S)$ and $\varphi (T)$ as the results of substituting $S$ and $T$ into the same designated free occurrences of a variable in $\varphi$. Both substitutions must avoid variable capture. The rule preserves the surrounding assumptions. This expresses first-order equality rather than treating equality as an arbitrary relation symbol.

Use reflexivity to obtain $T_1=T_1$. In equality elimination rule, take $\varphi (z)$ to be $z=T_1$, and replace the designated first occurrence of $T_1$ using the premise $T_1=T_2$:

ThereforeThe second occurrence of $T_1$ in $T_1=T_1$ is part of the fixed parameter in $\varphi (z)$ and is not replaced.

Introduce a fresh existential witness $v$ with $R(v)$. The universal premise gives $v=0\vee v=1$. In the first case, equality elimination rule gives $R(0)$. In the second, it gives $R(1)$, contradicting $\neg R(1)$; explosion then supplies the common case conclusion $R(0)$. Close both cases and then the witness scope:

HenceFor both uses of equality elimination rule, the formula template is $R(z)$. At the final existential elimination, $v$ is fresh in all three original premises and absent from $R(0)$, so the eigenvariable condition holds. No additional assumption that the constants $0$ and $1$ denote distinct objects is needed.