Lambek calculus extended with subexponential and bracket modalities

The Lambek calculus (1958, 1961) is a well-known logical formalism for modelling natural language syntax. The calculus can also be considered as a version of non-commutative intuitionistic linear logic. The Lambek calculus is a logical foundation of categorial grammar, a linguistic paradigm of grammar as logic and parsing as deduction. The original calculus covered a substantial number of intricate natural language phenomena. In order to address more subtle linguistic issues, the Lambek calculus has been extended in various ways.
For instance, an extension with so-called bracket modalities introduced by Morrill (1992) and Moortgat (1995) is capable of representing controlled non-associativity and is suitable for the modeling of islands. The syntax is more involved than the syntax of a standard sequent calculus. Derivable objects are sequents of the form Gamma $\to$ A , where the antecedent Gamma is a structure called meta-formula and the succedent A is a formula. Meta-formulae are built from formulae (types) using two metasyntactic operators: comma and brackets.
Morrill and Valentin (2015) introduce a further extension with so-called exponential modality, suitable for the modeling of medial and parasitic extraction. Their extension is based on a non-standard contraction rule for the exponential, which interacts with the bracket structure in an intricate way. The standard contraction rule for exponentials is not admissible in this calculus. In joint work with Max Kanovich and Stepan Kuznetsov we show that provability in this calculus is undecidable and we investigate restricted decidable fragments considered by Morrill and Valentin. We show that these fragments belong to NP.