I would like to add something to what I said about the !. Jim Otto pointed this out to me a year ago. If you take modules over a commutative ring it is closed monoidal category. It is a model for a fragment of linear logic, missing negation. Define !M as the free module generated by the underlying set of M. Then !(M x N) is !M tensor !N and so is ostensibly a cofree functor. The Eilenberg-Moore category is the category of sets and the Kleisli category is the full subcategory whose objects are the sets underlying modules. To me this seems to mean that unless the ! has some sensible relation to the linear logic of the category, there is really no content to the claim that you have a model of classical logic inside the linear logic. The only models that seem to fill that requirement are the cofree coalgebras, assuming they exist. Michael ==============================================================================
participants (1)
-
barr@triples.Math.McGill.CA