Linear distributivity

In a logic with two binary operators, say \otimes and \oplus, the axiom of linear distributivity states that one distributes over another, in the sense that

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

This axiom is the minimal axiom induced in a (linear) sequent calculus with two binary operators, \otimes and \oplus, behaving a little bit like \land and \lor. Such a logic is studied in detail (and many more references are given) by Cockett and Seely 2017, and dates back to their work on linearly distributive categories.

In linear logic

Linear distributivity is a key theorem of (classical) linear logic, and in particular of the fragment known as multiplicative linear logic. In that setting, it takes the form

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

Remembering that A \multimap B := A^\bot ⅋ B, this can be equivalently stated as

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

which is perhaps more intuitive (but also surprising).

References

BibTeX

@incollection{cockett_2017,
	title = {Proof {Theory} of the {Cut} {Rule}},
	url = {http://www.math.mcgill.ca/rags/misc/proof_theory-essay.pdf},
	booktitle = {Categories for the {Working} {Philosopher}},
	publisher = {Oxford University Press},
	author = {Cockett, J. R. B. and Seely, R. A. G.},
	editor = {Landry, Elaine},
	year = {2017}
}