论文标题
无限制行动逻辑与凸
Infinitary Action Logic with Exponentiation
论文作者
论文摘要
我们引入了具有指示性的无限动作逻辑 - 也就是说，用克莱恩之星和一个次指数模态延伸的综合添加的lambek微积分，这允许某些结构规则（收缩，弱化，置换，置换）。逻辑以无限序列的演算形式呈现。我们证明了切割消除，如果至少一个次指数允许非本地收缩，则在两种感觉中建立精确的复杂性边界。首先，我们证明此逻辑的衍生性问题为$π_1^1 $ -COMPLETE。其次，我们表明其衍生能力运算符的闭合序列为$ω_1^{\ mathrm {ck}} $。在没有次指数允许收缩的情况下，我们表明复杂性与无限行动逻辑本身相同。也就是说，在这种情况下的衍生性问题为$π^0_1 $ - complete，闭合序列不大于$ω^ω$。
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 $Π_1^1$-complete. Second, we show that the closure ordinal of its derivability operator is $ω_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 $Π^0_1$-complete and the closure ordinal is not greater than $ω^ω$.
