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

Use the equality introduction rule to prove $t_1=t_1$. In the equality elimination rule, choose the first-order formula $\varphi (z)$ to be $z=t_1$. Substituting $t_2$ for $t_1$ in its first position proves symmetry:

Thus $\boxed{t_1=t_2⊢t_2=t_1}$. This uses only the two supplied equality rules; symmetry has not been assumed as an additional rule.