In a logic with two binary operators, say and , the axiom of linear distributivity states that one distributes over another, in the sense that
This axiom is the minimal axiom induced in a (linear) sequent calculus with two binary operators, and , behaving a little bit like and . 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.
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
Remembering that , this can be equivalently stated as
which is perhaps more intuitive (but also surprising).
Cockett, J. R. B., and R. A. G. Seely. 2017. ‘Proof Theory of the Cut Rule’. In Categories for the Working Philosopher, edited by Elaine Landry. Oxford University Press. [pdf]
@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}
}