Logical equality ($s=t$)

In first-order logic with logical equality, $s=t$ asserts that the terms denote the same domain element. Logical equality is interpreted as identity rather than as an arbitrary binary predicate. Its natural deduction rules include reflexivity and substitution: equal terms can replace one another in a first-order formula, subject to capture-avoiding substitution. Double-negating logical equality atoms in a Gödel-Gentzen negative translation preserves these rules when the transported translated first-order formula is stable.

Equal variables can replace selected free occurrences in a first-order formula if the inserted variable is not captured. Starting with atomic equality replacement, derive symmetry, then prove both replacement directions together by structural induction. Negation uses the reverse induction implication; implication uses both directions; a universal quantifier is handled by instantiation, replacement and generalization with a variable fresh for the equality assumptions. Bound occurrences are not replaced as free ones.

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.