Are exponentials in categorical models of linear logic harmful?

Question

Categorical models for linear logic with $\otimes$, $1$, $\&$, $\top$, $\oplus$, $0$, and $\multimap$ are typically symmetric monoidal closed categories (for modeling $\otimes$, $1$, and $\multimap$) with products (for modeling $\&$ and $\top$) and coproducts (for modeling $\oplus$ and $0$). Is it harmful to additionally require that such a category has exponentials? Exponentials would model a binary operator $\Rightarrow$ for which proofs of $A \vdash B \Rightarrow C$ correspond to proofs of $A \mathbin\& B \vdash C$. Are there sensible categorical models for linear logic that have exponentials, or does the introduction of exponentials make the structure collapse?

Answer 1

No, it does not make the structure collapse. For example consider the category of small categories $\mathbf{Cat}$ --- it is clearly complete and cocomplete cartesian closed category, and moreover it has another closed monoidal structure induced by the "funny tensor" and linear exponents $\mathbb{C} \multimap \mathbb{D}$ given by the category of functors $\mathbb{C} \rightarrow \mathbb{D}$ together with (unnatural) transformations (i.e. "natural transformations" without "naturality" requirement).

Much more is true. Every (small) monoidal category $\langle \mathbb{V}, \otimes, I\rangle$ fully embeds into complete and cocomplete cartesian closed and monoidal closed category. The embedding is given by the usual Yoneda functor $y \colon \mathbb{V} \rightarrow \mathbf{Set}^{\mathbb{V}^{op}}$ and the monoidal closed structure is inherited via the Day convolution: $$(F \otimes G)(X) = \int^{A, B \in \mathbb{V}} F(A) \times G(B) \times \hom(X, A \otimes B)$$ $$(F \overset{L}\multimap G)(X) = \int_{A, B \in \mathbb{V}} G(A)^{F(B) \times \hom(A, X \otimes B)}$$ $$(F \overset{R}\multimap G)(X) = \int_{A, B \in \mathbb{V}} G(A)^{F(B) \times \hom(A, B \otimes X)}$$ where $\overset{L}\multimap$ is the left linear exponent and $\overset{R}\multimap$ is the right linear exponent (which are isomorphic precisely when the tensor $\otimes$ in $\mathbb{V}$ is symmetric). Moreover, it is easy to verify that Yoneda functor preserves the monoidal closed structures. Therefore, in some sense, every monoidal category can be (co)completed to a cartesian closed category with coproducts.

Answer 2

Michal already answered the question where we consider intuitionistic multiplicative linear logic, without an involutive linear negation; there are many such models where we can have a symmetric monoidal closed structure concurrent with a cartesian closed structure on a category. Another easy example (in fact a special case of one of his constructions) is the topos of $G$-sets where $G$ is an abelian group, made into a symmetric monoidal closed category by using the Day convolution.

I'd like to supplement his answer by mentioning that if you do demand an involutive negation as well (i.e., work with classical multiplicative linear logic), which we categorically model using $\ast$-autonomous categories, then we do get a collapse: every such model is posetal. More is true: a cartesian closed category $C$ that is self-dual must be a poset; notice that a classical linear negation gives a self-duality, i.e., an equivalence

$$\neg: C^{op} \stackrel{\cong}{\to} C.$$

This is because the initial object in a cartesian closed category is strict, i.e., for any object $X$, if there is a morphism $X \to 0$, then $X \cong 0$. Given that fact, consider morphisms $1 \to (A \Rightarrow B)$. Then, letting $(-)^\ast$ be the self-duality functor, these are in bijective correspondence with morphisms

$$(A \Rightarrow B)^\ast \to 0$$

and if such a morphism exists, then $(A \Rightarrow B)^\ast \cong 0$ by strictness. In particular, there is at most one morphism $(A \Rightarrow B)^\ast \to 0$, and therefore at most one morphism $1 \to A \Rightarrow B$, and hence at most one morphism $A \to B$ for any two objects $A$, $B$.