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