- Box is still straightforwardly "for all future worlds".
- Upshift is still frame-parameterized double-negation,
↑P @ w = ∀φ.(P @ w → #(φ, w)) → #(φ, w)
This is what achieves the "tethering" effect of Pfenning Davies.
- Diamond is a variant of this:
◇P @ w = ∀φ.w ≥ φ → (∀v ≥ w. P @ v → #(φ,v)) → #(φ, w)
The tricksy thing I am doing is assuming there is an inclusion from frames (e.g. the φ that is quantified over) into Kripke worlds (e.g. the v, w) so that I can compare them in that w ≥ φ there.
The punchline is that I should be able to vary the axiomatization of ≥ from no axioms to just refl to just trans to refl and trans, and I think I get out weather-report K, T, K4, and S4, respectively.