Infinitary Action Logic with Exponentiation

DOI10.1016/J.APAL.2021.103057arXiv2001.06863MaRDI QIDQ6333136FDOQ6333136

Authors: Stepan Kuznetsov, S. O. Speranskij 

Publication date: 19 January 2020

Abstract: We introduce infinitary action logic with exponentiation -- that is, the multiplicative-additive Lambek calculus extended with Kleene star and with a family of subexponential modalities, which allows some of the structural rules (contraction, weakening, permutation). The logic is presented in the form of an infinitary sequent calculus. We prove cut elimination and, in the case where at least one subexponential allows non-local contraction, establish exact complexity boundaries in two senses. First, we show that the derivability problem for this logic is $P{i}_1^1$-complete. Second, we show that the closure ordinal of its derivability operator is $omeg{a}_1^{mathrmCK}$. In the case where no subexponential allows contraction, we show that complexity is the same as for infinitary action logic itself. Namely, the derivability problem in this case is $P{i}_1^0$-complete and the closure ordinal is not greater than $omeg{a}^{o}mega$.

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Other infinitary logic (03C75) Undecidability and degrees of sets of sentences (03D35)

This page was built for publication: Infinitary Action Logic with Exponentiation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6333136)