= Solution
Write $E(x,y)$ for the displayed equality predicate. A6 and A4 give $\vdash E(x,x)$, establishing a <reflexive relation>.
An instance of A7, replacing just the first occurrence of $x$ in $E(x,x)$, is
$$
E(x,y)\to(E(x,x)\to E(y,x)).
$$
Assume $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 supplies
$$
E(y,z)\to(E(x,y)\to E(x,z)),
$$
by 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 gives
$$
\boxed{\vdash\forall x\,E(x,x),\quad\vdash\forall x\forall y(E(x,y)\to E(y,x)),\quad\vdash\forall x\forall y\forall z((E(x,y)\land E(y,z))\to E(x,z)).}
$$
Thus the predicate defines an <equivalence relation> within the calculus.
Back to article page
