*some*time 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)