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

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:

• 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? Commented May 26 at 12:58
• @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. Commented May 26 at 13:22

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.

• 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. Commented May 26 at 16:32
• @Bumble of course, thanks for pointing that out. Commented May 26 at 16:34
• @Bumble, what are KT and B? 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. 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.

Q.E.D.

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]

Q.E.D.

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]

Q.E.D.

Theorem 5; ◊ α= β ↔ α=β

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

Q.E.D.

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.

Q.E.D.

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

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