6
$\begingroup$

It is well known that multiplicative linear logic (MLL) is conservative over intuitionistic multiplicative linear logic (IMLL). In other words, if an IMLL formula is provable in MLL then it is already provable in IMLL.

Who first proved this, and how? It doesn’t seem to be in Girard’s original Linear Logic paper, yet I've never seen a reference given when this fact is referred to.

$\endgroup$
2
  • 1
    $\begingroup$ there are a few references I might suggest, depending on what exactly you have in mind. But since that is a different question, I think the modus operandi for this site would be to accept my answer to your first question (if you think it is resolved), then post your second question separately, with a new title. That way it might also get noticed by people who didn't happen to click on the first question. $\endgroup$ Apr 1, 2015 at 8:01
  • $\begingroup$ Done. $\endgroup$ Apr 1, 2015 at 11:02

1 Answer 1

7
$\begingroup$

This is (a piece of) Proposition 3.8 in

  • Harold Schellinx, Some Syntactical Observations on Linear Logic, J. Logic Compututa., Vol. 1 No. 4, pp. 537-559, 1991. (pdf at oxford journals)

His proof-theoretic argument is that the only way to use a sequent with multiple conclusions when giving a cut-free MLL proof of an intuitionistic sequent $\Gamma \Rightarrow C$ is as the left premise (of the form $\Gamma_1 \Rightarrow A,C$) of the ${\multimap}L$ rule. But then the right premise (of the form $\Gamma_2,B \Rightarrow \cdot$) must have an empty right hand side, and by induction it is easy to see that such sequents are unprovable in the absence of 0 or $\bot$. Hence any cut-free MLL proof of an intuitionistic sequent $\Gamma \Rightarrow C$ is limited to sequents with exactly one conclusion, and can be replayed as an IMLL proof.

$\endgroup$
1
  • 1
    $\begingroup$ Great, thanks! I don’t have access to this journal, but there seems to be an earlier version here, where the corresponding result seems to be Theorem 3.10. $\endgroup$ Mar 31, 2015 at 17:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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