Nonetheless, I have a new explanation, and it is holding up so far, and it's quite simple and sweet if it's true.

Simpson-style S5 box and diamond are what you get if you say

[]A @ p = ∀a. A @ a

<>A @ p = ∃a. A @ a

and they're

*also*what you get if you say

[]A @ p = ∀a ≥ p. A @ a

<>A @ p = ∃a ≥ p. A @ a

*when*you axiomiatize ≥ with symmetry, transitivity, and reflexivity.I think this is why tom7 always thought S5 was fundamentally "natural" --- the "relative" system with an equivalence relation gives you the same logic as the "absolute" system that doesn't truck with a relation at all. In fact, therefore, we can see that any system that does anything with the relation is bound to prove fewer things than S5, since the relation only acts as a restriction, preventing some proofs from working. So S5 is a natural ceiling to what the general framework can represent.

So, I conjecture the following. I'm pretty sure it's right, but it would take some careful proving.

You get Pfenning-Davies S4 by introducing a positive linear atomic proposition "here", and working in focused linear logic (focalizing also the source language) and saying

[]N @ p = ∀a. here(a) -o N @ a

<>P @ q = ∃a. here(a) * P @ a

where []N is positive and <>P is negative in the source language, and translating all other propositions homomorphically pushing the world-argument through, and doing the shifts like this:

(↓N) @ p = here(p) -o (N @ p)

(↑P) @ q = here(q) * (P @ q)

And you

*also*get Pfenning-Davies S4 if you say

[]N @ p = ∀a ≥ p. here(a) -o N @ a

<>P @ q = ∃a ≥ q. here(a) * P @ a

*when*you axiomatize ≥ to have reflexivity and transitivity! Because of the way the here-atoms need to match up, adding symmetry to ≥ doesn't buy you anything. S4 is the natural ceiling here. Deeper conjecture: this is why tom7 and others searched in vain for a "Pfenning-Davies S5".

Also if this is right it puts to rest in my mind the sense in which [] and <> are dual to one another, (which is different from the way that [] and () are dual, because [] = FU while () = UF) namely that <> arises from changing negative ∀ to positive ∃, and negative -o to positive *.