Vitor Greati

Substructural logics lack structural properties like weakening, contraction, associativity, or exchange (commutativity) that are familiar from classical and intuitionistic logic. The omission of such properties make these logics well-suited for reasoning about resources in various different senses. Substructural logics appear across theoretical computer science, linguistics, and philosophy, and they possess an intricate mathematical and logical structure. For the same reasons, these logics exhibit vast computational diversity including membership in (ordinal-indexed) fast-growing complexity classes. Here we consider substructural logics with weak versions of the usual contraction or weakening rules (collectively referred to as knotted axioms in the literature), and infinitely many of their axiomatic extensions. A host of new decidability and complexity upper bounds are established by exploiting the underlying knotted well-quasi-orders (wqos) and drawing on techniques from proof theory and wqo theory, contributing also with new length theorems in controlled bad sequences for knotted wqos and their power set extensions.