Past exam of the logic and set theory course of the University of Oxford / 2011 / A / 3 / c / i

Write $E(x,y)$ for the displayed equality predicate. A6 and A4 give $⊢E(x,x)$, establishing a reflexive relation.

An instance of A7, replacing just the first occurrence of $x$ in $E(x,x)$, isAssume $E(x,y)$, apply the modus ponens rule twice using reflexivity, and obtain $E(y,x)$. The deduction theorem for propositional logic discharges the assumption. This proves symmetry.

For transitivity, A7 suppliesby replacing $y$ in the atomic formula $E(x,y)$. From assumptions $E(x,y)$ and $E(y,z)$, two applications of the modus ponens rule give $E(x,z)$. Discharging assumptions and universally generalizing givesThus the predicate defines an equivalence relation within the calculus.