Solution (source code)

= Solution

\b[No such first-order axiom collection can force actual identity when the displayed symbol is treated as an ordinary relation.] The <duplication obstruction to axiomatizing identity> proves this even for an infinite collection of extra axioms.

Start with any nonempty <first-order structure> $\mathcal A$ in which the symbol is identity. Form $B=A\times\{0,1\}$ and the surjection $\pi:B\to A$. Interpret each relation by pulling it back along $\pi$; in particular,
$$
E^{\mathcal B}((a,i),(b,j))\iff a=b.
$$
Interpret every function on first coordinates as in $\mathcal A$ and choose second coordinate zero; likewise lift constants with second coordinate zero. Induction on <first-order terms> gives $\pi(t^{\mathcal B}(v))=t^{\mathcal A}(\pi v)$. Induction on <first-order formulas> then gives
$$
\mathcal B\models\theta[v]\iff\mathcal A\models\theta[\pi v].
$$
The quantifier steps use surjectivity of $\pi$, so every witness in $A$ lifts to $B$.

Every proposed axiom valid with actual equality is therefore true in $\mathcal B$ under every assignment, along with A1–A7. But $E^{\mathcal B}((a,0),(a,1))$ holds for two different domain elements. Thus those axioms cannot enforce identity. The usual interpretation of <logical equality> as identity is a semantic requirement.