Can anyone give me a good reason for taking ! literally as a comonad when defining the notion of "model of linear logic"? The problem I have with it is that it seems to force either the co-Kleisli or co-Eilenberg-Moore category on you. I have two objections to this. First, correct me if I'm wrong but I was under the impression that co-Eilenberg-Moore categories were hard to determine. Second, again correct me if I've misunderstood this, but if you have a particular adjunction in mind and F is not comonadic, then when you plug FU into the definition it won't give your F and U back. Instead it will go into convulsions trying to find some comonadic adjunction that you didn't want in the first place. The alternative I have in mind is that the notion of model should be defined so as to permit you to specify an adjunction F -| U such that ! = FU. This allows you to use whatever nice adjunction you had in mind in place of the canonical one determined by FU. One might require that U be monadic, but I don't see any compelling reason to require this. I've been doing just this for the past couple of years, but it occurs to me that the notion of "model of linear logic" might need to be standardized at some point, in which case it would be a pity if it got this detail wrong. Vaughan Pratt ==============================================================================
In asking my previous question about comonads vs. adjunctions in linear logic I had assumed a negative answer to the following question: Need the Kleisli category be the only CCC among the adjunctions defining a Girard comonad !:D->D (one with !(AxB)^!(A)@!(B), !(1)^I)? What is the truth of the matter? Under the proposed definition of ! (just a comonad, no specification of the intended adjunction) a counterexample to the above would be ruled out as a model of linear logic in the sense that abstracting the adjunction to a comonad in effect replaces the intended CCC by the (distinct) Kleisli CCC. Vaughan Pratt ==============================================================================
One answer to Vaughan's question is that if the original category has equalizers, then the Eilenberg-Moore category is also a CCC. With equalizers too, which makes it, by my estimation, a better model. A CCC that does not have equalizers is not much of a model of classical logic, since without equalizers, you cannot form predicates, at least not freely. Are there other CCCs? There is not reason why not, although I don't any example offhand. Michael ==============================================================================
participants (2)
-
barr＠triples.Math.McGill.CA -
Vaughan Pratt