Logic Colloquium 2024


Vitor Greati

Bernoulli Institute, Nijenborgh 9, 9747 AG, University of Groningen, The Netherlands

Talks at this conference:

  Thursday, 17:50, J222

Knotted substructural logics have fast-growing complexity

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).