Hypersequent Calculi Have Ackermannian Complexity

TL;DR

This paper demonstrates that hypersequent calculi for certain substructural logics have Ackermannian complexity bounds, and introduces novel techniques to establish these bounds without resorting to powerset constructions.

Contribution

It proves that all extensions of specific substructural logics with hypersequent calculi have Ackermannian upper bounds, challenging previous assumptions of hyper-Ackermannian complexity.

Findings

Hypersequent calculi for extensions of $ extbf{FL_{ec}}$ and $ extbf{FL_{ew}}$ have Ackermannian complexity bounds.

Novel dependencies between sequents enable avoiding powerset constructions in complexity analysis.

Improved upper bounds for the logic $ extbf{MTL}$ using Karp-Miller style acceleration.

Abstract

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}}$).