# Logic in closed symmetric monoidal categories; reference request.

Suppose we want an algebraic theory $T$ to be interpretable in any closed symmetric monoidal category $\mathbf{C}.$ I am thinking in particular of the case where $\mathbf{C}$ is the category of models for some commutative algebraic theory, like the equational theory of Abelian groups. Anyway:

Question 0. In what fragment of first-order logic must the axioms for $T$ be specified in order that we may interpret $T$ in any closed symmetric monoidal category? And what inference principles may we use?

I have read that the internal logic of closed monoidal categories is a linear type system. However, I'm not really sure what this means; in fact, I gather its a bit of fluffy statement. From $n$-Lab:

“linear logic” takes on many flavors: in addition to the Girard-style language that is naturally interpreted in star-autonomous categories, one has languages for monoidal biclosed categories, symmetric monoidal closed categories, compact closed categories, and others, collectively representing the “multiplicative” core of linear logic as understood in this general sense.

So what I'd appreciate most would be a reference, somewhere I can get started learning this stuff in a non-fluffy way:

Question 1. Where is a good place to learn about linear type systems in general, and logic in closed symmetric monoidal categories in particular?

• Linear logic is probably your best bet. You need to deal with the fact that variables cannot be duplicated or deleted without some extra structure. Mar 26, 2014 at 9:20
• @ZhenLin, is "linear logic" a specific logic, like "classical first-order logic," or is it a name for a broad class of logics sharing similar features? Mar 26, 2014 at 10:06
• It's a general name. The distinguishing feature is best understood in terms of sequent calculus: the weakening and contraction rules are restricted or removed altogether. Mar 26, 2014 at 10:21