Deducibility in the full Lambek calculus with weakening is HAck-complete
Logic in Computer Science
2024-06-25 v1 Computational Complexity
Logic
Abstract
We prove that the problem of deciding the consequence relation of the full Lambek calculus with weakening is complete for the class HAck of hyper-Ackermannian problems (i.e., level F_{\omega}^{\omega} of the ordinal-indexed hierarchy of fast-growing complexity classes). Provability was already known to be PSPACE-complete. We prove that deducibility is HAck-complete even for the multiplicative fragment. Lower bounds are proved via a novel reduction from reachability in lossy channel systems and the upper bounds are obtained by combining structural proof theory (forward proof search over sequent calculi) and well-quasi-order theory (length theorems for Higman's Lemma).
Cite
@article{arxiv.2406.15626,
title = {Deducibility in the full Lambek calculus with weakening is HAck-complete},
author = {Vitor Greati and Revantha Ramanayake},
journal= {arXiv preprint arXiv:2406.15626},
year = {2024}
}