= Solution
<Equality introduction rule> is reflexivity; <equality elimination rule> permits substitution of equals in a formula:
$$
\boxed{\frac{}{\Gamma\vdash t=t}\ (=\mathrm I),\qquad\frac{\Gamma\vdash s=t\quad\Gamma\vdash\phi(s)}{\Gamma\vdash\phi(t)}\ (=\mathrm E).}
$$
Terms substituted into $\phi$ must be <free for substitution>, so no variable becomes captured. The notation $\phi(s),\phi(t)$ means substitution into the same designated free variable positions of one formula; other occurrences may remain fixed. These rules express <first-order equality> without assuming symmetry or transitivity as additional axioms.
Back to article page
