Jason (jcreed) wrote,
Jason
jcreed

There's this story I've been trying to sell to myself and occasionally to others that Pfenning-Davies ◇ actually has two aspects, or, if you like, two "mechanisms" that it uses. One is tangled up with the Kripke relation: it's the existential quantifier over Kripke worlds, which is the mechanism dual to the □'s universal quantifier. The other mechanism is the "monadic" mechanism, which is the thing that requires "poss" to already be on the right when you use the left rule. The reason I call this monadic is because of its similarity to the fact that you need "lax" on the right to discharge a ◯ on the left.

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.
Tags: logic, math, modal
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 6 comments