Distributive property of tensor ($\otimes$) over par (⅋) in linear logic In the setting of linear logic, does the tensor $\otimes$ distribute over the par $⅋$? 
That is, is it possible to show that
$$
A \otimes (B ⅋ C) \stackrel?\equiv 
(A \otimes B) ⅋ (A \otimes C)
$$
holds? If not, what is a counterexample?
The intuition in terms of resources is that if I have $A$ and a multiplicative disjunction of $B$ and $C$ it is the same as saying that I have a multiplicative disjunction of  ($A \otimes B$) and ($A\otimes B$).
Other distributive properties of linear logic. For reference, it is certainly true that $\otimes$ distributes over $\oplus$ and that $⅋$ distributes over $\&$:
$$ A \otimes (B \oplus C) \equiv (A \otimes B)\oplus (A\otimes C)$$
$$ A ⅋ (B \& C) \equiv (A ⅋ B) \& (A ⅋ C)$$
 A: No, the equivalence $A \otimes (B ⅋ C) \equiv 
(A \otimes B) ⅋ (A \otimes C)$ does not hold in linear logic. Indeed, it is not possible to prove that $A \otimes (B ⅋ C) \vdash (A \otimes B) ⅋ (A \otimes C)$ in linear logic sequent calculus (and similarly, it is not possible to prove that $(A \otimes B) ⅋ (A \otimes C) \vdash A \otimes (B ⅋ C)$ in linear logic sequent calculus).
Let us prove this by contradiction. Suppose that $A \otimes (B ⅋ C) \vdash (A \otimes B) ⅋ (A \otimes C)$ is provable, where $A$, $B$ and $C$ are distinct propositional variables. Since the rules $\otimes_L$ and $⅋_R$ are reversible and the cut rule is admissible, there would be a derivation in linear logic sequent calculus of the form:
\begin{align}
\dfrac{\dfrac{\qquad\qquad\vdots \ \pi \\ A, (B ⅋ C) \vdash (A \otimes B), (A \otimes C)}{A \otimes (B ⅋ C) \vdash (A \otimes B), (A \otimes C)}\otimes_L}{A \otimes (B ⅋ C) \vdash (A \otimes B) ⅋ (A \otimes C)} ⅋_R
\end{align}
There would be several possibilities for the last rule of the derivation $\pi$ with conclusion $A, (B ⅋ C) \vdash (A \otimes B), (A \otimes C)$:


*

*$\dfrac{A, B \vdash A \otimes B \qquad C \vdash A \otimes C}{A, (B ⅋ C) \vdash (A \otimes B), (A \otimes C)} ⅋_L$, but then the sequent $C \vdash A \otimes C$ is not derivable (since $A$ is not derivable).

*$\dfrac{B \vdash A \otimes B \qquad A, C \vdash A \otimes C}{A, (B ⅋ C) \vdash (A \otimes B), (A \otimes C)} ⅋_L$, but then the sequent $B \vdash A \otimes B$ is not derivable (since $A$ is not derivable).

*$\dfrac{A, B \vdash A \otimes C \qquad C \vdash A \otimes B}{A, (B ⅋ C) \vdash (A \otimes B), (A \otimes C)} ⅋_L$, but then the sequent $C \vdash A \otimes B$ is not derivable (since $A$ and $B$ are not derivable).

*$\dfrac{B \vdash A \otimes C \qquad A, C \vdash A \otimes B}{A, (B ⅋ C) \vdash (A \otimes B), (A \otimes C)} ⅋_L$, but then the sequent $B \vdash A \otimes C$ is not derivable (since $A$ and $C$ are not derivable).

*$\dfrac{A \vdash A  \qquad B ⅋ C  \vdash B, A \otimes C}{A, (B ⅋ C) \vdash (A \otimes B), (A \otimes C)} \otimes_R$, but then the sequent $B ⅋ C \vdash B, A \otimes C$ is not derivable (since $A$ is not derivable).

*$\dfrac{A \vdash B \qquad B ⅋ C \vdash A, A \otimes C}{A, (B ⅋ C) \vdash (A \otimes B), (A \otimes C)} \otimes_R$, but then the sequent $A \vdash B$ is not derivable (since $A \neq B$).

*$\dfrac{A \vdash A, A \otimes C  \qquad B ⅋ C  \vdash B}{A, (B ⅋ C) \vdash (A \otimes B), (A \otimes C)} \otimes_R$, but then the sequent $B ⅋ C \vdash B$ is not derivable (since $C$ is not derivable).

*$\dfrac{A \vdash B, A \otimes C \qquad B ⅋ C \vdash A }{A, (B ⅋ C) \vdash (A \otimes B), (A \otimes C)} \otimes_R$, but then the sequent $A \vdash B$ is not derivable (since $A\neq B$).

*... (many other cases, in the same vein).
Therefore, in all cases the last rule for the derivation $\pi$ is impossible. Hence, there is no derivation $\pi$ with conclusion $,(⅋)⊢( \otimes ),( \otimes )$ and so there is no derivation with conclusion $ \otimes (⅋)⊢( \otimes ) ⅋ (\otimes )$.

There is another way to prove that the sequent $ \otimes (⅋)⊢( \otimes ) ⅋ (\otimes )$ is not derivable, when $A$, $B$ and $C$ are propositional variable. By cut admissibility, it is easy to prove that if a sequent $\Gamma \vdash \Delta$ containing only the connectives $\otimes$ and $⅋$ is derivable, then the propositional variables are balanced, which means that, for each propositional variable, the number of its occurrences in $\Gamma$ is equal to the number of its occurrences in $\Delta$. But in the sequent $ \otimes (⅋)⊢( \otimes ) ⅋ (\otimes )$ (which contains only the connectives $\otimes$ and $⅋$) on the left of $\vdash$ there is $1$ occurrence of the propositional variable $A$, while on te right of $\vdash$ there are $2$ occurrences of $A$. Therefore, the sequent $ \otimes (⅋)⊢( \otimes ) ⅋ (\otimes )$ is not derivable.

For a quick introduction to linear logic, see here, here and here.
