A sequent calculus for a semi-associative law

TL;DR

This paper presents a sequent calculus that characterizes the Tamari order, providing new proofs for its lattice structure and the enumeration of its intervals, through a focusing property and coherence theorem.

Contribution

It introduces a novel sequent calculus capturing the Tamari order and proves a coherence theorem, enabling simplified proofs of key properties of the Tamari lattice.

Findings

Established a focusing property for the calculus

Proved the lattice property of the Tamari order

Derived the Tutte-Chapoton formula for intervals

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, right 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. We then describe two main applications of the coherence theorem, including: 1. A new proof of the lattice property for the Tamari order, and 2. A new proof of the Tutte-Chapoton formula for the number of intervals in the Tamari lattice $Y_n$.