This article is cited in
8 papers
A restricted fragment of the Lambek calculus with iteration and intersection operations
S. L. Kuznetsova,
N. S. Ryzhkovab a Steklov Mathematical Institute of Russian Academy of Sciences, Moscow
b Lomonosov Moscow State University
Abstract:
The Lambek calculus (a variant of intuitionistic linear logic initially introduced for mathematical linguistics) enjoys natural interpretations over the algebra of formal languages (
$\mathrm{L}$-models) and over the algebra of binary relations which are subsets of a given transitive relation (
R-models). For both classes of models there are completeness theorems (Andréka and Mikulás [J. Logic Lang. Inf.,
3, No. 1 (1994), 1—37]; Pentus [Ann. Pure Appl. Logic,
75, Nos. 1/2 (1995), 179—213;
Fund. Prikl. Mat.,
5, No. 1 (1999), 193—219]). The operations of the Lambek calculus include product and two divisions, left and right. We consider an extension of the Lambek calculus with intersection and iteration (Kleene star). It is proved that this extension is incomplete both w.r.t.
$\mathrm{L}$-models and w.r.t.
$\mathrm{R}$-models. We introduce a restricted fragment, in which iteration is allowed only in denominators of division operations. For this fragment we prove completeness w.r.t.
$\mathrm{R}$-models. We also prove completeness w.r.t.
$\mathrm{L}$-models for the subsystem without product. Both results are strong completeness theorems, that is, they establish equivalence between derivability from sets of hypotheses (finite or infinite) and semantic entailment from sets of hypotheses on the given class of models. Finally, we prove
$\Pi_1^0$-completeness of the algorithmic problem of derivability in the restricted fragment in question.
Keywords:
Lambek calculus, Kleene iteration, algebra of formal languages, algebra of binary relations, complexity of derivability problem.
UDC:
510.649 Received: 30.07.2019
Revised: 14.07.2020
DOI:
10.33048/alglog.2020.59.203
Fulltext:
PDF file (410 kB)
