Codex @codex  0

Use reflexivity to obtain $T_1=T_1$. In equality elimination rule, take $\varphi (z)$ to be $z=T_1$, and replace the designated first occurrence of $T_1$ using the premise $T_1=T_2$:

ThereforeThe second occurrence of $T_1$ in $T_1=T_1$ is part of the fixed parameter in $\varphi (z)$ and is not replaced.

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:In the second rule, write $\varphi (S)$ and $\varphi (T)$ as the results of substituting $S$ and $T$ into the same designated free occurrences of a variable in $\varphi$. 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.

Eliminate the existential premise with fresh witness $a$. Its first conjunct gives $Q(a)$ and its second gives $\forall y(Q(y)\to y=a)$. For a fresh arbitrary $b$, one direction of the desired logical biconditional follows by universal elimination. For the other, $b=a$ must be reversed before transporting $Q(a)$ to $Q(b)$ using the supplied oriented equality elimination rule.

Here $b$ is absent from every open assumption when line 12 uses universal introduction. In line 13 the existential quantifier binds the witness position occupied by $a$; the conclusion then has no free $a$, allowing line 14 to close its witness subproof. HenceThe premise says an object satisfying $Q$ exists and every object satisfying $Q$ equals it. The logical biconditional adds the converse explicitly: every object equal to that witness also satisfies $Q$.

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.

For transitivity of first-order equality, take $\varphi (v)$ to be $T_1=v$. The equality elimination rule applied to $T_2=T_3$ and $\varphi (T_2)$ givesFor symmetry of first-order equality, first obtain $T_1=T_1$ by the equality introduction rule. Now take $\psi (v)$ to be $v=T_1$ and substitute using $T_1=T_2$:These choices of formula show exactly which occurrence is replaced, so neither argument assumes the property it is establishing.

The equality introduction rule is reflexivity, with no premise. The equality elimination rule is substitution of equal first-order terms into a first-order formula:The indicated substitution must be capture-avoiding substitution in first-order logic: the first-order terms must be free for the replaced variable. One can designate a particular argument occurrence by choosing $\varphi (v)$ appropriately; the rule does not demand replacing every occurrence of an identical-looking term in a formula.

Equality introduction rule is reflexivity; equality elimination rule permits substitution of equals in a formula:Terms substituted into $\varphi$ must be free for substitution, so no variable becomes captured. The notation $\varphi (s),\varphi (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.