Classical multiplicative linear logic \(\simeq\) intuitionistic MLL (Q2751819)

The authors show that a deduction in CMLL (Classical Multiplicative Linear Logic) can be regarded as the result of the natural translation, *, of an intuitionistic one, IMLL. This is as expected, because rules for multiplicative connectives are so set up that any recurrence of a formula can be traced unambiguously through a deduction. The authors allow the constant \(I\) (truth), and avoid proof nets so the translation is among sequents. On the CMLL side, symbols used are: \(I\), propositional variables and their negations. Formulas are built by means of \(\otimes\) (and), \({\mathfrak p}\) (or), and a sequent is a multi-set. On the IMLL side, the negation is not used, the connectives are \(\otimes\) and \(\circ\diagrbar\;\) (implies), and a sequent is of the form \(\Gamma\to A\). The theorem reads roughly: If \(d\) is a CMLL derivation of \(\Gamma,A\), and there are IMLL \(e\) and \(\Gamma_1\to A_1\) such that \(d\) is \(e^*\), and so \(\Gamma,A\) is \((\Gamma_1\to A_1)^*\). E.g. the axiom \(\overline{p},p\) is obtained as \((p\to p)^*\). \{The actual theorem is more complicated mainly due to \(I\)\}. NEWLINENEWLINENEWLINEIn definition of *, the negation sign is missing here and there.NEWLINENEWLINEFor the entire collection see [Zbl 0960.00036].