2

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.

Improve this question
4
  • 1
    I'm not sure that this is provable in system K. Kripke's identity postulate gives us (a=b) → □(a=b) but you are asking for the equivalent of ¬(a=b) → □¬(a=b). Suppose we assume ◇(a=b) → (a=b) is false, for the purposes of reductio. Then ◇(a=b) and ¬(a=b) hold at the actual world (@). So at some accessible PW (v), we have a=b. To get a contradiction, we would need @ to be accessible to v. So it seems we need symmetry or transitivity in our accessibility relation.
    – Bumble
    Sep 15 at 15:04
  • Thanks, I thought not. Oddly enough, treeproofgenerator.com has this as valid, so maybe they missed something.
    – PW_246
    Sep 15 at 18:04
  • 1
    Think in minute details you proved a=b→□(a=b) last time via substitution axiom but with a subtle unusual form in that substitution formula which is Fz :=□(x = z) which is unfortunately under the scope of box, it's a famous result in classical QML that number of planets of solar system is not necessarily greater than 7 insisted by Quine. Strictly speaking you can only substitute in atoms without modal scope. Now once you escape this classic restriction, then both your concerns are newly introduced rigid constants axioms per Kripke arriving ◊(a=b)→□(a=b). A posteriori is just possibility...
    – Double Knot
    Sep 15 at 23:48
  • As for the validity of your referenced prooftree, for simplicity it must use unrestricted subsititution axiom for equality for both classic QL and QML, thus effectively follows above said Kripkean rigid constants axioms embracing the controversial a posteriori necessity...
    – Double Knot
    Sep 16 at 21:34

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .