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

TL;DR

This paper establishes that deducibility in the full Lambek calculus with weakening is HAck-complete, indicating extremely high computational complexity, even for its multiplicative fragment, through novel reductions and proof-theoretic techniques.

Contribution

It proves HAck-completeness of deducibility in the calculus, extending known PSPACE-completeness results with new complexity bounds and reduction methods.

Findings

Deducibility is HAck-complete for the full Lambek calculus with weakening.

Lower bounds are established via reduction from reachability in lossy channel systems.

Upper bounds are achieved through structural proof theory and well-quasi-order theory.

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).