Oops! Somehow I failed to consider S5 yesterday, which immediately…: jcreed

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 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".

(no subject)

(no subject)

(no subject)

Error