Deducibility in the full Lambek calculus with weakening is HAck-complete
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913401546997760 |
|---|---|
| author | Greati, Vitor Ramanayake, Revantha |
| author_facet | Greati, Vitor Ramanayake, Revantha |
| contents | 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). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_15626 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Deducibility in the full Lambek calculus with weakening is HAck-complete Greati, Vitor Ramanayake, Revantha Logic in Computer Science Computational Complexity Logic 03B47 F.4.1; F.2.2 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). |
| title | Deducibility in the full Lambek calculus with weakening is HAck-complete |
| topic | Logic in Computer Science Computational Complexity Logic 03B47 F.4.1; F.2.2 |
| url | https://arxiv.org/abs/2406.15626 |