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

2024/06/21 by Vitor Greati, Greati, Vitor, Revantha Ramanayake +1 · 1 citation
Computer Science · #03B47 #Computability, Logic, AI Algorithms #Computational Complexity (cs.CC) #F.2.2 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.2406.15626

openalex publication_date 2024/06/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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_ω^ω 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).

Cited by

• The Complexity of Nested Reset Counter Systems

Related

• Tower-Complete Problems in Contraction-Free Substructural Logics
• Decidability and Complexity in Weakening and Contraction Hypersequent Substructural Logics
• On the Decidability of (ground) Reachability Problems for Cryptographic Protocols (extended version)
• Completeness and Well-Definability of a Provability Degree Measure in Sufficiently Powerful Formal Systems, and Finite-Time Effective Knowers
• Raising a Hardness Result