Consider the multiplicative fragment of linear logic (MLL) which only consists of the multiplicative connectives tensor and par together with the inference rules axiom, cut, $\otimes$ and ⅋. I was able to show that $(A⅋B) \otimes C \vdash A ⅋ (B \otimes C) $ holds. Is the other entailment $A ⅋ (B \otimes C) \vdash (A⅋B) \otimes C$ also provable in MLL? I could not come up with a proof.
Is $A ⅋ (B \otimes C) \vdash (A⅋B) \otimes C$ provable in MLL
linear-logiclogicsequent-calculus
Best Answer
The axioms and rules of MLLL are valid in classical logic if we read tensor as $\land$ and par as $\lor$. Since $A\lor(B\land C)$ doesn't classically imply $(A\lor B)\land C$, MLL doesn't prove your sequent.