= Logical equality
{title2=$s=t$}
= First-order equality
{synonym}
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.
Back to article page
