One can prove that $a=b \to \Box a=b$ by using the substitution axiom for equality. However, since $\neg a=b$ is not of the form $\alpha_1 =\alpha_2$, I don’t see how to prove $\Diamond a=b \to a=b$, even though I know it’s valid in most modal logics. Is the substitution $[a=b/\neg a=b]$ actually the correct way to prove it, or am I missing something?
I am able to prove this in quantified $ \sf S5$, but it’s valid in system $\sf K$. Any help would be appreciated.
Edit I already asked a similar question here: https://philosophy.stackexchange.com/questions/98888/identity-in-quantified-modal-logic, but the answer doesn’t specifically answer my current question.