9
$\begingroup$

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?

$\endgroup$
3
  • $\begingroup$ 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. $\endgroup$
    – Zhen Lin
    Mar 26, 2014 at 9:20
  • $\begingroup$ @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? $\endgroup$ Mar 26, 2014 at 10:06
  • $\begingroup$ 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. $\endgroup$
    – Zhen Lin
    Mar 26, 2014 at 10:21

1 Answer 1

2
$\begingroup$

I think there is a reference that fits perfectly with your requests (Question 1 and, indirectly, Question 0):

Paul-André Melliès: Categorical Semantics of Linear Logic. Panoramas et Synthèses 27, Société Mathématique de France, 2009.

This survey is designed to guide the reader in investigating the symbolic mechanisms of cut-elimination in proof theory and especially in linear logic, and their algebraic transcription as coherence diagrams in categories with structure.

From the abstract:

We start the survey by a short introduction to proof theory (Chapter 1) followed by an informal explanation of the principles of denotational seman- tics (Chapter 2) which we understand as a representation theory for proofs – generating algebraic invariants modulo cut-elimination. After describing in full detail the cut-elimination procedure of linear logic (Chapter 3), we explain how to transcribe it into the language of categories with structure. We review three alternative formulations of ∗-autonomous category, or monoidal category with classical duality (Chapter 4). Then, after giving a 2-categorical account of lax and oplax monoidal adjunctions (Chapter 5) and recalling the notions of monoids and monads (Chapter 6) we relate four different categorical axiomati- zations of propositional linear logic appearing in the literature (Chapter 7). We conclude the survey by describing two concrete models of linear logic, based on coherence spaces and sequential games (Chapter 8) and by discussing a series of future research directions (Chapter 9)

Chapter 4 is devoted to symmetric monoidal closed categories and their relationship with linear logic.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .