RUS  ENG
Full version
SEMINARS

Seminars "Proof Theory" and "Logic Online Seminar"
October 26, 2020 18:30, Moscow, Steklov Mathematical Institute (8 Gubkina), room 313 + Zoom


Decidable fragments of the Lambek calculus with subexponentials

S. L. Kuznetsov


https://youtu.be/cSOae0yVov8

Abstract: The extension of the Lambek calculus with the exponential modality (that is, non-commutative intuitionistic linear logic), is undecidable [Lincoln et al. 1992]. Moreover, the same happens for any subexponential modality, under which the non-local contraction rule is allowed [Kanovich et al. 2019]. However, if the subexponential modality is allowed to be applied only to variables, then the system becomes decidable [Kanovich et al. 2016] and belongs to the NP class, as the original Lambek calculus does. We prove decidability for broader fragments, in which we allow formulae of implication depth 1 under subexponential. (If one allows formulae of depth 2, the system is already undecidable.) We consider such fragments for two versions of subexponential: the exponential, which allows all structural rules, and the relevant modality, which allows contraction and permutation, but not weakening. The latter is motivated by linguistic applications.
Joint work with Boris Karlov and Evgenia Fofanova.

Language: English


© Steklov Math. Inst. of RAS, 2024