I have a system I worked out that predicts how a modal/substructural logic should look if you decide on a Kripke relation, and like I mentioned yesterday, its predictions don't line up with some modal logics Frank and Rowan have been talking about lately, which is really exciting. So I was hunting around for some other knob to turn or button to press on my encoding to accommodate this new logic.
And this morning I think I found it. The intuition comes out of remembering the fact that the plain ol' monad ◯A can be simulated in linear logic by (A → p) ⊸ p for an atom p. The judgment A lax on the right corresponds to the situation where you have a conclusion p, and a suspension A → p on the left. The correspondence of rules with their encoding looks like this:
|- A lax ----- |- ◯A becomes A → p |- p ------------------ |- (A → p) ⊸ p and |- A -------- |- A lax becomes ------ |- A p |- p ----------------- A → p |- p and A |- B lax ---------- ◯A |- B lax becomes A, B → p |- p ------------- ------ B → p |- A → p p |- p --------------------------- (A → p) ⊸ p, B → p |- p
To generalize this, we consider instead encoding ◯A as (A → p) ⊸ q for two different atoms p and q, and consider adding maybe p ⊸ q or q ⊸ p as axioms. If we add both, p and q are equivalent, and we're back to having the usual monad. The weird thing is that p ⊸ q is kind of like Kripke reflexivity, and without it, we lose A → ◯A. And conversely q ⊸ p is like Krikpe transitivity, and without it, we lose ◯◯A → ◯A.
The moral of the story is that if we want to construct a Pfenning-Davies-esque ◇, we have 4 different monadic mechanisms, (that are kind of like the necessity logics K, T, K4, and S4) and a fifth option of not using the monadic mechanism at all, and that these choices are orthogonal to our choice of the actual relation that the Krikpe mechanism interacts with. And there are at least four obvious distinct choices for that, which might again reasonably be called K, T, K4, and S4. And the fifth option of not using the Kripke mechanism at all, which gives us a more ◯-like operator rather than ◇.
So I think I have a nice 5x5 square of 25 disinct possibility/lax-ish modal operators, all of which satisfy cut, identity, and focusing-completeness theorems. Kind of an embarrassment of riches, since I only know of useful Curry-Howard interpretations of a few of them.