Hypersequent Calculi Have Ackermannian Complexity
A. R. Balasubramanian, Vitor Greati, Revantha Ramanayake
TL;DR
The work addresses the complexity of provability in cut-free hypersequent calculi for substructural logics, challenging the expectation that hypersequents automatically incur hyper-Ackermannian complexity. By avoiding the lift to the powerset and exploiting dependencies among hypersequent components, the authors prove Ackermannian upper bounds for all analytic extensions of $\mathbf{FL_{ec}}$ and $\mathbf{FL_{ew}}$, with contraction bounds shown to be optimal for $\mathbf{FL_{ec}}$ and weakening refined via Karp-Miller style acceleration. They further extend the framework to weakening via an $\omega$-calculus, producing a uniform Ackermannian bound for $\mathbf{MTL}$ and related fuzzy logics. The results clarify the complexity landscape, provide a constructive backward proof-search methodology, and connect proof theory with fast-growing hierarchies and automata-theoretic accelerations, yielding practical implications for automated reasoning in substructural logics. Overall, the paper demonstrates that hypersequents do not necessarily elevate complexity beyond Ackermannian levels and offers algorithmic techniques for optimal proof search in these logics.
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}}$).