Is $A \& B \multimap A$ derivable? Intuitively, the sentence $A \& B \multimap A$ seems to mean "Using a choice between $A$ and $B$, get an $A$." This feels like it should be derivable for any $A$ and $B$, but I haven't found any way to derive it from the definition of $\&$. Is it possible to establish this in linear logic? Or, if not, what makes this sentence different from the definition of $\&$?
 A: $\DeclareMathOperator{\par}{\unicode{8523}}$
Yes, $A \& B \multimap A$ is provable in linear logic sequent calculus, but the derivation in the answer above is wrong, because there is no rule that allows one to derive $\vdash (A^\bot\oplus B^\bot) \par A$ from $\vdash A^\bot \par A$ (an inference rule in the sequent calculus can only introduce a new principal connective in a formula).
A correct derivation of $A \& B \multimap A$ in the one-sided sequent calculus for linear logic is below.
Note that, according to the one-sided formulation, $A \& B \multimap A$ is the same formula as $(A^\bot\oplus B^\bot) \par A$.
\begin{align}
 \dfrac{\dfrac{\dfrac{}{A^\bot, A}\text{ax}}{A^\bot \oplus B^\bot, A}\oplus}{(A^\bot \oplus B^\bot) \par A} \par
\end{align}
A: It turns out that $A \& B \multimap A$ is provable. Here is the proof, or at least my best attempt at writing it:
$$\DeclareMathOperator{\par}{\unicode{8523}}
\cfrac
{\cfrac
 {\cfrac
  {init}
  {\vdash A^\bot \par A}}
 {\vdash (A^\bot\oplus B^\bot) \par A}}
{\vdash A \& B \multimap A}$$
Using a similar method, you can also prove $A \multimap A\oplus B$.
