I asked this question ten days ago on MathStackexchange (see here). Despite having placed a bounty on the question, I have not received any answers or comments until now. Following Nick Champion's advice, 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 on linearly distributive categories 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:
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?
- 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.