Jason (jcreed) wrote,

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

  • (no subject)

    Well I am certainly glad I saw Arrival so that I get the wug joke in http://languagelog.ldc.upenn.edu/nll/?p=29480#more-29480

  • (no subject)

    Saw "Arrival". It did have some nontrivial linguistics content, but it still felt kind of wrapped up in a discernible layer of Hollywood Woo. The…

  • (no subject)

    Had some dinner at Aliada with akiva and sasha and K, and afterwards saw Herzog's "Aguirre, the Wrath of God" in Socrates park. Enjoyably bleak.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 1 comment