I originally posted this on math.stackexchange.com, but I’m cross-posting it since I know there are good modal logicians on here too.
Also, I already asked a similar question here: Identity in Quantified Modal Logic, but the answer to it does not address my specific question.
One can prove that a=b → □(a=b) by using the substitution axiom for equality. However, since ¬(a=b) is not of the form α=γ, I don’t see how to prove ◊(a=b) → a=b, even though I know it’s valid in most modal logics. Is the substitution [a=b/¬(a=b)] actually the correct way to prove it, or am I missing something?
I am able to prove this in quantified S5, but it’s valid in system K. Any help would be appreciated.