Current browse context:
cs.LO
Change to browse by:
References & Citations
Computer Science > Logic in Computer Science
Title: Infinitary Action Logic with Exponentiation
(Submitted on 19 Jan 2020 (v1), last revised 7 Jul 2021 (this version, v3))
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 $\Pi_1^1$-complete. Second, we show that the closure ordinal of its derivability operator is $\omega_1^{\mathrm{CK}}$. 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 $\Pi^0_1$-complete and the closure ordinal is not greater than $\omega^\omega$.
Submission history
From: Stepan Kuznetsov [view email][v1] Sun, 19 Jan 2020 16:55:13 GMT (27kb)
[v2] Thu, 2 Apr 2020 11:48:37 GMT (28kb)
[v3] Wed, 7 Jul 2021 21:49:12 GMT (36kb)
Link back to: arXiv, form interface, contact.