I asked this question ten days ago on MathStackexchange (see [here](https://math.stackexchange.com/questions/4429556/linear-logic-and-linearly-distributive-categories)). Despite having placed a bounty on the question, I have not received any answers or comments until now. Following [Nick Champion's advice](https://meta.mathoverflow.net/questions/5012/can-i-ask-a-question-on-mathoverflow-and-also-on-another-site/5013#5013), I therefore have decided to cross-post the question on this site.


**1. Context**  

On page two of the introduction to their paper [*Weakly distributive categories*](https://www.math.mcgill.ca/rags/linear/Cockett-Seely-WDC-Durham1991-corrected.pdf) on [linearly distributive categories](https://ncatlab.org/nlab/show/linearly+distributive+category) Cockett and Seely write:



> 
> It turns out that these weak distributivity maps, when present coherently, are precisely the necessary structure required to construct a polycategory superstructure, and hence a Gentzen style calculus, over a category with two tensors. **The weak distributivity maps allow the expression of the Gentzen cut rule in terms of ordinary (categorical) composition.**  
> 
> We call categories with two tensors linked by coherent weak distribution *weakly distributive categories*. **They can be built up to be the proof theory of the full multiplicative fragment of classical linear logic by adding the following maps. $$\top \rightarrow A ⅋ A^{\perp}$$ $$A \otimes A^{\perp} \rightarrow \bot$$**
> 
> 
> 


Similarly, Blute and Scott write in [*Category theory for Linear Logicians*](https://www.site.uottawa.ca/%7Ephil/papers/catsurv.web.pdf):



> 
> **Roughly, linearly distributive categories axiomatize multiplicative linear logic in terms of tensor and par, as opposed to tensor and negation.**
> 
> 
> 


I am trying to understand the sentences marked in bold. It seems that they refer to a relationship between linearly distributive categories and linear logic which I do not understand.


**2. Questions**


* What is meant by the sentence "[weakly distributive categories] can be built up to be the proof theory of the full multiplicative fragment of classical linear logic"? How do you make this statement (formally) precise? Is it related to the adjunction $Theories \rightleftarrows Categories$ described in the nLab-article [syntactic category](https://ncatlab.org/nlab/show/syntactic+category)?
* How do the linear distributivity maps "allow the expression of the Gentzen cut rule in terms of ordinary (categorical) composition"?


Besides an explanation, I would also happily accept a reference to a text that discusses the relationship in question in detail.



Linear logic and linearly distributive categories
Yes, Cockett and Seely's comment about proof theory is a reference to the theory/category adjunction. Each kind of theory corresponds to a kind of category, for instance:





| Theory | Category |
| --- | --- |
| simply typed lambda-calculus | cartesian closed category |
| intuitionistic multiplicative linear logic | closed symmetric monoidal category |
| classical multiplicative linear logic with $\otimes,⅋$, and negation | $\ast$-autonomous category = linearly distributive category with duals |
| classical multiplicative linear logic with $\otimes$ and ⅋ only | linearly distributive category |



In between the theories and the above "categories with structure", there are notions like multicategories and polycategories that represent the judgmental structure of a theory only, and in which connectives can be characterized by universal properties yielding a structure equivalent to the above categories with structure.


For instance, IMLL has sequents of the form $A\_1,\dots,A\_m \vdash B$, corresponding to the homsets of a multicategory, in which $\otimes,\multimap$ can be given universal properties yielding a CSMC. Similarly, CMLL has sequents of the form $A\_1,\dots,A\_m \vdash B\_1,\dots,B\_n$, corresponding to the homsets of a polycategory, and in which $\otimes,⅋,(-)^\perp$ can be given universal properties. A polycategory in which only $\otimes,⅋$ exist is equivalent to a linearly distributive category, while if it also has duals $(-)^\perp$ it is equivalent to a $\ast$-autonomous category. I think this adding of duals is what Cockett and Seely are referring to "build up" -- starting from a linearly distributive category you can add an assumption of duals to obtain the structure corresponding to full CMLL (namely, a $\ast$-autonomous category).


Your quote from Blute and Scott is, I believe, a reference to this connection between linearly distributive and $\ast$-autonomous categories. The usual definition of a $\ast$-autonomous category involves only $\otimes$ and duals, from which ⅋ can be constructed; so I think they are contrasting this with linearly distributive categories, which have $\otimes,⅋$, in terms of which duals can be characterized (though they may not always exist).


Finally, the sentence about the Gentzen cut rule is a reference to the equivalence between polycategories with $\otimes$,⅋ and linearly distributive categories. Given a linearly distributive category $\cal C$, we define the polycategorical morphisms $(A\_1,\dots,A\_m) \to (B\_1,\dots,B\_n)$ to be the morphisms $A\_1 \otimes \cdots \otimes A\_m \to B\_1 ⅋ \cdots ⅋ B\_n$ in $\cal C$. The linear distributivities are then used to construct the polycategorical composition on these morphisms.


The simplest nontrivial case is composing a morphism $A \to (B,C)$ with a morphism $(C,D) \to E$, which should yield a morphism $(A,D) \to (B,E)$. This is an instance of polycategorical composition, which is a categorical representation of the cut rule for CLL:


$$ \frac{A \vdash B,C \qquad C,D \vdash E}{A,D \vdash B,E}$$


To construct such a composition in a linearly distributive category, we have morphisms $A\to B⅋C$ and $C\otimes D\to E$, and we can form the composite
$$A\otimes D \to (B⅋C) \otimes D \to B ⅋(C\otimes D) \to B ⅋E$$
using the linear distributivity in the middle.


