For substructural logics with contraction or weakening admitting cut-free sequent calculi, proof search was analyzed using well-quasi-orders on $\mathbb{N}^d$ (Dickson's lemma), yielding Ackermannian upper bounds via controlled bad-sequence arguments. For hypersequent calculi, that argument lifted the ordering to the powerset, since a hypersequent is a (multi)set of sequents. This induces a jump from Ackermannian to hyper-Ackermannian complexity in the fast-growing hierarchy, suggesting that cut-free hypersequent calculi for extensions of the commutative Full Lambek calculus with contraction or weakening ($\mathbf{FL_{ec}}$/$\mathbf{FL_{ew}}$) inherently entail hyper-Ackermannian upper bounds. We show that this intuition does not hold: every extension of $\mathbf{FL_{ec}}$ and $\mathbf{FL_{ew}}$ admitting a cut-free hypersequent calculus has an Ackermannian upper bound on provability. To avoid the powerset, we exploit novel dependencies between individual sequents within any hypersequent in backward proof search. The weakening case, in particular, introduces a Karp-Miller style acceleration, and it improves the upper bound for the fundamental fuzzy logic $\mathbf{MTL}$. Our Ackermannian upper bound is optimal for the contraction case (realized by the logic $\mathbf{FL_{ec}}$).

翻译：对于具有收缩或弱化规则且允许无切割序列演算的子结构逻辑，证明搜索曾通过$\mathbb{N}^d$上的良拟序（迪克森引理）进行分析，利用受控坏序列论证得出阿克曼复杂度的上界。对于超序列演算，由于超序列是序列的（多）集合，该论证将序关系提升至幂集，这导致复杂度在快速增长层级中从阿克曼复杂度跃升至超阿克曼复杂度，从而暗示了对于带有收缩或弱化的交换完全兰贝克演算扩展（$\mathbf{FL_{ec}}$/$\mathbf{FL_{ew}}$）的无切割超序列演算本质上蕴含超阿克曼复杂度的上界。我们证明这一直觉并不成立：$\mathbf{FL_{ec}}$和$\mathbf{FL_{ew}}$的每个允许无切割超序列演算的扩展，其可证性均具有阿克曼复杂度的上界。为避免幂集操作，我们利用了在逆向证明搜索中任意超序列内各独立序列间的新型依赖关系。特别是弱化情形引入了卡普-米勒风格的加速技术，并改进了基本模糊逻辑$\mathbf{MTL}$的上界。我们的阿克曼复杂度上界在收缩情形下是最优的（由逻辑$\mathbf{FL_{ec}}$实现）。