Circular and infinitary proofs for complexity analysis of action logic

Action logic is the extension of the full Lambek calculus (intuitionistic-style non-commutative substructural logic) with the operation of Kleene iteration. The natural algebraic semantics for action logic is given by residuated Kleene lattices (RKLs). Action logic appears in two variants: the logic of all RKLs (action logic itself), with an inductive axiomatisation for iteration, and a stronger infinitary system, where iteration is governed by an omega-rule. The latter corresponds to the natural subclass of *-continuous RKLs. In this talk, we discuss how calculi with circular and infinitary proofs help analyse algorithmic complexity for theoremhood and entailment from hypotheses in action logic and its infinitary extension. Namely, using circular proofs we show $\Sigma^0_1$-completeness of action logic. The theoremhood problem in infinitary action logic is $\Pi^0_1$-complete. For entailment from *-free hypotheses in the latter, we get an $\omega^\omega$ upper bound on the closure ordinal (for the system with an omega-rule) and the corresponding hyperarithmetical complexity bound, which is actually exact. Finally, entailment from arbitrary hypotheses in infinitary action logic is $\Pi^1_1$-complete, the closure ordinal being $\omega_1^{CK}$.
Partially based on joint work with Tikhon Pshenitsyn and Stanislav Speranski.