Re: Non-triviality of *-autonomous categories

[Robert Seely <rags@math.mcgill.ca>]

If you want *-autonomous categories which are not preorders (I assume
that's what you mean by "non-trivial"), 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)

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.)

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.

-= rags =-

On Sat, 3 Aug 2013, Harley D. Eades III wrote:

> Hi, everyone.
>
> I am having trouble finding a reference.  I thought perhaps someone here
> might know.
>
> It is well known that adding the isomorphism:
>   d : A -> (A => 1) => 1
> to a bicartisan closed category degenerates to a preorder.
>
> In *-autonomous categories we have such an isomorphism, but
> is non-trivial.  Where can I find a proof of this?  I would like to
> reference it.
>
> I think one could proof this using the category of coherence spaces and linear maps
> as a concrete *-autonomous category. See for example:
>
> [1] R. a. g. Seely. Linear logic, *-autonomous categories and cofree coalgebras. In Computer Science Logic, 1989.
>
> Any references anyone might have would be great.
>
> Thanks,
> .\ Harley
>
>
>
-- 
<rags@math.mcgill.ca>
<www.math.mcgill.ca/rags>


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]