# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorMike Shulman
• CommentTimeMay 15th 2012

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.

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeDec 19th 2017

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.

• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeMay 24th 2018

Added a note about how regarding PCAs as ternary frames almost recovers the notion of implication from realizability.

• CommentRowNumber4.
• CommentAuthorSam Staton
• CommentTimeMay 24th 2018

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?

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeMay 24th 2018

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$