The MIX rule of Linear Logic

In linear logic, the MIX rule is defined to be

	\frac{
  	\vdash \Gamma
    \quad
    \vdash \Delta
  }{
    \vdash \Gamma, \Delta
  }

This is equivalent to the provability of

A \otimes B \multimap A ⅋ B

and also to the provability of

\bot \multimap \mathbf{1}

There is also a 0-ary version:

	\frac{}{\vdash\ }

(That is, a proof of the empty sequent.) This one corresponds to the provability of

\mathbf{1} \multimap \bot

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:

\lnot A \otimes \lnot B \multimap \lnot (A \otimes B)
\qquad 1 \multimap \lnot 1

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 \otimes).

The role of MIX in semantics

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).

MIX in the theory of proof nets

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.

@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}
}

@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 \pi (potentially incorrect proof net, traditionally called "proof structure") proving some formula A, one can compute its coherent semantics [[\pi]] for any assignment mapping atoms of A to coherence spaces, using the "method of experiments" which does not assume correctness a priori. While [[\pi]] is guaranteed to be a subset of the web |[[A]]| for any pre-proof net, it is not always a clique. The main theorem of Retoré 1997 is that [[\pi]] is a clique of [[A]] for all assignments (a notion of "semantic correctness") if and only if \pi is a correct proof net for MLL+Mix.

@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 \triangleleft that enjoys (A \triangleleft B)^\perp = A^\perp \triangleleft B^\perp 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.

Girard's changing view

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.

References

• A sequent calculus and proof net correctness criterion for classical linear logic with the mix rule is given by

@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. \vdash^i \Gamma. The indices remain invariant under cut elimination. The reasons behind this tomfoolery are explained in

@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}

• Categorical semantics for the MIX rule are given in

@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 \otimes 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:

@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}

@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}
}

@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},
}

@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}
}