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 , replace the domain by and pull all relations back along the projection . Lift functions so that commutes with them. Induction on first-order formulas preserves satisfaction because 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.

Articles by others on the same topic (0)

There are currently no matching articles.