Linear Logic Question About Exponentials

Question

In Linear Logic (L.L.), exponentials {!,?} are used to allow the rules of Weakening and Contraction for formulas under their scope. It is a theorem of Linear Logic that !(P⊗Q)⊸!(P&Q) where ‘⊗’ is multiplicative conjunction, ‘&’ is additive conjunction, and ‘⊸’ is linear implication. So, since Linear Logic is resource sensitive, is it the case that for any L.L. formulas Φ and Ψ, !(Φ⊗Ψ)⊸!(Φ&Ψ) ?

Answer 1

If the formula $!(P \otimes Q) \multimap\ !(P \& Q)$ was a theorem of Linear Logic, then by the identity expansion property $!(\Phi \otimes \Psi) \multimap\ !(\Phi \& \Psi)$ would be a theorem as well for all formulas $\Phi, \Psi$.

The issue is that, contrary to what you wrote, the formula $!(P \otimes Q) \multimap\ !(P \& Q)$ is not a theorem of Linear Logic. You can confirm this by showing that $!(P \& Q) \multimap P$ holds in Linear Logic, while $!(P \otimes Q) \multimap P$ does not.

Intuitively, think about buying shoes: if $P$ is the option to buy the left half of a pair of boots for £100, and $Q$ is the option to buy the right half of a pair of boots for £100, then the policy $!(P \otimes Q)$ just states that you can buy as many pairs of boots as you'd like for £200 each. But the policy $!(P \& Q)$ is much more permissive: it allows you to buy just the left half of a pair of boots for £100, without paying for the corresponding right half at all.