Subject: categories: Re: quantum quandaries - a category-theoretic perspective

From: Vaughan Pratt <[email-masked]>
Date: Fri, 09 Apr 2004 14:18:39 -0700

Hi, Paul,

>> This view of intuitionistic logic as a fragment of the bigger linear logic,
>is widely held but I don't agree with it.

What's to disagree with?  Girard's ! admits bicartesian models.

>But a model of linear logic doesn't, as far as I'm aware, give rise to a
>bicartesian closed category.

"Give rise to"?

Granted the LL axioms don't stipulate that the image of bang be bicartesian
(have sum in addition to product), but neither do they disallow it.  The
interpretations of ! encountered in LL applications tend to be bicartesian
closed, in particular the one that my message was all about, namely Set.

>So there's no translation (at the level of proofs, rather than
>provability) from intuitionistic logic to linear logic.

Perhaps so, but then that's your problem, you're the one who's insisting on
a different definition of "intuitionistic" from the one Girard had in mind
when he axiomatized !.  If he'd wanted bicartesian closed, the axioms for
! would have said so.  Since you're the one who wants it, the responsibility
for axiomatizing !  accordingly is yours, not Girard's.

Vaughan Pratt