In linear logic, the MIX rule is defined to be
This is equivalent to the provability of
and also to the provability of
There is also a 0-ary version:
(That is, a proof of the empty sequent.) This one corresponds to the provability of
The 0-ary version is required to formulate a cut elimination procedure: see [Fleury and Retoré 1994].
The Mix rule may also be formulated using tensor and negation:
which shows that it corresponds to endowing the negation functor with a lax monoidal structure. This is the right formulation of Mix in tensorial logic [Melliès 2017, p. 242] where negation is not involutive (so one cannot define ⅋ as the dual of ).
The MIX rule often appears as a natural inhabitant of many semantic structures investigated in the context of linear logic. From [Bellin 1997]:
[...] the presence of Mix is ubiquitous in researches on linear logic: it is satisfied by most models of linear logic, such as the denotational semantics of coherent spaces, the game-theoretic semantics and more. As the example of the game-theoretic semantics shows (Abramsky and Jagadeesan 1994; Hyland and Ong (manuscript)), results are often obtained for LL MIX first, and additional efforts are then needed to refine them to the case of LL
Most webbed semantics of linear logic indeed satisfy Mix, and the case of coherence spaces has some importance in relation to proof nets (see below).
Allowing the Mix rule in proof nets corresponds to relaxing the Danos-Regnier correctness criterion "every switching graph is acyclic and connected (i.e. a tree)" into "every switching is acyclic (i.e. a forest)", see [Fleury & Retoré 1994]. This is convenient in some circumstances: for instance, it simplifies MELL proof nets since the "jumps" on the weakening nodes – whose only purpose is to be involved in the connectedness condition – become unnecessary. (Similar "jumps" also occur for ⊥ nodes in MLL with units, and here the simplification induced by Mix is radical: it collapses 1 and ⊥ together!)
Another noteworthy feature of the MLL+Mix correctness criterion is that it is equivalent through low-complexity reductions to a classical graph-theoretic problem: the non-existence of alternating elementary cycles for perfect matchings, i.e. (by Berge's lemma) the uniqueness of those perfect matchings inside their ambient graphs. One direction was provided by [Retoré 2003] and the converse is due to [Nguyễn 2020]. The latter paper shows that a lot of structure is preserved by these reductions; this allows one to see for example that a structural theorem from [Bellin 1997] on proof nets is equivalent to a simple statement in pure graph theory.
Retoré, Christian. "Handsome proof-nets: perfect matchings and cographs". Theoretical Computer Science, Linear Logic, 294, nᵒ3 (February 2003): 473‑88. https://doi.org/10.1016/S0304-3975(01)00175-X.
@article{DBLP:journals/tcs/Retore03,
author = {Christian Retor{\'{e}}},
title = {Handsome proof-nets: perfect matchings and cographs},
journal = {Theor. Comput. Sci.},
volume = {294},
number = {3},
pages = {473--488},
year = {2003},
url = {https://doi.org/10.1016/S0304-3975(01)00175-X},
doi = {10.1016/S0304-3975(01)00175-X},
timestamp = {Wed, 17 Feb 2021 21:56:42 +0100},
biburl = {https://dblp.org/rec/journals/tcs/Retore03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
Nguyễn, Lê Thành Dũng. "Unique Perfect Matchings, Forbidden Transitions and Proof Nets for Linear Logic with Mix". Logical Methods in Computer Science Volume 16, Issue 1, nᵒ27 (February 2020): 27:1-27:31. https://lmcs.episciences.org/6172
@article{DBLP:journals/lmcs/Nguyen19,
author = {L{\^{e}} Th{\`{a}}nh Dung Nguy{\~{\^{e}}}n},
title = {Unique perfect matchings, forbidden transitions and proof nets for
linear logic with Mix},
journal = {Log. Methods Comput. Sci.},
volume = {16},
number = {1},
year = {2020},
url = {https://doi.org/10.23638/LMCS-16(1:27)2020},
doi = {10.23638/LMCS-16(1:27)2020},
timestamp = {Wed, 28 Oct 2020 17:00:55 +0100},
biburl = {https://dblp.org/rec/journals/lmcs/Nguyen19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
There is also a semantic justification of the acyclicity criterion in the purely multiplicative setting (MLL+Mix) [Retoré 1997]. Given a multiplicative pre-proof net (potentially incorrect proof net, traditionally called "proof structure") proving some formula , one can compute its coherent semantics for any assignment mapping atoms of to coherence spaces, using the "method of experiments" which does not assume correctness a priori. While is guaranteed to be a subset of the web for any pre-proof net, it is not always a clique. The main theorem of [Retoré 1997] is that is a clique of for all assignments (a notion of "semantic correctness") if and only if is a correct proof net for MLL+Mix.
Retoré, Christian. "A semantic characterisation of the correctness of a proof net". Mathematical Structures in Computer Science 7, nᵒ5 (October 1997): 445‑52.
@article{DBLP:journals/mscs/Retore97,
author = {Christian Retor{\'{e}}},
title = {A Semantic Characterisation of the Correctness of a Proof Net},
journal = {Math. Struct. Comput. Sci.},
volume = {7},
number = {5},
pages = {445--452},
year = {1997},
url = {https://doi.org/10.1017/S096012959700234X},
doi = {10.1017/S096012959700234X},
timestamp = {Wed, 01 Apr 2020 08:48:38 +0200},
biburl = {https://dblp.org/rec/journals/mscs/Retore97.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
Retoré also designed a conservative extension of MLL+Mix called pomset logic using this idea: first define the coherence semantics, and then find a characterization of the semantically correct pre-proof nets. The extension consists in adding a non-commutative connective that enjoys and its proof nets have a binary link for this connective. Pomset logic has been quite influential since it led to the birth of deep inference. The Mix rule holds in pomset logic as well as in the deep inference systems BV and NEL.
Mix is first discussed in Girard's original paper on linear logic (1987). While it is acknowledged that the rule itself isn't proof-theoretically terrible, it is discussed and overall dismissed.
In his later work, Girard is not as dismissive of MIX. The following comes from The Blind Spot, sec. 11.A.4:
Mix is natural in various category-theoretic settings [...]. But this rule is not completely convincing:
- One should perhaps add the 0-ary case, i.e. the axiom ⊥, one would then contradict classical logic and also weakening.
- Weakening, which plays on similar grounds, seems more convincing.
This discussion (by the way, note that I am pushing very prudent views) is typical of the present state of logic. Between « mix » and weakening, none of them, both of them, layer -1 will not decide. Layer -2 neither, since we shall see (Section 12.2.3), that the hypothesis of polarisation destroys the heavy objections against weakening. One finds oneself naked at layer -3: procedurality must decide. But it has not yet spoken: no striking phenomenon has been observed for or against either rule.
Fleury, Arnaud, and Christian Retoré. 1994. ‘The Mix Rule’. Mathematical Structures in Computer Science 4 (2): 273–85. https://doi.org/10.1017/S0960129500000451.
@article{fleury_mix_1994,
title = {The mix rule},
volume = {4},
doi = {10.1017/S0960129500000451},
number = {2},
journal = {Mathematical Structures in Computer Science},
author = {Fleury, Arnaud and Retor\'{e}, Christian},
year = {1994},
pages = {273--285}
}
Strangely, Fleury and Retoré's syntax has sequents annotated with natural number indices, i.e. . The indices remain invariant under cut elimination. The reasons behind this tomfoolery are explained in
Bellin, Gianluigi. 1997. ‘Subnets of Proof-Nets in Multiplicative Linear Logic with MIX’. Mathematical Structures in Computer Science 7 (6): 663–69. https://doi.org/10.1017/S0960129597002326.
@article{bellin_subnets_1997,
title = {Subnets of proof-nets in multiplicative linear logic with {MIX}},
volume = {7},
doi = {10.1017/S0960129597002326},
number = {6},
journal = {Mathematical Structures in Computer Science},
author = {Bellin, Gianluigi},
month = dec,
year = {1997},
pages = {663--669}
Cockett, J. R. B., and R. A. G. Seely. 1997. ‘Proof Theory for Full Intuitionistic Linear Logic, Bilinear Logic, and MIX Categories’. Theory and Applications of Categories 3 (5): 85–131. http://www.tac.mta.ca/tac/volumes/1997/n5/n5.pdf
@article{cockett_proof_1997,
title = {Proof {Theory} for {Full} {Intuitionistic} {Linear} {Logic}, {Bilinear} {Logic}, and {MIX} {Categories}},
volume = {3},
url = {http://www.tac.mta.ca/tac/volumes/1997/n5/n5.pdf},
number = {5},
journal = {Theory and Applications of Categories},
author = {Cockett, J. R. B. and Seely, R. A. G.},
year = {1997},
pages = {85--131}
}
More on categories: an initiality
There is an interesting stackexchange answer by Damiano Mazza. It concerns cut elimination for system of 'compact closed logic' in which and are identified. Damiano calls it too degenerate to be of interest, and points out that it may be very close to the relational model of linear logic.
See the nLab page on the mix rule.
Some more related literature:
Eades III, Harley, and Valeria de Paiva. 2020. ‘Multiple Conclusion Linear Logic: Cut Elimination and More’. Journal of Logic and Computation 30 (1): 157–74. https://doi.org/10.1093/logcom/exaa006.
@article{eades_iii_multiple_2020,
title = {Multiple conclusion linear logic: cut elimination and more},
volume = {30},
doi = {10.1093/logcom/exaa006},
number = {1},
journal = {Journal of Logic and Computation},
author = {Eades III, Harley and de Paiva, Valeria},
year = {2020},
pages = {157--174}
Asperti, Andrea. 1995. ‘Causal Dependencies in Multiplicative Linear Logic with MIX’. Mathematical Structures in Computer Science 5 (3): 351–80. https://doi.org/10.1017/S0960129500000797.
@article{asperti_causal_1995,
title = {Causal dependencies in multiplicative linear logic with {MIX}},
volume = {5},
doi = {10.1017/S0960129500000797},
number = {3},
journal = {Mathematical Structures in Computer Science},
author = {Asperti, Andrea},
year = {1995},
pages = {351--380}
}
Melliès, Paul-André. "Une étude micrologique de la négation". Habilitation à diriger des recherches, Université Paris-Diderot – Paris VII, 2017. pdf
@phdthesis{mellies_hdr_2017,
type = {Habilitation à diriger des recherches},
title = {Une étude micrologique de la négation},
school = {Université Paris-Diderot – Paris VII},
author = {Melliès, Paul-André},
year = {2017},
}
Castellan, Simon, and Nobuko Yoshida. 2019. ‘Causality in Linear Logic: Full Completeness and Injectivity (Unit-Free Multiplicative-Additive Fragment)’. In Foundations of Software Science and Computation Structures, edited by Mikołaj Bojańczyk and Alex Simpson, 11425:150–68. Lecture Notes in Computer Science. Cham: Springer International Publishing. http://iso.mor.phis.me/publis/Causality_in_Linear_Logic_FOSSACS19.pdf
@inproceedings{castellan_causality_2019,
address = {Cham},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Causality in {Linear} {Logic}: {Full} {Completeness} and {Injectivity} ({Unit}-{Free} {Multiplicative}-{Additive} {Fragment})},
volume = {11425},
shorttitle = {Causality in {Linear} {Logic}},
doi = {10.1007/978-3-030-17127-8_9},
language = {en},
booktitle = {Foundations of {Software} {Science} and {Computation} {Structures}},
publisher = {Springer International Publishing},
author = {Castellan, Simon and Yoshida, Nobuko},
editor = {Bojańczyk, Mikołaj and Simpson, Alex},
year = {2019},
pages = {150--168}
}