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 (resit) / 8 / c

The equality introduction rule is reflexivity, with no premise. The equality elimination rule is substitution of equal first-order terms into a first-order formula:The indicated substitution must be capture-avoiding substitution in first-order logic: the first-order terms must be free for the replaced variable. One can designate a particular argument occurrence by choosing $\varphi (v)$ appropriately; the rule does not demand replacing every occurrence of an identical-looking term in a formula.

For transitivity of first-order equality, take $\varphi (v)$ to be $T_1=v$. The equality elimination rule applied to $T_2=T_3$ and $\varphi (T_2)$ givesFor symmetry of first-order equality, first obtain $T_1=T_1$ by the equality introduction rule. Now take $\psi (v)$ to be $v=T_1$ and substitute using $T_1=T_2$:These choices of formula show exactly which occurrence is replaced, so neither argument assumes the property it is establishing.

Choose fresh arbitrary eigenvariables $u,v$. Under $u=v$, use the equality elimination rule to transport $P(u)$ to $P(v)$. For the reverse direction, first derive $v=u$ by the symmetry derivation above. In full natural deduction form:All temporary assumptions are discharged before either universal quantifier introduction rule application, so both eigenvariable conditions hold. No premises remain: