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