Hot dang I'm trying to be cautiously optimistic here, because the last several times I thought I finally figured out What The Deal Was with the two big notions of intuitionistic modal logic [] and (i.e. "Pfenning-Davies style" vs. "Simpson-style") relative to each other, I turned out to be wrong. 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... read more
