Why don't the quantifiers split in linear logic?

685 Views Asked by At

Every presentation of linear logic I've seen seems to either omit or treat quantifiers as an after-thought. Even Girard says that there is "little to say" about them. However, if we view universal (existential) quantification as a generalization of conjunction (disjunction), then we would expect that we would have two of each. For instance, we might expect that there is a $\forall_\otimes$ corresponding to $\otimes$, where $\forall_\otimes x\in A. \varphi(x)$ could be interpreted as saying that you can simultaneously have $\varphi(a)$ for all $a\in A$; and a $\forall_\&$ corresponding to $\&$, where $\forall_\& x\in A. \varphi(x)$ could be interpreted as saying that you may pick any one $a\in A$ and obtain $\varphi(a)$. I'm wondering if there is something wrong with my thinking, or some good reason for why quantifiers are boring in linear logic.