Multiplicative Linear Logic (MLL) is the fragment of linear logic consisting of
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.
Please expand.
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].
Please expand.
MLL can be axiomatized as follows [Devarajan et al. 1999]. We begin with the axioms
| Axiom | Formula |
|---|---|
| identity | |
| associativity of | |
| associativity of | |
| commutativity of | |
| commutativity of |
To these we must add the key axiom of linear distributivity:
which can equivalently be stated as .
Finally, we must close these axioms under the functorial rule:
Abramsky, Samson, and Radha Jagadeesan. 1994. ‘Games and Full Completeness for Multiplicative Linear Logic’. The Journal of Symbolic Logic 59 (2): 543. https://doi.org/10.2307/2275407. arXiv
@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}
}
Devarajan, H., D. Hughes, G. Plotkin, and V. Pratt. 1999. ‘Full Completeness of the Multiplicative Linear Logic of Chu Spaces’. In Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), 234–43. IEEE Computer Society. https://doi.org/10.1109/LICS.1999.782619. pdf
@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}
}