= Duplication obstruction to axiomatizing identity
When an equality-like symbol is treated as an ordinary binary predicate, no <first-order theory> consisting of assertions valid for actual identity can force it to be identity. Given a genuine-equality structure on $A$, replace the domain by $A\times\{0,1\}$ and pull all relations back along the projection $\pi$. Lift functions so that $\pi$ commutes with them. Induction on <first-order formulas> preserves satisfaction because $\pi$ is surjective. Yet the two copies of each point satisfy the equality-like predicate. Thus actual identity must be part of the semantics, or the resulting equivalence classes must be quotiented out.
Back to article page
