Title: A sequent calculus for the Tamari order,
Abstract: We introduce a sequent calculus with a simple restriction of Lambek's product
rules that precisely captures the classical Tamari order, i.e., the partial
order on fully-bracketed words (equivalently, binary trees) induced by a
semi-associative law (equivalently, tree rotation). We establish a focusing
property for this sequent calculus (a strengthening of cut-elimination), which
yields the following coherence theorem: every valid entailment in the Tamari
order has exactly one focused derivation. One combinatorial application of this
coherence theorem is a new proof of the Tutte-Chapoton formula for the number
of intervals in the Tamari lattice $Y_n$. We also apply the sequent calculus
and the coherence theorem to build a surprising bijection between intervals of
the Tamari order and a certain fragment of lambda calculus, consisting of the
$\beta$-normal planar lambda terms with no closed proper subterms.