Hypersequent Calculi Have Ackermannian Complexity
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2602.19229
curl -X POST /api/v1/records/arxiv/2602.19229/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2602.19229/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'