Hi, Robert. On Aug 4, 2013, at 9:10 AM, Robert Seely <rags@math.mcgill.ca> wrote:
If you want *-autonomous categories which are not preorders (I assume that's what you mean by "non-trivial"), Yes, this is what I meant. I guess I should have not said "non-trivial", due to it being somewhat ambiguous.
there is an enormous selection to chose from, including the "first" you mention. One that's simple to use is "the" free *-aut cat (over an arbitrary category, so there are many such free *-aut cats), what we call "circuits" (aka proof nets). One ref:
Natural Deduction and Coherence for Weakly Distributive Categories (Blute-Cockett-Seely-Trimble) (JPAA 113(1996)3, pp 229-296)
I have not read this. Grabbing it now.
In fact, you can find many examples where the double negation isomorphism is in fact an equality, by the following result:
Coherence of the Double Involution on *-Autonomous Categories (Cockett-Hasegawa-Seely) (TAC 17(2006) pp 17-29)
(Of course the second paper is online; the first is also available on my webpage.) Wonderful! I will grab this too.
This illustrates Girard's point (made in his first paper on linear logic) that the double negation isn't inherently non-constructive, rather that the "problem" with classical logic lies with the contraction structure rule. Indeed, and this point is wonderful, because it tells us that in linear logic every connective can have a dual without the equational reasoning
collapsing. What do I mean by this? Consider bi-intuitionistic logic. It is well-known (Crolard:2001) that taking a bi-cartisan closed category and adding co-exponentials we obtain a preorder.
What I am working on is showing that we can do a similar construction using linear categories without degenerating to a preorder in general. That is taking a linear category and its dual a collinear category and smashing them together into what I call a dual linear category. Bellin:2012 showed that a collinear category does (unsurprisingly) model a co-linear type theory using Crolard's term assignment to co-inutitionisitc logic. However, I am a bit dubious of his chosen path. It is well known that Crolard's subtractive logic is not complete for bi-intuitionstic logic. So melding together Bellin's model for co-intutionsitic logic, co-linear categories, with linear categories may not yield a model for bi-intutitionistic linear logic. So this seems to be an open question. Anyway, just thought I would mention what I am working on if anyone has any feedback. Thanks for such a quick response. .\Harley [For admin and other information see: http://www.mta.ca/~cat-dist/ ]