### Deducibility in the full Lambek calculus with weakening is HAck-complete

Proceeding of AiML (to appear)

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 \(\mathbf{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).