一句话：提出一个限制 Lambek 积规则的相继式演算，精确刻画 Tamari 序，并证明聚焦性与唯一聚焦推导的相干定理。
本文为经典 Tamari 序——由半结合律（等价地右旋转）在全括号词/二叉树上诱导的偏序——引入一个相继式演算。该演算通过对 Lambek 积规则施加简单限制，精确对应 Tamari 序。作者证明该演算具有聚焦性质（cut-elimination 的加强），并由此得到相干定理：Tamari 序中每个有效蕴含都有恰好一个聚焦推导。作为应用，文中给出 Tamari 序格性质的新证明，以及 Tamari 格 Y_n 区间数满足 Tutte-Chapoton 公式的新证明。本文是 FSCD 2017 论文的扩展版。
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$. Comment: This article is an extended version of a paper presented at FSCD 2017. [v2: minor rev] arXiv admin note: text overlap with arXiv:1701.02917