### (no subject)

Oops! Somehow I failed to consider S5 yesterday, which immediately breaks even the classical PD = classical simpson equivalence. Simpson S5 proves A ⊢ □⋄A, like you'd expect, but Pfenning-Davies S5 doesn't, and I've known this for a long time. It's "not really very S5ish after all". The □L/⋄R rules, the ones that synchronously let you

So there's a handful of very heavily restricted (classical, propositional, nonlinear, asymmetric) PD logics that are equivalent to a handful of Simpson logics. That's all I got. No proof of any systematic relationship, and now I don't have a guess how I would even formulate a conjecture of one. Because "asymmetric" as a condition on a collection of axioms about ≤ is horrifyingly negationy and it makes the constructivist in me go ewww.

Anyway, quite a weird situation. This is the most fragile result I've seen since Dyckhoff's contraction-free calculi.

---

Hmm. A possible way forward is straitjacketing Simpson to be just as "asymmetric" as Pfenning-Davies is. Where Simpson says

(□A) @ t = ∀x≥t. (A @ x)

[which is just an abbreviated way of saying

(□A) @ t = ∀x. (x≥t) ⇒ (A @ x)]

I could instead say

(□A) @ t = ∀x. (x≥t) ⇒ (x⊒t) ⇒ (A @ x)

Where ≥ remains the accessibility relation defined by some "user-chosen" axioms, and ⊒ is a relation axiomatized by reflexivity and transitivity, which seems to be somehow the natural limit of the Pfenning-Davies mechanism the same way that S5 (i.e. refl, trans, and symmetry) is of the Simpson mechanism.

So if I redo Simpson with that definition, then this classical, propositional, nonlinear variant-simpson coincides with classical PD for all the kripke-axiom-sets I can think of right now, and coincides with real-simpson for any axiomatization that is implied by refl and trans.

Still no closer to any idea of how to prove this "internally".

*choose*a world, have a Model-T-color-selection quality in that you can choose any modal world you want, as long as it's the*current*world. So unless you can actually*transport*yourself back to the world at which the A was hypothesized (and you can't: □R/⋄L are the only rules that transport, and they transport you to fresh worlds) you can't use it.So there's a handful of very heavily restricted (classical, propositional, nonlinear, asymmetric) PD logics that are equivalent to a handful of Simpson logics. That's all I got. No proof of any systematic relationship, and now I don't have a guess how I would even formulate a conjecture of one. Because "asymmetric" as a condition on a collection of axioms about ≤ is horrifyingly negationy and it makes the constructivist in me go ewww.

Anyway, quite a weird situation. This is the most fragile result I've seen since Dyckhoff's contraction-free calculi.

---

Hmm. A possible way forward is straitjacketing Simpson to be just as "asymmetric" as Pfenning-Davies is. Where Simpson says

(□A) @ t = ∀x≥t. (A @ x)

[which is just an abbreviated way of saying

(□A) @ t = ∀x. (x≥t) ⇒ (A @ x)]

I could instead say

(□A) @ t = ∀x. (x≥t) ⇒ (x⊒t) ⇒ (A @ x)

Where ≥ remains the accessibility relation defined by some "user-chosen" axioms, and ⊒ is a relation axiomatized by reflexivity and transitivity, which seems to be somehow the natural limit of the Pfenning-Davies mechanism the same way that S5 (i.e. refl, trans, and symmetry) is of the Simpson mechanism.

So if I redo Simpson with that definition, then this classical, propositional, nonlinear variant-simpson coincides with classical PD for all the kripke-axiom-sets I can think of right now, and coincides with real-simpson for any axiomatization that is implied by refl and trans.

Still no closer to any idea of how to prove this "internally".