CATEGORICAL PROOF THEORY OF CO-INTUITIONISTIC LINEAR LOGIC

To provide a categorical seniantics for co-intuitionistic logic, one has to face the fact, noted by Tristan Crolard, that the definition of co-exponents as adjuncts of co-products does not work in the category Set, where co-products are disjoint unions. Following the familiar construction of models of intuitionistic linear logic with exponential we build models of co-intuitionistic logic in symmetric monoidal closed categories with additional structure, using a variant of Crolard's term assignment to co-intuitionistic logic in the construction of a free category.