Speaker

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