Complexity of Lambek calculi with modalities and of total derivability in grammars

The Lambek calculus with the unit can be defined as the atomic theory (algebraic logic) of the class of residuated monoids. This calculus, being a theory of a broader class of algebras than Heyting ones, is weaker than intuitionistic logic. Namely, it lacks structural rules: permutation, contraction, and weakening. We consider two extensions of the Lambek calculus with modalities — the exponential, under which all structural rules are permitted, and the relevant modality, under which only permutation and contraction rules are allowed. The Lambek calculus with a relevant modality is used in mathematical linguistics. Both calculi are algorithmically undecidable. We consider their fragments in which the modality is allowed to be applied to just formulas of Horn depth not greater than $1$. We prove that these fragments are decidable and belong to the NP class. To show this, in the case of a relevant modality, we introduce a new notion of $\mathcal{R}$-total derivability in context-free grammars, i.e., existence of a derivation in which each rule is used at least a given number of times. It is stated that the $\mathcal{R}$-totality problem is NP-hard for context-free grammars. Also we pinpoint algorithmic complexity of $\mathcal{R}$-total derivability for more general classes of generative grammars.