Multiplicative Linear Logic

Multiplicative Linear Logic (MLL) is the fragment of linear logic consisting of

• the multiplicative connectives \otimes and ⅋
• (optionally) their multiplicative units \mathbf{1} and \bot

Because of the presence of ⅋, MLL is a fragment of classical linear logic.

MLL is often extended by the MIX rule, to form a fragment known as MLL+MIX.

Proof nets

Please expand.

Models

Any model of a superset of MLL (MELL, MALL, MAELL, and full linear logic) is also a model of MLL.

Chu spaces can be used to define a fully complete model of MLL Devarajan et al. 1999.

Decidability

Please expand.

Axiomatization

MLL can be axiomatized as follows Devarajan et al. 1999. We begin with the axioms

To these we must add the key axiom of linear distributivity:

(A ⅋ B) \otimes C \vdash A ⅋ (B \otimes C)

which can equivalently be stated as A \multimap B, C \vdash A \multimap (B \otimes C).

Finally, we must close these axioms under the functorial rule:

\frac{
  A \vdash A'
    \quad
  B \vdash B'
}{
  A \otimes B \vdash A' \otimes B'
}
  \quad
\frac{
  A \vdash A'
    \quad
  B \vdash B'
}{
  A ⅋ B \vdash A' ⅋ B'
}

See also

• Linear Logic
• Multiplicative Exponential Linear Logic

References

• The following papers present models of MLL:

@article{abramsky_1994,
	title = {Games and {Full} {Completeness} for {Multiplicative} {Linear} {Logic}},
	volume = {59},
	doi = {10.2307/2275407},
	number = {2},
	journal = {The Journal of Symbolic Logic},
	author = {Abramsky, Samson and Jagadeesan, Radha},
	year = {1994},
	pages = {543}
}

@inproceedings{devarajan_1999,
	title = {Full completeness of the multiplicative linear logic of {Chu} spaces},
	doi = {10.1109/LICS.1999.782619},
	booktitle = {Proceedings. 14th {Symposium} on {Logic} in {Computer} {Science} ({Cat}. {No}. {PR00158})},
	publisher = {IEEE Computer Society},
	author = {Devarajan, H. and Hughes, D. and Plotkin, G. and Pratt, V.},
	year = {1999},
	pages = {234--243}
}