带 Kleene 星的无穷 Lambek 演算的复杂性

The Lambek calculus with iteration: two variants

Formulae of the Lambek calculus are constructed using three binary connectives, multiplication and two divisions. We extend it using a unary connective, positive Kleene iteration. For this new operation, following its natural interpretation, we present two lines of calculi. The first one is a fragment of infinitary action logic and includes an omega-rule for introducing iteration to the antecedent. We also consider a version with infinite (but finitely branching) derivations and prove equivalence of these two versions. In Kleene algebras, this line of calculi corresponds to the *-continuous ca…

Infinitary Action Logic with Exponentiation

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 t…

带交集与常量的Lambek演算的关系模型

Relational Models for the Lambek Calculus with Intersection and Constants

本文研究了带交集与常量的Lambek演算的关系语义，证明禁止空前件限制下强完备性失效，但为常量非标准解释证明了弱完备性，并扩展至迭代除法及无积片段。

Action Logic is Undecidable

Action logic is the algebraic logic (inequational theory) of residuated Kleene lattices. This logic involves Kleene star, axiomatized by an induction scheme. For a stronger system which uses an $ω$-rule instead (infinitary action logic) Buszkowski and Palka (2007) have proved $Π_1^0$-completeness (thus, undecidability). Decidability of action logic itself was an open question, raised by D. Kozen in 1994. In this article, we show that it is undecidable, more precisely, $Σ_1^0$-complete. We also prove the same complexity results for all recursively enumerable logics between action logic and infi…

无穷作用逻辑的代数证明理论

Algebraic Proof Theory for Infinitary Action Logic

本文提出一种统一方法，通过结合非良基证明理论与代数证明理论工具，为各类 *-连续作用代数构建可靠完备的无切序列式证明系统。

带多路复用的无穷动作逻辑的超算术复杂度

Hyperarithmetical Complexity of Infinitary Action Logic with Multiplexing

本文针对带多路复用的无穷动作逻辑$!^m\nabla \mathrm{ACT}_\omega$的可推导性问题，证明其在图灵归约下为$\Delta^0_{\omega^\omega}$-完全，确定其闭包序数为$\omega^\omega$，并给出相关片段的复杂度结果。