Re: Non-triviality of *-autonomous categories

["Harley D. Eades III" <harley.eades@gmail.com>]

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/ ]