Substructural logics are

obtained from classical logic and intuitionistic logic (\(\mathbf{IL}\)) by rejecting axioms corresponding to familiar structural properties

like exchange (\(\mathbf e\)), weakening (\(\mathbf w\)) and contraction (\(\mathbf c\)).

Such logics exhibit resource-awareness and this additional expressivity is well-suited for applications in

mathematics, computer science, linguistics and philosophy.

For the same reason, these logics tend to be computationally very challenging. This is best illustrated by the decision problems of provability (the input formula is provable) and deducibility (the input formula is provable from an input set of formulas). For example, removing \((\mathbf c)\) from \(\mathbf{IL}\) yields a logic whose provability is PSPACE-complete, and deducibility is {TOWER}-complete (i.e., non-elementary). Remove \((\mathbf e)\) and \((\mathbf w)\) instead and both problems are undecidable.

Removing just \((\mathbf w)\) from \(\mathbf{IL}\) yields a logic whose provability and deducibility are both Ackermannian-complete (i.e., non-primitive recursive, at level \(\mathbf{F}_\omega\) in the ordinal-indexed fast-growing hierarchy).

We have already seen how the computational status varies with different combinations of structural properties. In this work, we discuss a natural family of logics arising when replacing \((\mathbf c)\) and \((\mathbf w)\) in \(\mathbf{IL}\) with a knotted axiom \(p^m \to p^n\). These logics possess analytic proof calculi but their analysis is impeded by size-increasing rules and the heavy combinatorial nature of the proofs.

Specifically, we study the complexity of axiomatic extensions of the full Lambek logic \(\mathbf{FL}\) (that is, \(\mathbf{IL}\) minus \(\{(\mathbf e), (\mathbf w), (\mathbf c) \})\) with knotted axioms yielding fast-growing complexity classifications. A key feature here is the reliance on multiple areas of mathematics and computer science: proof theory and well-quasi-order theory for deriving upper bounds, and reductions using algebraic counter machines to obtain lower bounds.

Joint work with Nikolaos Galatos (Denver), Revantha Ramanayake (Groningen), and Gavin St. John (Salerno).