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"?
EDIT: Besides an explanation, I would also happily accept a reference to a text that discusses the relationship in question in detail.
Best Answer
Linearly distributive categories are the models of the fragment of linear logic consisting of the two connectors $\otimes$, $⅋$ and the two multiplicative units $\top$ for $\otimes$ and $\bot$ for $⅋$. This is classical multiplicative linear logic minus the negation.
Models of classical muliplicative linear logic are $*$-autonomous categories. If you have a $*$-autonomous category with tensor $\otimes$, monoidal unit $\top$ and duals noted $A^{\perp}$, you can define $A ⅋ B := (A^{\perp} \otimes B^{\perp})^{\perp}$ and $\bot = \top^{\perp}$ and it gives you a linearly distributive category.
$*$-autonomous categories axiomatize multiplicative linear logic in terms of tensor and negation. Linearly distributive categories doesn't completely axiomatize classical multiplicative linear logic in terms of tensor and par because it doesn't give you the negation. If you add objects $A^{\perp}$ and maps $$\top \rightarrow A ⅋ A^{\perp}$$ $$A \otimes A^{\perp} \rightarrow \bot$$ satisfying appropriate coherence conditions, you recover a $*$-autonomous category.
I think it explains the second and third sentences. Now, the first. From one proof of each of this sequents in linear logic: $$A,B\vdash C,D$$ $$D,E \vdash F$$ you obtain a proof of this sequent $$A,B,E \vdash C,F$$ by using the Gentzen cut rule. In a linearly distributive category we can perform this step in terms of (ordinary) categorical composition like this:
The two proofs correspond to two morphisms: $$ f:A \otimes B \rightarrow C ⅋ D $$ $$ g:D \otimes E \rightarrow F $$
We can form $$ f \otimes E: A \otimes B \otimes E \rightarrow (C⅋D) \otimes E $$ $$ C ⅋ G: C ⅋ (D \otimes E) \rightarrow C ⅋ F $$
To compose them you need an intermediate morphism $$ (C ⅋ D)\otimes E \rightarrow C ⅋ (D \otimes E) $$ between the two and it's exactly one of the four distributive natural transformations defining (non symmetric in the paper) linearly distributive categories, page 52 in the paper of Cockett and Seely.
If you compose the three morphisms, you obtain one of the appropriate type $$ A \otimes B \otimes E \rightarrow C ⅋ F $$ corresponding to the proof obtained by using the cut rule in linear logic.
You can surely find informations in Categorical Semantics of Linear Logic by Paul-André Melliès in addition to the nLab (for example, you have the page star-autonomous category).
I don't really know about