Complexities of Well-Quasi-Ordered Substructural Logics

TL;DR

This work analyzes the computational complexity of deducibility and provability across a broad family of substructural logics with well-quasi-ordered semantics. It develops a uniform methodology that combines proof theory via hypersequent calculi, algebraic semantics through residuated lattices, and relational semantics with residuated frames to obtain decidability (via FEP) and precise upper bounds in ordinal-indexed fast-growing classes. The study reveals that introducing knotted axioms and weak exchange drives complexities up to Ackermannian and hyper-Ackermannian scales, while certain systematic restrictions (e.g., weak exchange with knotted contraction, integrality) cap complexity at lower, still substantial levels. These results illuminate how small design choices in resource-sensitive logics drastically influence algorithmic behavior and provide a robust toolkit for future exploration of the intersection between substructural proof theory, universal algebra, and complexity theory.

Abstract

Substructural logics are formal logical systems that omit familiar structural rules of classical and intuitionistic logic such as contraction, weakening, exchange (commutativity), and associativity. This leads to a resource-sensitive logical framework that has proven influential beyond mathematical logic and its algebraic semantics, across theoretical computer science, linguistics, and philosophical logic. The set of theorems of a substructural logic is recursively enumerable and, in many cases, recursive. These logics also possess an intricate mathematical structure that has been the subject of research for over six decades. We undertake a comprehensive study of substructural logics possessing an underlying well-quasi-order (wqo), using established ordinal-indexed fast-growing complexity classes to classify the complexity of their deducibility (quasiequational) and provability (equational) problems. This includes substructural logics with weak variants of contraction and weakening, and logics with weak or even no exchange. We further consider infinitely many axiomatic extensions over the base systems. We establish a host of decidability and complexity bounds, many of them tight, by developing new techniques in proof theory, well-quasi-order theory (contributing new length theorems), the algebraic semantics of substructural logics via residuated lattices, algebraic proof theory, and novel encodings of counter machines. Classifying the computational complexity of substructural logics (and the complexity of the word problem and of the equational theory of their algebraic semantics) reveals how subtle variations in their design influence their algorithmic behavior, with the decision problems often reaching Ackermannian or even hyper-Ackermannian complexity.

Figures (5)

• Figure 1: Hilbert calculus for the Full Lambek logic.
• Figure 2: The hypersequent calculus $\mathbf{HFL}_{}$ for $\mathbf{FL}_{}$.
• Figure 3: Some hypersequent analytic structural rule schemas in presence of exchange, including the rules $\mathsf k({m},{n})$ that realize the knotted extensions. Below each rule is the corresponding axiom and below that is its pair $(\text{formula multiplicity},\text{active component number})$. Note: $(\varphi)_{\land 1}$ is notation for $(\varphi\land 1)$.
• Figure 4: In each picture, the set $H$ is a hyperplane containing the points $\vec{m}_1,\ldots,\vec{m}_k$ corresponding to the joinands of $\varepsilon$ and the vector $\mathbf{n}$ has non-negative integer entries and lies normal to $H$; i.e., $H$ is the solution set to the linear system $\mathbf{n}^\top\mathbf{x} = b$ for some integer $b\geq 0$. The plane $\mathbb{N}^n$ is a disjoint union of the sets $H: \mathbf{n}^\top \mathbf{x} = b$, $H^-: \mathbf{n}^\top \mathbf{x} < b$, and $H^+: \mathbf{n}^\top \mathbf{x} > b$. The shaded regions represent the negative and positive cones with vertex $\vec{m}_0$, respectively denoted by sets ${\downarrow}{\vec{m}_0}$ and ${\uparrow}{\vec{m}_0}$. For $\sigma$ the substitution $x_i\mapsto x^{\mathbf{n}(i)}$, $\sigma(\varepsilon)$ is the equation $x^a\leq x^b$ where $a = \mathbf{n}^\top \vec{m}_0$. The case (a) shows when $\vec{m}_0\in H^-$, in which case $a<b$ and $\sigma(\varepsilon)$ is a knotted contractive equation; moreover, $\varepsilon$ is joinand-increasing iff $\{\vec{m}_1,\ldots ,\vec{m}_k\}\cap {\uparrow}\vec{m}_0 \neq \varnothing$. The case (b) shows when $\vec{m}_0\in H^+$, in which case $a>b$ and $\sigma(\varepsilon)$ is a knotted weakening equation; moreover, $\varepsilon$ is joinand-decreasing iff $\{\vec{m}_1,\ldots ,\vec{m}_k\}\cap {\downarrow} \vec{m}_0 \neq \varnothing$. The case (c) shows when $\vec{m}_0\in H$, in which case $a=b$ and $\sigma(\varepsilon)$ is trivial.
• Figure :

Theorems & Definitions (240)

• Remark 2.1
• Definition 2.2
• Example 2.3
• Remark 2.4
• Remark 2.5
• Definition 2.6
• Lemma 2.7
• Lemma 2.8
• Remark 2.9
• Example 2.10