1
$\begingroup$

I have a question that might seem odd to linear logic experts (I am somewhat of a novice). I know that two items of the same type can be combined into one premise with a tensor (multiplicative conjunction). Is the opposite also possible? Say, that we have a premise $A\otimes B$, but the only other premise needs the premises $A$ and $B$ to be inserted individually. Is this at all possible? Or is there some rule against this?

Many thanks in advance.

Improve this question
$\endgroup$
8
  • 2
    $\begingroup$ It’s not quite clear to me what the question is, but anyway, a sequent $\Gamma,A,B\Longrightarrow\Delta$ is interderivable with $\Gamma,A\otimes B\Longrightarrow\Delta$. $\endgroup$
    – Emil Jeřábek
    Commented Mar 24, 2015 at 16:56
  • 2
    $\begingroup$ May I suggest that some linear logician (not me, notwithstanding this book) give an explanation of $\otimes$ for the general enlightenment of MO readers. This requires that the question not be closed. I am not aware that Stefan Kohl and Alex Degtyarev are experts in this subject. $\endgroup$
    – Paul Taylor
    Commented Mar 24, 2015 at 18:22
  • 1
    $\begingroup$ I know linear logic quite well but unfortunately I don't understand the question. What do you mean by "opposite"? Are you asking about reversibility of the tensor rule? (If that's the case, the answer is no, the tensor rule is irreversible). $\endgroup$
    – Damiano Mazza
    Commented Mar 25, 2015 at 19:32
  • 2
    $\begingroup$ Zerkezhi, I suggest you focus on Emil's comment instead. The answer I gave to your other question suggests that his interpretation is the relevant one. I think what Damiano is saying is that $A \otimes B \vdash A, B$ is not valid in linear logic, and that's true, but that's because a list of formulas to the right of the entailment symbol is to be interpreted as a linear disjunction, not conjunction. But I suspect that observation is not relevant here. $\endgroup$
    – Todd Trimble
    Commented Mar 26, 2015 at 19:53
  • 1
    $\begingroup$ @Todd actually I meant irreversibility in the proof-theoretic sense: given a proof of $\Gamma\vdash A\otimes B$, if you know that the last rule introduces $A\otimes B$, then you know there are proofs of $\Gamma_1\vdash A$ and $\Gamma_2\vdash B$ with $\Gamma_1+\Gamma_2=\Gamma$ but in general you still don't know how to determine $\Gamma_1$ and $\Gamma_2$. This is unrelated to the derivability of $A\otimes B\vdash A,B$ (the so-called "mix" rule), but I think it is still not what Zerkezhi was asking :-) $\endgroup$
    – Damiano Mazza
    Commented Mar 28, 2015 at 21:30

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .