Tikhon Pshenitsyn

In 2023, Kuznetsov and Speranski introduced infinitary action logic with multiplexing $!^{m}\nabla \textrm{ACT}_{\omega }$ and proved that the derivability problem for it lies between the $\omega $ level and the $\omega ^{\omega }$ level of the hyperarithmetical hierarchy. We prove that this problem is $\varDelta ^{0}_{\omega ^{\omega }}$-complete under Turing reductions. Namely, we show that it is recursively isomorphic to the satisfaction predicate for computable infinitary formulas of rank less than $\omega ^{\omega }$ in the language of arithmetic. As a consequence we prove that the closure ordinal for $!^{m}\nabla \textrm{ACT}_{\omega }$ equals $\omega ^{\omega }$. We also prove that the fragment of $!^{m}\nabla \textrm{ACT}_{\omega }$ where Kleene star is not allowed to be in the scope of the subexponential is $\varDelta ^{0}_{\omega ^{\omega }}$-complete. Finally, we present a family of logics, which are fragments of $!^{m}\nabla \textrm{ACT}_{\omega }$, such that the complexity of the $k$-th logic lies between $\varDelta ^{0}_{\omega ^{k}}$ and $\varDelta ^{0}_{\omega ^{k+1}}$.

The class of all $\ast $ -continuous Kleene algebras, whose description includes an infinitary condition on the iteration operator, plays an important role in computer science. The complexity of reasoning in such algebras—ranging from the equational theory to the Horn one, with restricted fragments of the latter in between—was analyzed by Kozen (2002). This paper deals with similar problems for $\ast $ -continuous residuated Kleene lattices, also called $\ast $ -continuous action lattices, where the product operation is augmented by residuals. We prove that, in the presence of residuals, the fragment of the corresponding Horn theory with $\ast $ -free hypotheses has the same complexity as the $\omega ^\omega $ iteration of the halting problem, and hence is properly hyperarithmetical. We also prove that if only commutativity conditions are allowed as hypotheses, then the complexity drops down to $\Pi ^0_1$ (i.e., the complement of the halting problem), which is the same as that for $\ast $ -continuous Kleene algebras. In fact, we get stronger upper bound results: the fragments under consideration are translated into suitable fragments of infinitary action logic with exponentiation, and our upper bounds are obtained for the latter ones.

Lambek categorial grammars is a class of formal grammars based on the Lambek calculus. Pentus proved in 1993 that they generate exactly the class of context-free languages without the empty word. In this paper, we study categorial grammars based on the Lambek calculus with the permutation rule LP. Of particular interest is the product-free fragment of LP called the Lambek-van Benthem calculus LBC. Buszkowski in his 1984 paper conjectured that grammars based on the Lambek-van Benthem calculus (LBC-grammars for short) generate exactly permutation closures of context-free languages. In this paper, we disprove this conjecture by presenting a language generated by an LBC-grammar that is not a permutation closure of any context-free language. Firstly, we introduce an ad-hoc modification of vector addition systems called linearly-restricted branching vector addition systems with states and additional memory (LRBVASSAMs for short) and prove that the latter are equivalent to LBC-grammars. Then we construct an LRBVASSAM that generates a non-semilinear set and thus disprove Buszkowski’s conjecture. Since Buszkowski’s conjecture is false, not so much is known about the languages generated by LBC-grammars or by LP-grammars. The equivalence of LRBVASSAMs and LBC-grammars allows us to establish a number of their properties. We show that LP-grammars generate the same class of languages as LBC-grammars; that is, removing product from LP does not decrease expressive power of corresponding categorial grammars. We also prove that this class of languages is closed under union, intersection, concatenation, and Kleene plus.