Distributivity of ⊗ over & in linear logic?

Question

In linear logic, we have that multiplicative conjunction distributes over additive conjunction:

$$(A\ \&\ B) \otimes C ⊸ (A \otimes C)\ \&\ (B \otimes C).$$

But we do not have the other direction:

$$(A \otimes C)\ \&\ (B \otimes C) \not{\!\!⊸\;} (A\ \&\ B) \otimes C.$$

What's a good intuitive explanation of this impossibility?

Answer 1

Remember how the left and right rules for $\&$ can be interpreted (with a formulation related to game semantics, I think this is the most intuitive):

• You need to be able to prove both $A$ and $B$ (under the given hypotheses) if you want to prove $A\& B$, because your opponent (or “the environment”) chooses whether $A \& B$ is $A$ or is $B$. $$\frac{Γ ⊢ A, Δ \qquad Γ ⊢ B, Δ}{Γ ⊢ A \& B, Δ}$$
• Dually, to use $A\& B$, you choose whether it is $A$ or $B$ and the opponent has to provide a proof. $$\cfrac{Γ, A ⊢ Δ}{Γ, A \& B ⊢ Δ} \qquad \cfrac{Γ, B ⊢ Δ}{Γ, A \& B ⊢ Δ}$$

---

Now let us have a look at the first implication: $$(A\ \&\ B) \otimes C ⊸ (A \otimes C)\ \&\ (B \otimes C)$$ You have to be able to prove $A \otimes C$ as well as $B \otimes C$. Let us treat the former case; the latter is symmetric.

To build your proof, you can use a proof of $(A\ \&\ B) \otimes C$, that is to say a proof of $A\ \&\ B$ and a proof of $C$. Since you're on the left side of the sequent, you can choose that this proof of $A\ \&\ B$ is a proof of $A$; then you combine it with the proof of $C$ to get a proof of $A\ \otimes\ C$.

In a proof tree: $$\cfrac{\cfrac{\cfrac{\cfrac{ \cfrac{}{A \vdash A} \quad \cfrac{}{C \vdash C} }{A,C \vdash A \otimes C} }{A\& B,C \vdash A \otimes C} }{(A\&B)\otimes C \vdash A \otimes C} \quad \cfrac{\vdots}{(A\&B)\otimes C \vdash B \otimes C} }{(A\&B)\otimes C \vdash (A\otimes C)\&(B\otimes C)}$$

You can look at it interactively.

---

For the implication which doesn't work: $$(A \otimes C)\ \&\ (B \otimes C) \not{\!\!⊸\;} (A\ \&\ B) \otimes C.$$

It is a linearity problem: to prove $(A\ \&\ B) \otimes C$, you have to decide which part of your hypotheses will be used for $A\ \&\ B$ and which part for $C$ (there is no possible duplication*). Clearly, none of these two conclusions can be derived from the empty sequent, so you have to decompose the hypothesis $(A \otimes C)\ \&\ (B \otimes C)$ first; but this forces you to make a choice between $A \otimes C$ and $B \otimes C$, and you will loose either $A$ or $B$!

(*) Of course, if you were allowed to duplicate hypotheses, i.e. if you had $!((A \otimes C)\ \&\ (B \otimes C))$, it would be different...