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 / b

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.