6
$\begingroup$

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.

$\endgroup$

1 Answer 1

6
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ A very helpful answer, thank you. What texts do you recommend to better understand the theory/category adjunction? In particular, it would be nice to see a detailed application to star-autonomous categories/linearly distributive categories. On the last aspect I wasn't able to find much. Seely's Proposition 1.5 in Linear Logic, *-Autonomous Categories and Cofree Coalgebras (1989) did not help really. $\endgroup$ Apr 29, 2022 at 12:10
  • $\begingroup$ Do you know any texts where your claims that "the internal language of a linearly distributive category is classical linear logic with tensor and par only" and that "the syntactic category of classical linear logic with tensor and par only is the category of linearly distributive categories (with what type of functors?)" are proved? $\endgroup$ May 3, 2022 at 10:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.