Jason (jcreed) wrote,
Jason
jcreed

I keep fiddling around with the logic/embedding thingy from yesterday, even though its relationship to BI is highly unclear... I know sometime in the deep past of mid-thesis times I set up a labelled deduction system where the labels existed over some monoid, but I think I understand the focusing consequences of that a lot better now.

Say your context is full of propositions at labels p that can be the identity, or a variable, or a (not necessarily commutative!) monoid operation or maybe some other function symbols:


I assume the monoid operation * is associative, and has unit e.

I'm going to need to lift the monoid operation to an action on contexts, but this is totally straightforward:



I then get two interesting modalities, one positive and one negative:


I seem to be forced into this ordering by considering the general case where * is not commutative. I kind of expected modalities to synchronously demand stuff be pulled off the same end that they put it on, but they don't --- they insert and delete at opposite ends of monoid expressions. Maybe this is another shadow of whatever phenomenon makes queue logic happen instead of stack logic?

Anyway I am pretty sure the circle operation I'd been talking about up until now is this box-plus, and the filled-circle I want is box-minus. The plain old conjunction and disjunction and units don't do anything interesting here; they just propagate (or allow) all labels. But implication takes just a little bit of care:


Although I'm writing contexts as Γ and Δ, I still understand contraction and weakening to be implicitly allowed. I just have to do a context merge in implies-left because one of the contexts gets hit with a [p *], while the other doesn't.

Here's what identity and cut:


And here's the encodings of tensor and its right adjoint that I think are correct for some value of "correct":





(full image here)
Tags: bunched, logic, math
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 

  • 1 comment