I have been thinking about this question for a long time but didn't seem to make any progress. Here are the axioms of SQML:

Axioms of SQML

  • Why can't you just use NEC (which isn't generally true) to draw the conclusion immediately. If A then it's necessary that A. So if not (X=Y) then it's necessary that not (X=Y), by NEC? Or, is there an error in your expression of NEC, so that NEC should read it's necessary that A; therefore A?
    – lee pappas
    Commented May 26 at 12:58
  • 1
    @leepappas No you can't. NEC only sends p to ☐p but you cannot have p→☐p, since this is not generally true in SQML. I'm showing ⊢~a=b→☐~a=b, not {~a=b}⊢☐~a=b. Commented May 26 at 13:13
  • I don't know if this helps, but the denotation of symbols doesn't vary in time. Thus if not (a=b) then it's necessary that not (a=B), so it IS true, but I don't see that SQML is strong enough to derive it.
    – lee pappas
    Commented May 26 at 13:22

2 Answers 2


I’ll provide a sketch of the proof in SQML.

1. a=b→□(a=a)→□(a=b) II

2. □(a=a)            RX, NEC

3. a=b→□(a=b)        1,2 Prop. Logic

4. □(a=b→□(a=b))     3 NEC

5. ◊(a=b)→◊□(a=b)    4, system K theorem □(P→Q)→◊P->◊Q

6. ◊(a=b)→a=b        5, S5 theorem ◊□P→P, Prop. Logic

7. ¬(a=b)→□¬(a=b)    6, Prop. Logic, def ◊

As far as I can tell, this is the simplest method to prove it. I could be wrong, but I do not believe that ¬(a=b)→□¬(a=b) is a theorem of quantified S4 or other quantified modal systems not containing the B axiom. This is because, as Bumble pointed out, line 6 follows from line 5 in quantified KB, since ◊□P→P is the contrapositive of the B axiom.

  • 1
    Looks fine. You don't need S5 to get ◇□P → P, you only need KTB for that. In fact in general, if you have KT and B you can derive ⊢ □(P → □P) → (¬P → □¬P) which takes you straight from step 4 to 7.
    – Bumble
    Commented May 26 at 16:32
  • @Bumble of course, thanks for pointing that out.
    – PW_246
    Commented May 26 at 16:34
  • @Bumble, what are KT and B?
    – lee pappas
    Commented May 26 at 17:59
  • That is clear, thanks. By the way, the first line needs one more pair of brackets and the brackets around a=b are redundant. 5th line can be more explicit since I didn't quite get the twice contrapositive at first sight. Commented May 26 at 21:10
  • I’m using the common convention to bracket equalities under the scope of an operator and to drop brackets around chains of implications in a right-associative manner.
    – PW_246
    Commented May 26 at 21:40

How can I derive ~a=b→☐~a=b in SQML?

There's an alternative to RX and II, that allows you to prove this quickly, that I discovered recently. It's a modal logic version of Hao Wang's axiom of Identity.

Modal Logic Version of Hao Wang's axiom of Identity

∀y[Φ(y) iff ∃x[◊x=y ∧ Φ(x)]]

In a related thread I show how to use this axiom to prove the following substitution principle.

Substitution Principle

If ◊ α= β ∧ Φ(α) then Φ(β)

Which is Semantically equivalent to

◊ α= β → (Φ(α) → Φ(β))

I then show how to derive universal generalization.

Now the first goal is to prove RX.

Theorem 1: ∀y [◊y=y]

Define ∀z[Φ(z) iff ~(◊z=β)]

  1. Φ(β) iff ∃x[◊x=β ∧ Φ(x)]] [axiom, UI]
  2. Φ(β) iff ~(◊β=β) [Df]
  3. ~(◊β=β) iff ∃x[◊x=β ∧ Φ(x)] [1,2; rule of replacement]
  4. ~(◊β=β) [OSC1]
  5. ∃x[◊x=β ∧ Φ(x)]] [3,4; MP2]
  6. ◊x1=β ∧ Φ(x1) [5; EI]
  7. Φ(x1) iff ~(◊x1=β) [Df]
  8. ◊x1=β ∧ ~(◊x1=β) [6,7; RR]
  9. ~(◊β=β) → contradiction [4-8; CSC1]
  10. ◊β=β [9; RAA, DN]
  11. ∀y[◊y=y] [10; UG]

Q E.D.

Theorem 2: ∀z[z=z]

Proof found here.


Thus RX is proved.

Now let Φ(β) be ☐α=β in the substitution principle.

Theorem 3: ◊ α= β → α=β

  1. ◊ α= β → (☐α=α→ ☐α=β)
  2. α = α [Th.2]
  3. ☐α=α [2; NEC]
  4. ◊ α= β → ☐α=β [1,3; propositional calculus]
  5. ☐α=β → α=β [T]
  6. ◊ α= β → α=β [4,5; HS]


At this point you can prove your theorem quickly.

 1. ◊ a=b → a=b             [Th.3]
 2. ~☐~a=b →  a=b           [1; Df]    
 3. ~(a=B) → ☐~a=b          [2; transposition]

Theorem 4: P → ◊P

  1. ☐~P → ~P [T]
  2. ~~P → ~☐~P [1; transposition]
  3. P → ◊P [3; DN, Df]


Theorem 5; ◊ α= β ↔ α=β

  1. ◊ α= β → α=β [Th.3]
  2. α=β → ◊ α= β [Th.4]
  3. ◊ α= β ↔ α=β [1,2; conj, Df]


Theorem 5, and the rule of replacement allow you to prove II, from this system's substitution principle.

Theorem 6: α= β → (Φ(α) → Φ(β))

The proof is left to the reader.


This alternative to SQML, has one less axiom, and one less underived rule of inference. It's simpler than SQML.

  • 2
    That’s not even close to an argument.
    – PW_246
    Commented May 26 at 15:40

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .