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 $x \Vdash P\multimap Q$ if for all $y$ with $y \Vdash Q$, either $(xy)\Vdash Q$ or $(xy)$ 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 $\bot$ and defining $x y = \bot$ if it used to be undefined. Then $x \Vdash P\multimap Q$ iff either $x \Vdash P \to Q$ in the realizability sense or $\bot \Vdash Q$…
1 to 5 of 5