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?