A restricted fragment of the Lambek calculus with iteration and intersection operations

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.