Geodesic
Versions of a local contraction subexponential in the Lambek calculus
Algebra i logika, Tome 61 (2022) no. 4, pp. 401-423.

Voir la notice de l'article provenant de la source Math-Net.Ru

The Lambek calculus was introduced as a tool for examining linguistic constructions. Then this calculus was complemented with both new connectives and structural rules like contraction, weakening, and permutation. The structural rules are allowed only for formulas under the symbol of a specific modality called exponential. The Lambek calculus itself is a noncommutative structural logic, and for arbitrary formulas, the structural rules mentioned are not allowed. The next step is the introduction of a system of subexponentials: under the symbol of such a modality, only certain structural rules are admitted. The following question arises: is it possible to formulate a system with a certain version of the local contraction rule (for formulas under subexponential) to recover the cut elimination property? We consider two approaches to solving this problem: one can both weaken the rule of introducing ${!}$ in the right-hand side of a sequent (LSCLC) and extend the local contraction rule from individual formulas to their subsequents (LMCLC). It is also worth mentioning that in commutative calculi, such a problem is missing since formulas in a sequent are allowed to be permuted (i.e, the local contraction rule coincides with the nonlocal one). The following results are proved: cut eliminability in the LMCLC and LSCLC calculi; algorithmic decidability of fragments of these calculi in which ${!}$ is allowed to be applied only to variables; algorithmic undecidability of LMCLC (for LSCLC, decidability remains an open question); correctness and absence of strong completeness of LSCLC with respect to a class of relational models; various results on equivalence for the calculi in question and the calculi with other versions of the contraction subexponential.
Mots-clés : Lambek calculus
Keywords: local contraction subexponential. 
@article{AL_2022_61_4_a1,
     author = {M. V. Valinkin},
     title = {Versions of a local contraction subexponential in the {Lambek} calculus},
     journal = {Algebra i logika},
     pages = {401--423},
     publisher = {mathdoc},
     volume = {61},
     number = {4},
     year = {2022},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/AL_2022_61_4_a1/}
}
TY  - JOUR
AU  - M. V. Valinkin
TI  - Versions of a local contraction subexponential in the Lambek calculus
JO  - Algebra i logika
PY  - 2022
SP  - 401
EP  - 423
VL  - 61
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/AL_2022_61_4_a1/
LA  - ru
ID  - AL_2022_61_4_a1
ER  - 
%0 Journal Article
%A M. V. Valinkin
%T Versions of a local contraction subexponential in the Lambek calculus
%J Algebra i logika
%D 2022
%P 401-423
%V 61
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/AL_2022_61_4_a1/
%G ru
%F AL_2022_61_4_a1
M. V. Valinkin. Versions of a local contraction subexponential in the Lambek calculus. Algebra i logika, Tome 61 (2022) no. 4, pp. 401-423. http://geodesic.mathdoc.fr/item/AL_2022_61_4_a1/

[1] J. Lambek, “The mathematics of sentence structure”, Amer. Math. Mon., 65 (1958), 154–170 ; I. Lambek, “Matematicheskoe issledovanie struktury predlozhenii”, Matematicheskaya lingvistika, sb. per. pod. red. Yu. A. Shreidera i dr., Mir, M., 1964, 47–68 | DOI | MR | Zbl

[2] J.-Y. Girard, “Linear logic”, Theor. Comput. Sci., 50:1 (1987), 1–102 | DOI | MR | Zbl

[3] V. Nigam, D. Miller, “Algorithmic specifications in linear logic with subexponentials”, Proc. 11th int. ACM SIGPLAN conf. Principles and Practice of Declarative Programming (Coimbra, Portugal, September 7-9, 2009), 2009, 129–140

[4] M. Kanovich, S. Kuznetsov, V. Nigam, A. Scedrov, “Subexponentials in non-commutative linear logic”, Math. Struct. Comput. Sci., 29:8 (2019), 1217–1249 | DOI | MR | Zbl

[5] T. Braüner, V. de Paiva, Cut-elimination for full intuitionistic linear logic, BRICS Report RS-96-10, April 1996

[6] M. Kanovich, S. Kuznetsov, A. Scedrov, “Undecidability of the Lambek calculus with a relevant modality”, Formal grammar, 20th and 21st int. conf., FG 2015, FG 2016 (Barcelona, Spain, August 2015; Bozen, Italy, August 2016), Lect. Notes Comput. Sci., 9804, eds. A. Foret et al., Springer, Berlin, 2016, 240–256 | DOI | MR | Zbl

[7] K. Chvalovsky, R. Horčik, “Full Lambek calculus with contraction is undecidable”, J. Symb. Log., 81:2 (2016), 524–540 | DOI | MR | Zbl

[8] H. Andréka, Sz. Mikulás, “Lambek calculus and its relational semantics: completeness and incompleteness”, J. Logic Lang. Inf., 3:1 (1994), 1–37 | DOI | MR | Zbl