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

我们考虑 Lambek 演算（即非交换乘法直觉主义线性逻辑）扩展以迭代或 Kleene 星，通过 $\omega$-规则公理化，并证明该演算中的可推导性问题为 $\Pi_1^0$-困难的。这解决了 Buszkowski（2007）留下的开放问题，他获得了无穷动作逻辑相同的复杂性界，该逻辑还额外包含加法合取与析取。作为副产品，我们证明任何不含空词的上文无关语言均可由具有唯一类型赋值的 Lambek 文法生成，且不施加 Lambek 的非空限制（参见 Safiullin 2007）。