I'm frustrated that I'm able (I think, unless I made a mistake) to see by individual proofs that
classical Pfenning-Davies K = classical Simpson K
classical Pfenning-Davies T = classical Simpson T
classical Pfenning-Davies K4 = classical Simpson K4
classical Pfenning-Davies S4 = classical Simpson S4
but that each proof relies on individual insights about world graphs and expressions involving boxes and so on. I have a strong gut feeling that there's got to be a more systematic proof, but I can't find one, and I've currently run out of leads.
An intuition for why the proof is hard to systematize is that it's really close to false. If you make things intuitionistic, it's false. (see Rob's counterexample from the other day) If you add a first-order quantifier (at least if you do it the obvious way: see Barcan's formula) it's false. If you make things linear, it's false. (For □A & □B ⊢ □(A & B) holds in simpson but not pfenning-davies).
It leads me to suspect that the whole thing should hinge on the ambipolarity of nonlinear conjunction: because we're in a propositional, classical, nonlinear setting, it's kind of the only connective around, besides □, and the negation that's baked into the classical setting.
(Q: "What the heck do you mean by Pfenning-Davies K, T, K4?"
A: Well, the systematic way of determining what Pfenning-Davies X is from a set of axioms X about a Kripke-ish world accessibility relation is the paper I'm currently working with Sean on writing up. Specifically, however, S4 is actual Pfenning-Davies as it exists, K4 is what you get if you throw out the copy rule, T is what you get if the box-right rule erases all true hypotheses and also turns all valid hypothesis into merely true, and K is what you get if you do both of these things)