Complexities of Well-Quasi-Ordered Substructural Logics

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.