2026-09-20T23:50:25Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26797 2026-09-05T19:57:31Z ddc:004 open_access

Hypersequent Calculi Have Ackermann Complexity Balasubramanian, A. R. Greati, Vitor Ramanayake, Revantha Hypersequent calculi Substructural logics Ackermann complexity Well-quasi-orders For substructural logics with contraction or weakening admitting cut-free sequent calculi, proof search was analyzed using well-quasi-orders on ℕ^d (Dickson’s lemma), yielding Ackermann 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 Ackermann to hyper-Ackermann complexity in the fast-growing hierarchy, suggesting that cut-free hypersequent calculi for extensions of the commutative Full Lambek calculus with contraction or weakening (FL_ec/FL_ew) inherently entail hyper-Ackermann upper bounds. We show that this intuition does not hold: every extension of FL_ec and FL_ew admitting a cut-free hypersequent calculus has an Ackermann 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 MTL. Our Ackermann upper bound is optimal for the contraction case (realized by the logic FL_ec). Schloss Dagstuhl – Leibniz-Zentrum für Informatik A. R. Balasubramanian and Vitor Greati and Revantha Ramanayake 2026 Is Part Of LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.LICS.2026.10 urn:nbn:de:0030-drops-267970 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.10 eng https://creativecommons.org/licenses/by/4.0/legalcode