Is $A \& B \multimap A$ derivable?

Question

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

Answer 1

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

Answer 2

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