3
$\begingroup$

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

$\endgroup$
2
$\begingroup$

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

$\endgroup$
0
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.