GroLog Seminar

SPEAKER: Nick Galatos (University of Denver)

DATE: Monday 26 October 2026

TIME: 16:00-17:00

PLACE: BernoulliBorg, room 5161.0289

TITLE: Computational complexity for knotted substructural logics: lower bounds

ABSTRACT: 

Substructural logics are resource-sensitive generalizations of classical and intuitionistic logic. In particular, they may lack the (structural) properties of exchange, weakening and contraction, so the order and multiplicity of assumptions is important in a derivation. As a result, they are useful, among other things, in studying degrees of truth and settings where various information tokens are received or where the order of formulas is important (non-Abelian groups, sentence structure in linguistics).

Knotted axioms reinstate some (controlled and specified) degree of the structural properties of contraction and weakening back in the logic, which may be suitable for certain settings. The deductibility of knotted substructural logics is known to be undecidable when exchange is fully absent and decidable when exchange (or weaker versions of it) is present. In our work, we establish the exact computational complexity of these logics in cases when they are decidable: we prove that this complexity class is exactly Ackermaniann (the first non-elementary complexity class).

In this talk we present the methods used to obtain the lower complexity bounds. In particular, we show hardness with respect to this complexity class by encoding the termination problem for and-branching counter machines that have an Ackermaniann memory limit. Actually, our results apply to more general axioms than knotted ones (joinand-increasing and joinand-decreasing) and to specific weaker versions of exchange. Finally, we show that for knotted rules of contractive type, provability has the same complexity as deducibility.

(Joint work with V. Greati, R. Ramanayake and G. St. John.)