A theory of identity between terms according to which that $s=t$ entails that it is necessary that $s=t$ for two referring terms $s$ and $t$. Logics that have necessary identity formalize this thesis by the inference rule:

Such accounts are counter to modal logics with contingent identity, in which for terms $s,t$, $s=t$ may be true at one world $w$ and false at another.