Ordered logic is the internal language of which class of categories?

Question

Wikipedia says:

The internal language of closed symmetric monoidal categories is linear logic and the type system is the linear type system.

"A Fibrational Framework for Substructural and Modal Logics" says:

Linear logic is ordered logic with exchange, so to model this we add a commutativity equation $$x \otimes y \equiv y \otimes x$$

1. Does this mean that if we take the definition of a closed symmetric monoidal category, and then remove the requirement that the tensor product $\otimes$ be commutative, we obtain the class of categories whose internal language is ordered logic?
2. Would braided monoidal categories, where $x \otimes y \cong y \otimes x$, have an internal language that's strictly between linear logic and ordered logic in terms of restrictions?

Answer 1

Yes, ordered logic is the internal language of non-symmetric monoidal categories. As with linear and nonlinear logic, if the ordered logic contains function-types then they correspond to internal-homs making the monoidal category closed, although one has to be a bit careful since in the non-symmetric case there are two inequivalent notions of internal-hom; sometimes one speaks of "left closed" and "right closed" to distinguish, with either "closed" or "biclosed" when both are present.

And yes, in principle braided monoidal categories should have an internal "braided logic". I've never seen such a thing written down, but something along those lines could be obtained by writing the mode theory of a braided monoidal category in our general framework.