Linear logic

Remarks

The two conjunctions differ in how they treat the context. The right rule of $\otimes$ derives $\Gamma, \Gamma' \vdash A \otimes B, \Delta, \Delta'$ from $\Gamma \vdash A, \Delta$ and $\Gamma' \vdash B, \Delta'$, so the context is split. The right rule of $\&$ derives $\Gamma \vdash A \mathbin{\&} B, \Delta$ from $\Gamma \vdash A, \Delta$ and $\Gamma \vdash B, \Delta$, so the context is shared.

Example: $A \vdash A \mathbin{\&} A$ is derivable for a variable $A$: apply the $\&$ rule to two copies of the axiom $A \vdash A$.

Non-example: $A \vdash A \otimes A$ is not derivable for a variable $A$. By cut elimination, a derivation can be taken cut-free, and then its last rule is the $\otimes$ rule. That rule would need $A$ for one premise and the empty context for the other, and $\vdash A$ is not derivable. In classical propositional logic, $A \to A \land A$ holds, which shows the role of contraction.