Couldn't help myself and noodled around with that encoding over lunch again. It's beginning to look like I can get Pfenning-Davies-style and Simpson-style modalities in the same logic, mediated by a "Simpsonly true" sort of, um, metamodality. Why have Pfenning-Davies be the default and Simpson guarded by a propositional operator and not the other way around, you ask? Because the main difference between how the two logics are encoded is whether a certain equality between worlds is checked (namely: are you trying to perform an "untethered" decomposition at a world that is not equal to the "current" world?) and it seems like it works out to tag the world with a bit of data that, when present, collapses that equality relation. And, being the good intuitionist that I am, it's easy to learn new equalities as intuitionism-time advances, and seems weird and wrong to forget them. So, passing under a modality should collapse more things, and become more licentious and Simpson-y.