# 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 $$\&$$?

$$\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}
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$$.