Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Created ternary frame, a class of models for substructural logic which are basically obtained from Day convolution for promonoidal posets. Presumably people who know things know this, but in a few minutes of looking I haven’t found anyone mentioning it. Girard’s “phase space” semantics for linear logic (no relation to phase spaces of physics) are just the special case of regarding a monoidal category as a promonoidal one.
I cleaned up ternary frame a bit, including adding some references (none of which I’ve read myself yet!). I still don’t quite understand the “compatibility relation” from the promonoidal/Day perspective.
That’s a nice point. I suppose you say “almost” because it amounts to if for all with , either or undefined. So it’s a kind of partial realizability?
Yeah, that’s what I had in mind by “almost”. I was wondering whether it could be made to coincide exactly by some trick, like introducing a formal bottom element and defining if it used to be undefined. Then iff either in the realizability sense or …
The way this is written a ternary frame is not just the de-categorified Day convolution, because the relation doesn’t satisfy the associativity (or unit?) condition of a promonoidal category. Shouldn’t this cause issues with the resulting semantics? E.g., is the semantics of the tensor products even associative? As written there’s not even an interpretation of unit as well, which would be the other missing part of a promonoidal category.
Isn’t this discussed on the page, in the section “from ternary frames to quantales”?
Not exactly. The page says “We can model logic using a ternary frame…” but to me this would imply that this is a model of substructural logic with e.g., associativity of tensor. And then later on it says you can add a bunch of things and then it would be a de-categorified Day convolution. The page doesn’t actually say that this is almost certainly what you actually want to do, since the model of logic doesn’t admit associativity of tensor.
I’m asking because I want to rewrite the page to be clearer in this regard and put the connection to Day convolution front and center but I want to make sure I’m not missing something about why it’s written the way it is.
I don’t think associativity of tensor is necessarily required in order to call something a “logic”.
For instance, couldn’t you have a “logic” for skew-monoidal categories?
There is indeed a sequent calculus for skew-monoidal categories.
Highlight that the most general version models non-associative non-unital substructural logic, and add a note about Day Convolution to the idea section.
How do I write the right to left version of ? doesn’t work in the sandbox.
1 to 14 of 14