Categorical Proof Theory of Co-Intuitionistic Linear Logic

摘要

To provide a categorical semantics for co-intuitionistic logic one has toface the fact, noted by Tristan Crolard, that the definition of co-exponents asadjuncts of coproducts does not work in the category Set, where coproducts aredisjoint unions. Following the familiar construction of models ofintuitionistic linear logic with exponential"!", we build models ofco-intuitionistic logic in symmetric monoidal left-closed categories withadditional structure, using a variant of Crolard's term assignment toco-intuitionistic logic in the construction of a free category.