# What is the proper name for "compact closed" multiplicative intuitionistic linear logic?

Multiplicative intuitionistic linear logic (MILL) has only multiplicative conjunction $\otimes$ and linear implication $\multimap$ as connectives. It has models in symmetric monoidal closed categories.

Compact closed categories are symmetric monoidal closed categories in which every object $A$ has a dual $A^*$ and $A \multimap B \cong A^* \otimes B$. Thought of as a resource, $A^*$ is a debt, owing someone an $A$. Is there a special name for MILL when these conditions hold? ͏ ͏

This logic was studied by Masaru Shirahata, "A Sequent Calculus for Compact Closed Categories". He just calls it "CMLL", but points out it is equivalent in provability to MLL (classical multiplicative linear logic) with tensor and par identified. Note that the direction tensor $\vdash$ par is commonly called "MIX", so this is also MLL + MIX as an isomorphism.
• Hmm...since BI is a conservative extension of IMLL, I would think that classical BI would also be conservative extension of CMLL, so that the resource interpretations of the multiplicative connectives coincide. Though reading Brotherston and Calcagno's paper (arxiv.org/PS_cache/arxiv/pdf/1005/1005.2340v2.pdf), it's not clear to me that this is the case. For example, is the CMLL equivalence $(A \multimap 1) \multimap 1 \equiv A$ valid in every CBI model? Sep 1, 2010 at 22:05
• And I think the answer is no, because they distinguish the unit of the monoid from an element $\infty$ "that characterises the result of combining an element with its dual involution". The equivalence will be valid in CBI models coming from Abelian groups, but not in general. Brotherston and Calcagno give a bunch of examples of interesting models that don't come from Abelian groups -- but that is the form of the "credits and debits" interpretation. Sep 1, 2010 at 22:21