{"id":"arxiv/2602.19229","url":"https://arxiv.org/abs/2602.19229","tags":["cs.LO","cs.CC","math.LO"],"score":0,"title":"Hypersequent Calculi Have Ackermannian Complexity","domain":"cs.LO","source":"arxiv","authors":["A. R. Balasubramanian","Vitor Greati","Revantha Ramanayake"],"reviews":0,"subject":"cs.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-02-22","reactions":{}}