On Involutive Nonassociative Lambek Calculus

Involutive Nonassociative Lambek Calculus (InNL) is a nonassociative version of Noncommutative Multiplicative Linear Logic (MLL) (Abrusci in J Symb Log 56:1403–1451, 1991), but the multiplicative constants are not admitted. InNL adds two linear negations to Nonassociative Lambek Calculus (NL); it is a strongly conservative extension of NL (Buszkowski in Amblard, de Groote, Pogodalla, Retoré (eds) Logical aspects of computational linguistics. LNCS, vol 10054. Springer, Berlin, pp 68–84, 2016). Here we also add unary modalities satisfying the residuation law and De Morgan laws. For the resulting logic InNLm, we define and study phase spaces (some frame models, typical for linear logics). We use them to prove the cut elimination theorem for a one-sided sequent system for InNLm, introduced here. Phase spaces are also employed in studying auxiliary systems InNLm(k), assuming the k-cyclic law for negation. The latter behave similarly as Classical Nonassociative Lambek Calculus, studied in de Groote and Lamarche (Stud Log 71(3):355–388, 2002) and Buszkowski (2016). We reduce the provability in InNLm to that in InNLm(k). This yields the equivalence of type grammars based on InNLm with ( $$\epsilon $$ -free) context-free grammars and the PTIME complexity of InNLm.