= Solution
The <equality introduction rule> is reflexivity: any well-formed <first-order term> is equal to itself, with no premises. The <equality elimination rule> permits replacement of equals in a <first-order formula>:
$$
\boxed{\frac{}{T=T}\;{=I},\qquad\frac{S=T\qquad\phi(S)}{\phi(T)}\;{=E}.}
$$
In the second rule, write $\phi(S)$ and $\phi(T)$ as the results of substituting $S$ and $T$ into the same designated free occurrences of a variable in $\phi$. Both substitutions must avoid variable capture. The rule preserves the surrounding assumptions. This expresses <first-order equality> rather than treating equality as an arbitrary relation symbol.
Back to article page
