On Involutive Nonassociative Lambek Calculus
 258 Downloads
Abstract
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 onesided sequent system for InNLm, introduced here. Phase spaces are also employed in studying auxiliary systems InNLm(k), assuming the kcyclic 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) contextfree grammars and the PTIME complexity of InNLm.
Keywords
Lambek calculus Linear logic Phase space Sequent system Type grammar Contextfree grammar1 Introduction and Preliminaries
1.1 Overview
This paper contributes to the study of nonassociative linear logics, essentially weaker than noncommutative linear logics, studied in Yetter (1990) and Abrusci (1991). Furthermore, we consider logics without multiplicative constants 1, 0 [0 is \(\bot \) in the notation of linear logics (Girard 1987; Yetter 1990; Abrusci 1991)]. Our logics have models whose product and par do not admit the unit elements. These logics were not much studied earlier. de Groote and Lamarche (2002) studied Classical Nonassociative Lambek Calculus (CNL) which amounts to Nonassociative Lambek Calculus (NL), due to Lambek (1961), augmented with negation \(^{\bot }\), satisfying (in algebras) the double negation law \(a^{\bot \bot }= a\) and some other laws (see below). This purely prooftheoretic paper, focusing on proof nets for CNL, provided a sequent system for CNL and proved: (1) CNL is a conservative extension of NL, (2) CNL is PTIME.
Buszkowski (2016) studies algebras and phase spaces for CNL and uses them to prove some new results: (1) CNL is strongly conservative over NL (this means: both logics yield the same consequence relation in the language of NL), (2) type grammars based on CNL are equivalent to \(\epsilon \)free contextfree grammars (CFGs), (3) the finitary consequence relation for CNL is PTIME. Earlier, analogous results were obtained for NL (Buszkowski 2005).
The present paper focuses on a weaker logic, called Involutive Nonassociative Lambek Calculus (InNL), which amounts to NL augmented with two negations \(^{\sim },^{}\), satisfying (in algebras) the double negation laws \(a^{\sim }=a=a^{\sim }\) and some contraposition laws. InNL is a nonassociative version of Noncommutative MLL from Abrusci (1991) but without multiplicative constants, while CNL is an analogous version of Cyclic Noncommutative MLL from Yetter (1990). In Buszkowski (2016) InNL is denoted by CNL\(^{}\). Not all tools applied in the study of CNL can be applied for InNL; in particular, a finite set of formulas cannot be closed under negations in finitely many steps.
Buszkowski (2017a) introduces and studies a onesided sequent system for InNL and proves the cutelimination theorem in a syntactic way. The paper also shows that InNL is PTIME. Phase spaces are not employed. Here this research is continued. We consider a richer logic InNLm, i.e. InNL with (unary) modalities, which form a residuation pair. We study phase spaces for InNLm and use them in modeltheoretic proofs of the completeness and the cutelimination theorems for the sequent system. We also prove the PTIME complexity of InNLm with the aid of auxiliary logics InNLm(k); the corresponding algebras support the kcyclic laws \(a^{\sim \cdots \sim }=a\), where \(\sim \) is iterated k times (k is even). We prove that type grammars based on InNLm are equivalent to \(\epsilon \)free CFGs.
Warning In this paper we do not follow the notation of linear logics, due to Girard (1987), where e.g. \(\oplus \) stands for additive disjunction (here \(\vee \)). Our notation follows the standards of substructural logics (Galatos et al. 2007).
All results of this paper hold for InNL: it suffices to omit modalities, the operation f (in frames) and angle brackets in all systems and proofs. Furthermore, all results of this paper remain true for InNL and InNLm with multiplicative constants 1, 0, but we skip almost all details to keep the paper in a reasonable size. These results also hold for multimodal versions of these systems, containing several modalities \(\Diamond _{i},\Box ^{\downarrow }_{i}\) and several Lambek connectives \(\otimes _{i},\backslash _{i},/_{i}\). Some linguistic applications are discussed later in this section.
This paper extends the conference paper (Buszkowski 2017b), which studies phase spaces for InNL only (modalities are not considered) and provides some results of Sect. 4 (restricted to InNL(k)) without proof. No result of the present paper was published earlier.
1.2 Algebras
A residuated semigroup is a residuated groupoid such that \(\otimes \) is associative. Residuated semigroups are models of (associative) Lambek Calculus (L), due to Lambek (1958).
 (RG1)

\(a\otimes (a\backslash b)\le b\), \((a/b)\otimes b\le a\,\) (application laws),
 (RG2)

\(a\le b\backslash (b\otimes a)\), \(a\le (a\otimes b)/b\,\) (coapplication laws),
 (MON)

if \(a\le b\) then \(c\otimes a\le c\otimes b\), \(a\otimes c\le b\otimes c\), \(c\backslash a\le c\backslash b\), \(a/c\le b/c\), \(b\backslash c\le a\backslash c\), \(c/b\le c/a\,\) (monotony laws).
 (RGm)

\(a\le \Box ^{\downarrow }\Diamond a\), \(\Diamond \Box ^{\downarrow }a\le a\),
 (MONm)

if \(a\le b\) then \(\Diamond a\le \Diamond b\) and \(\Box ^{\downarrow }a\le \Box ^{\downarrow }b\).
 (DN)

\(a^{\sim }=a=a^{\sim }\),
 (CON)

\(a^{\sim }/b=a\backslash b^{}\),
 (COMP)

\(a\otimes b\le c^{}\) iff \(b\otimes c\le a^{\sim }\), for all \(a,b,c\in M\).
(CON) stipulates a connection between negations and Lambek operations. One derives other contraposition laws: \(a\backslash b=a^{\sim }/b^{\sim }\), \(a/b=a^{}\backslash b^{}\).
 (IRG1)

\((a\otimes b)^{\sim }=b^{\sim }\oplus a^{\sim }\), \((a\otimes b)^{}=b^{}\oplus a^{}\) (De Morgan laws),
 (IRG2)

\(a\backslash b=a^{\sim }\oplus b=(b^{}\otimes a)^{\sim }\), \(a/b=a\oplus b^{}=(b\otimes a^{\sim })^{}\),
 (IRG3)

\(a\oplus b=a^{}\backslash b=a/b^{\sim }\).
Therefore, in involutive residuated groupoids, all operations can be expressed in terms of \(\otimes \) and negations. The onesided sequent systems, considered later on, admit the language \(\otimes ,\oplus ,^{\sim },^{}\) (negations at variables only).
 (DMm)

\((\Diamond a)^{\sim }=\Box ^{\downarrow }(a^{\sim })\), \((\Diamond a)^{}=\Box ^{\downarrow }(a^{})\), for any element a.
 (COMPm)

\(\Diamond a\le b^{}\) iff \(\Diamond b\le a^{\sim }\), for any elements a, b,
If a residuated groupoid contains an element 1, satisfying \(1\otimes a=a=a\otimes 1\) for any element a, it is called unital. In involutive unital residuated groupoids, \(1^{\sim }=1^{}\), and one defines \(0=1^{\sim }\). One easily shows \(0\oplus a=a=a\oplus 0\), \(a^{\sim }=a\backslash 0\), \(a^{}=0/a\).
1.3 Intuitionistic Sequent Systems
Our logics can be presented as intuitionistic sequent systems.
Using LindenbaumTarski algebras, one easily shows that NL is strongly complete with respect to residuated groupoids and InNL (resp. CNL) with respect to (resp. cyclic) involutive residuated groupoids. Recall that a valuation in an algebra \({\mathbf {M}}\) is a homomorphism from the formula algebra to \({\mathbf {M}}\). It is extended for bunches by interpreting each comma as product. \(\Gamma \Rightarrow A\) is true for a valuation \(\mu \) in \({\mathbf {M}}\) if \(\mu (\Gamma )\le \mu (A)\). The strong completeness means: the sequents provable in the logic from a set of sequents \(\Phi \) (a set of assumptions, not closed under substitutions) are precisely those which follow from \(\Phi \) in the corresponding algebras (they are true for any algebra \({\mathbf {M}}\) and valuation \(\mu \) such that all sequents from \(\Phi \) are true).
1.4 Type Grammars
We define type grammars. Let \({\mathcal {L}}\) be a logic, which yields provable sequents of the form \(\Gamma \Rightarrow A\). The formulas of \(\mathcal L\) are referred to as types. By a type grammar based on \({\mathcal {L}}\) we mean a triple \(G=(\Sigma ,I,A_{0})\) such that \(\Sigma \) is a nonempty finite alphabet (lexicon), I (the type lexicon) is a map which assigns a finite set of types to any \(v\in \Sigma \), and \(A_{0}\) is a type (the designated type). Usually, one takes an atomic type for \(A_{0}\), e.g. s—the type of sentence (statement). We define a basic notion: G assigns a type A to a string \(u\in \Sigma ^{+}\) (write: u : A in G); the definition depends on the form of sequents. For logics without modalities, \(v_{1}\ldots v_{n}:A\) in G, if there exist types \(A_{i}\in I(v_{i})\), for \(i=1,\ldots ,n\), and a bunch \(\Gamma \) such that \(\Gamma \Rightarrow A\) is provable in \({\mathcal {L}}\) and \((A_{1},\ldots ,A_{n})\) is the sequence resulting from \(\Gamma \), after one has dropped all bunch parentheses (i.e. the yield of \(\Gamma \)). (For associative logics, like L, one simply states: \(A_{1},\ldots ,A_{n}\Rightarrow A\) is provable.) For logics with modalities, we admit the same definition, but we additionally require that \(\Gamma \) does not contain angle brackets. This is natural: one can ignore the phrase structure (the tree structure) on the string, but not the modal structure. Otherwise a grammar (based on NLm) assigning s to v would also assign \(\Diamond s\) to v, since \(\langle s\rangle \Rightarrow \Diamond s\) is provable in NLm, by (NLid) and (\(\Rightarrow \Diamond \)), though \(s\Rightarrow \Diamond s\) is not provable in NLm. The latter is provable in a stronger logic, namely NLm with the axiom (T) \(A\Rightarrow \Diamond A\).
By the language ofG (or: generated by G, recognized by G) we mean the set of all \(u\in \Sigma ^{+}\) such that \(u:A_{0}\) in G; this language is denoted by L(G). If G is based on a nonassociative logic, like NL, InNL, etc., then the bunch structure of \(\Gamma \) induces a tree structure (phrase structure) on the generated string. Accordingly, such grammars naturally describe languages of phrase structures rather than languages of strings, and the latter are obtained from the former by neglecting the structure.
This paper is concerned with mathematical foundations of some logics connected with type grammars (also interesting for themselves). It cannot discuss in detail applications in natural language processing. We only briefly point out some main lines.
Basic Categorial Grammars, tracing back to Ajdukiewicz (1935), BarHillel et al. (1960), employ a minimal logic, based on the application laws \(A,A\backslash B\Rightarrow B\), \(A/B,B\Rightarrow A\). Thus, under the type lexicon ‘John’: np, ‘Mary’: np, ‘likes’: \((np\backslash s)/np\), one derives ‘John likes Mary’: s with the induced tree structure (John (likes Mary)); np is the type of noun phrase. This logic can be axiomatized as a fragment of NL, admitting (NLid) and the left introduction rules for \(\backslash ,/\). Lambek (1958) considers a stronger logic, nowadays called Lambek Calculus (L), which yields new laws, e.g. \(A\backslash B,B\backslash C\Rightarrow A\backslash C\), \(A/B,B/C\Rightarrow A/C\) (composition laws). Now, with ‘he: \(s/(np\backslash s)\), ‘her’: \((s/np)\backslash s\), one derives ‘he likes her’: s. Due to the associativity of product. the type grammars based on L are not sensitive to the tree structure of the generated string. Therefore, many linguists prefer nonassociative logics like NL. To improve the expressivity power of these logics one enriches them with unary modalities \(\Diamond ,\Box ^{\downarrow }\); the multimodal framework, elaborated in Moortgat (1996), Morrill (1994), Moortgat (1997) and Moot and Retoré (2012), admits several pairs of unary modalities and several binary products with the corresponding residuals. One assumes some restricted associativity and commutativity laws for modal formulas, which makes it possible to apply the corresponding structural rules in a controlled manner. This resembles Girard’s usage of exponentials in linear logics (Girard 1987).
Logics with linear negations are much richer, but they are conservative extensions of their negationfree fragments. It was shown in Buszkowski (2016) that CNL is a strongly conservative extension of NL; earlier de Groote and Lamarche (2002) had shown that CNL is a conservative extension of NL (that means: every NLsequent provable in CNL is provable in NL). Since InNL is intermediate between NL and CNL, it is also a strongly conservative extension of NL. Also CNLm is a strongly conservative extension of NLm, hence the same holds for InNLm.
This implies that every type grammar based on NL (resp. NLm) can be treated as a grammar based on InNL or CNL (resp. InNLm, CNLm), with no change of the generated language (this remains true, if one adds some nonlogical axioms to the former logic). The richer logic offers a more interesting proof machinery and often more symmetries. For instance, in InNL, the application laws are dual to the coapplication laws by the basic duality: \(A\Rightarrow B\) iff \(B^{\sim }\Rightarrow A^{\sim }\) iff \(B^{}\Rightarrow A^{}\), which cannot be expressed in NL. In the algebraic notation: \(a\otimes (a\backslash b)\le b\) iff \(b^{}\le (a\backslash b)^{}\oplus a^{}\) iff \(b^{}\le (b^{}\otimes a)/a\).
Some sample types in different formalisms
Word  NLtype  InNLtype  CBLtype 

works  \(np\backslash s\)  \(np^{\sim }\oplus s\)  \([np]^{r}s\) 
likes  \((np\backslash s)/np\)  \((np^{\sim }\oplus s)\oplus np^{}\)  \([np]^{r}s[np]^{l}\) 
whom  \((n\backslash n)/(s/np)\)  \((n^{\sim }\oplus n)\oplus (np^{{}{}}\otimes s^{})\)  \(n^{r}n[np]^{ll}s^{l}\) 
Linear logics strongly influenced some current ideas in type grammars. Proof nets are interpreted as logical forms of expressions (Moot and Retoré 2012). Unary modalities enable one to apply structural rules in a controlled manner. Some authors maintain logics intermediate between NL or L and MLL. Moortgat (2009) considers an extension of NL with \(\oplus \), its (dual) residuals and some mixed associativity and commutativity axioms, due to Grishin (1983), under the name Lambek–Grishin Calculus (LG). The corresponding type grammars are called symmetric categorial grammars. Bastenhof (2013) provides a detailed study of these grammars (also see Sect. 3). All new axioms of LG are provable in the associative and commutative version of InNL.
1.5 Contents
The present paper aims to develop the theory of nonassociative multiplicative linear logics, which—as it has been explained above—are very close to some basic logics of type grammars. Besides their possible applications in linguistics, they seem interesting for themselves. Nonassociative logics are more efficient than their associative versions; the latter are NPcomplete (Pentus 2006), whereas the former are PTIME. From the theoretical perspective, the study of these weaker logics throws some new light on the whole area. For instance, our notion of a phase space exhibits an essentially modal character of linear negations.
This paper is organized as follows. In Sect. 2 we define and discuss phase spaces for InNLm. Section 3 studies a onesided sequent system for InNLm; the cutelimination theorem is proved in a modeltheoretic way. Section 4 concerns auxiliary logics InNLm(k). With the aid of them we show that InNLm is PTIME and the type grammars based on InNLm are equivalent to the \(\epsilon \)free CFGs.
2 Phase Spaces
A closure operation C on \({{\mathcal {P}}}(M)\) is called a nucleus, if it satisfies: (C4) \(C(X)\cdot C(Y)\subseteq C(X\cdot Y)\), (C5) \(\Diamond C(X)\subseteq C(\Diamond X)\), for all \(X,Y\subseteq M\). Assuming (C1)–(C3), (C4) is equivalent to: (C4\('\)) for any Cclosed set X and any \(Y\subseteq M\), the sets \(Y\backslash X\) and X / Y are Cclosed, and (C5) to: (C5\('\)) for any Cclosed set X, \(\Box ^{\downarrow }X\) is Cclosed (Buszkowski 2011). We show that (C4\('\)) entails (C4). From \(X\cdot Y\subseteq C(X\cdot Y)\) we get \(Y\subseteq X\backslash C(X\cdot Y)\), hence \(C(Y)\subseteq X\backslash C(X\cdot Y)\) by (C2) and (C4\('\)). This yields \(X\cdot C(Y)\subseteq C(X\cdot Y)\). So \(X\subseteq C(X\cdot Y)/C(Y)\), hence \(C(X)\subseteq C(X\cdot Y)/C(Y)\), which yields (C4). We show that (C5\('\)) entails (C5). From \(\Diamond X\subseteq C(\Diamond X)\) we get \(X\subseteq \Box ^{\downarrow }C(\Diamond X)\), hence \(C(X)\subseteq \Box ^{\downarrow }C(\Diamond X)\), by (C2) and (C5\('\)). This yields (C5), by (URES).
Let \((M,\cdot , f)\), be as above, and let C be a closure operation on \({{\mathcal {P}}}(M)\). By \(M_{C}\) we denote the family of Cclosed subsets of M. \(M_{C}\) is closed under infinite meets (intersections), hence it is a complete lattice. For \(X,Y\in M_{C}\) one defines: \(X\otimes _{C}Y=C(X\cdot Y)\), \(\Diamond _{C}X=C(\Diamond X)\), and \(X/Y, X\backslash Y\), \(\Box ^{\downarrow }\) as above. If C is a nucleus, then \(M_{C}\) with these operations (restricted to \(M_{C}\)) and \(\subseteq \) is a modal residuated groupoid. We show (URES). Let \(X,Y\in M_{C}\). Assume \(\Diamond _{C}X\subseteq Y\). Then, \(\Diamond X\subseteq Y\), by (C1), hence \(X\subseteq \Box ^{\downarrow }Y\). Assume \(X\subseteq \Box ^{\downarrow }Y\). Then, \(\Diamond X\subseteq Y\), hence \(\Diamond _{C}X\subseteq Y\), by (C2), since \(Y\in M_{C}\).
 (Shift)

for all \(a,b,c\in M\), \(R(a\cdot b,c)\) iff \(R(a,b\cdot c)\).
 (mShift)

for all \(a,b\in M\), R(f(a), b) iff R(a, f(b)).
For any phase space \((M,\cdot ,f,R)\), R is symmetric if and only if \(X^{\sim }=X^{}\) for any \(X\subseteq M\). Consequently, if R is symmetric, then \(\phi _{R}=\psi _{R}\). So every phase space for CNLm (resp. CNL) is a phase space for InNLm (resp. InNL).
The following lemma shows that, in general, (Shift) yields (CON) in the powerset algebra.
Lemma 1
 (i)

\(X^{\sim }/Y=X\backslash Y^{}\) for all \(X,Y\subseteq M\),
 (ii)

\(X\backslash Y^{\sim }=(Y\cdot X)^{\sim }\) for all \(X,Y\subseteq M\),
 (iii)

\(X^{}/Y=(Y\cdot X)^{}\) for all \(X,Y\subseteq M\).
Proof
First, (Shift) is equivalent to (i) restricted to oneelement sets: for all \(a,b\in M\), \(\{a\}^{\sim }/\{b\}=\{a\}\backslash \{b\}^{}\). We have: \(x\in \{a\}^{\sim }/\{b\}\) iff \(x\cdot b\in \{a\}^{\sim }\) iff \(R(a,x\cdot b)\). Also: \(x\in \{a\}\backslash \{b\}^{}\) iff \(a\cdot x\in \{b\}^{}\) iff \(R(a\cdot x,b)\). So (Shift) is equivalent to: for all \(a,b,x\in M\), \(x\in \{a\}^{\sim }/\{b\}\) iff \(x\in \{a\}\backslash \{b\}^{}\).
Lemma 2
 (i)

\((\Diamond X)^{\sim }=\Box ^{\downarrow }(X^{\sim })\), for any \(X\subseteq M\),
 (ii)

\((\Diamond X)^{}=\Box ^{\downarrow }(X^{})\), for any \(X\subseteq M\).
Proof
We show that (mShift) entails (i) for oneelement sets X. We have: \(b\in (\Diamond \{a\})^{\sim }\) iff R(f(a), b) iff R(a, f(b)) iff \(f(b)\in \{a\}^{\sim }\) iff \(b\in \Box ^{\downarrow }(\{a\}^{\sim })\). Conversely, (mShift) follows from (i) for oneelement sets. Furthermore, (i) for all oneelement sets is equivalent to (i) for all sets. This can be shown as in the proof of Lemma 1, using the fact that \(\Diamond \) distributes over \(\bigcup \) and \(\Box ^{\downarrow }\) over \(\bigcap \). In a similar way, one shows the equivalence of (mShift) and (ii). \(\square \)
If \(\phi _{R}=\psi _{R}\), then \(M_{\phi _{R}}=M_{\psi _{R}}\); we denote this family by \(M_{R}\). Clearly \(M_{R}\) is closed under \(^{\sim },^{}\). We write \(\otimes _{R}, \Diamond _{R}\) for \(\otimes _{\phi _{R}},\Diamond _{\phi _{R}}\).
Theorem 1
Let \((M,\cdot ,f,R)\) be a phase space for InNLm. Then, \(\phi _{R}\) is a nucleus and \(M_{R}\) with operations \(\otimes _{R}\), \(\backslash \), / , \(\Diamond _{R}\), \(\Box ^{\downarrow }\), \(^{\sim }\), and \(^{}\), restricted to \(M_{R}\), is a modal involutive residuated groupoid.
Proof
We prove (C4’). Assume \(X\in M_{R}\), \(Y\subseteq M\). There exist \(Z,U\subseteq M\) such that \(X=Z^{\sim }=U^{}\). By Lemma 1, \(X/Y=U^{}/Y=(Y\cdot U)^{}\), hence \(X/Y\in M_{R}\). Similarly, \(Y\backslash X=Y\backslash Z^{\sim }=(Z\cdot Y)^{\sim }\), hence \(Y\backslash X\in M_{R}\). We prove (C5’). Assume \(X\in M_{R}\). Then, \(X=Z^{\sim }\), as above. So \(\Box ^{\downarrow }X=(\Diamond Z)^{\sim }\), by Lemma 2, hence \(\Box ^{\downarrow }X\in M_{R}\). Consequently, \(\phi _{R}\) is a nucleus. So the algebra is a modal residuated groupoid.
For \(X\in M_{R}\), we have: \(X^{\sim }=\phi _{R}(X)=X\) and \(X^{\sim }=\psi _{R}(X)=X\), which yields (DN). (CON) follows from Lemma 1, and (DMm) from Lemma 2. \(\square \)
We refer to the algebra \(M_{R}\), defined above, as the complex algebra of the phase space \((M,\cdot ,f,R)\). (In the literature on linear logics, the elements of this complex algebra are called facts.)
Lemma 3
Let \((M,\cdot ,f,R)\) be a phase space, satisfying (Shift) and (mShift). Let \(U\subseteq M\) be a set of generators of the free algebra \((M,\cdot ,f)\). Then, \(\phi _{R}=\psi _{R}\) if and only if for any \(a\in U\), \(\{a\}^{\sim }\) is \(\psi _{R}\)closed and \(\{a\}^{}\) is \(\phi _{R}\)closed.
Proof
We prove the ‘only if’ part. Assume \(\phi _{R}=\psi _{R}\). So the \(\phi _{R}\)closed sets coincide with the \(\psi _{R}\)closed sets. Since \(\{a\}^{\sim }\) is \(\phi _{R}\)closed, it is \(\psi _{R}\)closed. Since \(\{a\}^{}\) is \(\psi _{R}\)closed, it is \(\phi _{R}\)closed.
We prove the ‘if’ part. Assume the righthand side of the equivalence. We show that this condition holds for any \(a\in M\). Assume that \(a_{1},a_{2}\in M\) satisfy this condition. We show that \(a_{1}\cdot a_{2}\) satisfies this condition. We have \(\{a_{1}\cdot a_{2}\}^{\sim }=(\{a_{1}\}\cdot \{a_{2}\})^{\sim }\), and this set equals \(\{a_{2}\}\backslash \{a_{1}\}^{\sim }\), by Lemma 1(ii). Since \(\{a_{1}\}^{\sim }=\{a_{1}\}^{\sim \sim }\), by the second assumption, then this set equals \(\{a_{2}\}^{\sim }/\{a_{1}\}^{\sim \sim }\), by Lemma 1(i). Since \(\{a_{2}\}^{\sim }=\{a_{2}\}^{\sim \sim }\), by the assumption, this set equals \(\{a_{1}^{\sim \sim }\cdot a_{2}^{\sim \sim }\}^{}\), by Lemma 1(iii), hence it is \(\psi _{R}\)closed. In a similar way, one shows that \(\{a_{1}\cdot a_{2}\}^{}\) is \(\phi _{R}\)closed. Assume that a satisfies this condition. We show this condition for f(a). We have: \(\{f(a)\}^{\sim }=(\Diamond \{a\})^{\sim }=\Box ^{\downarrow }(\{a\}^{\sim })=\Box ^{\downarrow }(\{a\}^{\sim \sim })=(\Diamond (\{a\}^{\sim \sim }))^{}\). So this set is \(\psi _{R}\)closed. In a similar way, one shows that \(\{f(a)\}^{}\) is \(\phi _{R}\)closed.
Remark 1
If \((M,\cdot ,f,R)\) is a phase space for CNLm, then its complex algebra is a modal cyclic involutive residuated groupoid. This directly follows from Theorem 1 and the equality \(X^{\sim }=X^{}\), for \(X\subseteq M\).
Remark 2
Remark 3
Abrusci (1991) studied phase spaces for Noncommutative MALL. Like for other linear logics, his phase space is of the form \((M,\cdot ,O)\), where \(O\subseteq M\) (linear logicians write \(\bot ^{\bullet }\) for our O). One can define \(R_{O}=\{(a,b)\in M^{2}:\,a\cdot b\in O\}\). Then \(X^{\sim }=X\backslash O\), \(X^{}=O/X\). Our notion is more general and natural for logics without multiplicative constants; see Examples 1 and 2. However, if \((M,\cdot )\) is a free groupoid, then always \(R=R_{O}\) for \(O=\{a\cdot b:\,R(a,b)\}\).
 (ShiftO)

\((a\cdot b)\cdot c\in O\) iff \(a\cdot (b\cdot c)\in O\), for all \(a,b,c\in M\).
Remark 4
If \((M,\cdot ,1,f,R)\) is a unital phase space for InNLm (1 is the unit for \(\cdot \)), then \(\phi _R(\{1\})\) is the unit for \(\otimes _R\) in the complex algebra. This construction yields models for logics with multiplicative constants. Observe that (Shift) implies: R(a, b) iff \(R(a\cdot b,1)\), and consequently \(R=R_O\) for \(O=\{a\in M:R(a,1)\}\).
Example 1
Let \({{\mathbf {M}}}=(M,\cdot ,\backslash ,/,^{\sim },^{},\Diamond ,\Box ^{\downarrow },\le )\) be a modal involutive residuated groupoid. One defines the canonical phase space \((M,\cdot ,\Diamond ,R)\), by setting: R(a, b) iff \(a\le b^{}\) (equivalently: \(b\le a^{\sim }\)). One shows that this is a phase space for InNLm and the mapping \(h(a)=\{b\in M:b\le a\}\) is an embedding of \({\mathbf {M}}\) into the complex algebra of this canonical phase space. In general, the canonical relation R cannot be represented as \(R_{O}\) for \(O\subseteq M\).
Example 2
Let M be the set of all pairs of positive integers. We define the addition of pairs pointwise. So \((M,+)\) is a commutative semigroup. The relation \(R\subseteq M^{2}\) is defined as follows: R(x, y) iff neither x, nor y is a sum of two pairs. Clearly R is symmetric and satisfies (Shift). Consequently, \((M,+,R)\) is a phase space for CNL. We show that \(R\ne R_O\) for any \(O\subseteq M\). Suppose that \(R=R_O\). Since R((1, 2), (2, 1)), we get \((3,3)\in O\). Hence R((1, 1), (2, 2)). This contradicts the definition of R, since \((2,2)=(1,1)+(1,1)\).
3 Sequent Systems
We present our onesided sequent system for InNLm. Propositional variables are denoted by \(p, q, r,\ldots \). Atomic formulas (atoms) are of the form \(p^{(n)}\), where p is a variable and \(n\in {{\mathbb {Z}}}\). \(p^{(n)}\), for \(n\ge 0\), means \(p^{\sim \cdots \sim }\) with \(^{\sim }\) occurring n times, and for \(n<0\), it means \(p^{\cdots }\) with \(^{}\) occurring n times. So \(p^{(0)}=p\), \(p^{(2)}=p^{\sim \sim }\), \(p^{(2)}=p^{{}{}}\), and so on. The connectives are \(\otimes ,\oplus ,\Diamond ,\Box ^{\downarrow }\).
Bunches are defined as for NLm. Sequents are pairs of bunches. The metalogical notation is like for NLm. \(\Upsilon \) is reserved for sequents. \(\Gamma ;\Delta \) denotes the sequent being the pair of \(\Gamma \) and \(\Delta \).
Notice that the rules of the cutfree SInNLm do not manipulate negations. This system possesses the subformula property: the sequents appearing in a proof of \(\Upsilon \) consist of subformulas of the formulas occurring in \(\Upsilon \). We assume that the only subformula of \(p^{(n)}\) is \(p^{(n)}\). So e.g. p is not a subformula of \(p^{\sim }\).
We need two prooftheoretic lemmas. The complete proofs of these lemmas for InNL can be found in Buszkowski (2017a).
Lemma 4
The rules (rShift), (rmShift) are admissible in \(S_{0}\).
Proof
We prove: \(\vdash _{0}(\Gamma _{1},\Gamma _{2});\Gamma _{3}\) iff \(\vdash _{0}\Gamma _{1};(\Gamma _{2},\Gamma _{3})\). The onlyif part is proved by induction on the proof of \((\Gamma _{1},\Gamma _{2});\Gamma _{3}\) in \(S_{0}\), and the converse implication in a similar way. \((\Gamma _{1},\Gamma _{2});\Gamma _{3}\) is not an axiom. It can be the conclusion of \(\hbox {(r}\otimes \)), \(\hbox {(r}\oplus 1\)), \(\hbox {(r}\oplus 2\)), \(\hbox {(r}\oplus 4\)), \(\hbox {(r}\Diamond \)) and \(\hbox {(r}\Box ^{\downarrow }\)). The nonmodal rules are treated as in Buszkowski (2017a). For the modal rules, the active formula occurs in \(\Gamma _{i}\) for some i. We apply the induction hypothesis to the premise of this modal rule, then apply this rule.
We prove: \(\vdash _{0}\langle \Gamma _{1} \rangle ;\Gamma _{2}\) iff \(\vdash _{0}\Gamma _{1} ;\langle \Gamma _{2} \rangle \). The onlyif part is proved by induction on the proof of \(\langle \Gamma _{1} \rangle ;\Gamma _{2}\) in \(S_{0}\), and the converse implication in a similar way. \(\langle \Gamma _{1}\rangle ;\Gamma _{2}\) is not an axiom. It can be the conclusion of \(\hbox {(r}\otimes \)), \(\hbox {(r}\oplus \)1), \(\hbox {(r}\oplus \)2), \(\hbox {(r}\Diamond \)), \(\hbox {(r}\Box ^{\downarrow }\)) and \(\hbox {(r}\Box ^{\downarrow }2\)). The first four rules cause no problem: the active formula or the active bunch (for \(\oplus \)rules) must be contained in \(\Gamma _{1}\) or \(\Gamma _{2}\). One applies the induction hypothesis to a premise of this rule, then applies this rule. For \(\hbox {(r}\Box ^{\downarrow }\)), the interesting case is: \(\langle \Gamma _{1}\rangle ;\Gamma _{2}\) equals \(\langle \Box ^{\downarrow }A\rangle ;\Gamma _{2}\) with the premise \(A;\Gamma _{2}\). Then, \(\Box ^{\downarrow }A;\langle \Gamma _{2}\rangle \) arises by \(\hbox {(r}\Box ^{\downarrow }1\)). For \(\hbox {(r}\Box ^{\downarrow }2\)), \(\langle \Gamma _{1}\rangle ;\Gamma _{2}\) equals \(\langle \Gamma _{1}\rangle ;\Box ^{\downarrow }A\) with the premise \(\Gamma _{1};A\). Then, \(\Gamma _{1};\langle \Box ^{\downarrow }A\rangle \) arises by \(\hbox {(r}\Box ^{\downarrow }\)). \(\square \)
Lemma 5
The rules (\(\hbox {r}^{\sim \sim }\)), (\(\hbox {r}^{{}{}}\)) are admissible in the cutfree SInNLm.
Proof
It suffices to prove that these rules are admissible in \(S_{0}\). For (\(\hbox {r}^{\sim \sim }\)), we prove: if \(\vdash _{0}D;\Theta \) then \(\vdash _{0}\Theta ;D^{\sim \sim }\), by the outer induction on the number of connectives in D and the inner induction on the proof of \(D;\Theta \) in \(S_{0}\). For (\(\hbox {r}^{{}{}}\)) the argument is similar.
Assuming our claim for all \(D'\) having less connectives than D, we run the inner induction. If \(D;\Theta \) is an axiom (id), where \(D=p^{(n)}\), \(\Theta = p^{(n+1)}\), then \(\Theta ;D^{\sim \sim }\) equals \(p^{(n+1)};p^{(n+2)}\), which is an axiom, too.
Assume that \(D;\Theta \) is the conclusion of a rule. The nonmodal rules are treated as in Buszkowski (2017a).
\(\hbox {(r}\Diamond \)). The interesting case is: \(D;\Theta \) equals \(\Diamond A;\Theta \) with the premise \(\langle A\rangle ;\Theta \). Due to Lemma 4, we get \(A;\langle \Theta \rangle \), by (rmShift), hence \(\langle \Theta \rangle ;A^{\sim \sim }\), by the outer induction hypothesis. Then, \(\Theta ;\langle A^{\sim \sim }\rangle \), by (rmShift), and finally \(\Theta ;\Diamond (A^{\sim \sim })\), by \(\hbox {(r}\Diamond \)). Clearly \(\Diamond (A^{\sim \sim })\) equals \((\Diamond A)^{\sim \sim }\).
\(\hbox {(r}\Box ^{\downarrow }\)). The active bunch \(\langle \Box ^{\downarrow }A\rangle \) must occur in \(\Theta \). One applies the inner induction hypothesis to the premise, then applies \(\hbox {(r}\Box ^{\downarrow })\).
\(\hbox {(r}\Box ^{\downarrow }1\)). Then, \(D;\Theta \) equals \(\Box ^{\downarrow }A;\langle \Theta '\rangle \) with the premise \(A;\Theta '\). We get \(\Theta ';A^{\sim \sim }\), by the inner induction hypothesis, hence \(\Theta ;\Box ^{\downarrow }(A^{\sim \sim })\), by \(\hbox {(r}\Box ^{\downarrow }2\)).
\(D,\Theta \) cannot be the conclusion of \(\hbox {(r}\Box ^{\downarrow }2\)). \(\square \)
\(S_{0}\) is needed just for the proof of Lemma 5. With SInNLm, there would be problems for (rShift) and (rmShift). For instance, if \(D;(\Gamma ,\Delta )\) arises from \((D,\Gamma );\Delta \) by (rShift), one cannot apply the inner induction hypothesis to the premise.
Corollary 1
\(\vdash A^{};\Gamma \) if and only if \(\vdash \Gamma ; A^{\sim }\)
Theorem 2
For any sequent \(\Upsilon \), \(\vdash \Upsilon \) if and only if \(\Upsilon \) is valid in InNLm.
Proof
It is easy to verify that the axioms (id) are valid and all rules preserve validity (in fact, they preserve the truth for \(\mu \) in \({\mathbf {M}}\)). For \(\hbox {(r}\otimes \)) and \(\hbox {(r}\Diamond \)) this is obvious. For \(\hbox {(r}\oplus \)1), \(\hbox {(r}\oplus \)2) this follows from the laws \(a^{}\otimes (a\oplus b)\le b\), \((a\oplus b)\otimes b^{\sim }\le a\) and for \(\hbox {(r}\Box ^{\downarrow }\)) from (RGm). One uses (COMP) for (rShift) and (COMPm) for (rmShift).
For the ‘if’ part, we construct a countermodel for any unprovable sequent. We consider a phase space \((M,\cdot ,f,R)\) such that \((M,\cdot ,f)\) is the free algebra of bunches (i.e. \(\Gamma \cdot \Delta =(\Gamma ,\Delta )\) and \(f(\Gamma )=\langle \Gamma \rangle \)) and: \(R(\Gamma ,\Delta )\) iff \(\vdash \Gamma ;\Delta \). Clearly this phase space satisfies (Shift) and (mShift), due to (r–Shift) and (rmShift).
 (P1)

If \(X\in M_{R}\) and \((B,C)\in X\), then \(B\otimes C\in X\).
By the induction hypothesis, (3) holds for B and C. From \(B\in \mu (B)\) and \(C\in \mu (C)\) we obtain \((B,C)\in \mu (B)\cdot \mu (C)\subseteq \mu (B)\otimes _{R}\mu (C)=\mu (B\otimes C)\), hence \(B\otimes C\in \mu (B\otimes C)\), by (P1). Also \(\mu (B)\subseteq [B]=\{B^{}\}^{\sim }\) and \(\mu (C)\subseteq [C]=\{C^{}\}^{\sim }\). Hence, for all \(\Gamma \in \mu (B)\), \(\vdash B^{};\Gamma \), and for all \(\Delta \in \mu (C)\), \(\vdash C^{};\Delta \). By \(\hbox {(r}\oplus \)3), \(\vdash C^{}\oplus B^{};(\Gamma ,\Delta )\), for all \(\Gamma \in \mu (B)\), \(\Delta \in \mu (C)\). Consequently, \(\mu (B)\cdot \mu (C)\subseteq \{(B\otimes C)^{}\}^{\sim }=[B\otimes C]\), which yields \(\mu (B\otimes C)=\phi _{R}(\mu (B)\cdot \mu (C))\subseteq [B\otimes C]\), since \([B\otimes C]\) is \(\phi _{R}\)closed.
\(A=B\oplus C\). Since B and \(B^{}\) have the same number of connectives, and similarly for C and \(C^{}\), then (3) holds for \(B^{}\) and \(C^{}\) by the induction hypothesis. So \(C^{}\otimes B^{}\in \mu (C^{}\otimes B^{})\subseteq [C^{}\otimes B^{}]\), by the above. We obtain \([C^{}\otimes B^{}]^{\sim }\subseteq \mu (C^{}\otimes B^{})^{\sim }\subseteq \{C^{}\otimes B^{}\}^{\sim }\), which yields (3) for \(B\oplus C\), since \(B\oplus C\in \{B\oplus C\}^{\sim }=[C^{}\otimes B^{}]^{\sim }\), \(\mu (C^{}\otimes B^{})^{\sim }=\mu (B\oplus C)\) and \(\{C^{}\otimes B^{}\}^{\sim }=[B\oplus C]\).
 (P1m)

if \(X\in M_{R}\) and \(\langle B\rangle \in X\), then \(\Diamond B\in X\).
The case \(A=\Box ^{\downarrow }B\) is similar to \(A=B\oplus C\) and left to the reader.
Assume \(\not \vdash \Gamma ;\Delta \). From \(A\in \mu (A)\), for any formula A, one easily proves \(\Theta \in \mu (\Theta )\) for any bunch \(\Theta \), by induction on the number of commas and angle brackets in \(\Theta \). So \(\Gamma \in \mu (\Gamma )\) and \(\Delta \in \mu (\Delta )\). By the assumption, \(\Gamma \not \in \mu (\Delta )^{}\), hence \(\mu (\Gamma )\not \subseteq \mu (\Delta )^{}\). Consequently, \(\Gamma ;\Delta \) is not valid. \(\square \)
Corollary 2
(cut\(^{\sim }\)) and (cut\(^{}\)) are admissible in the cutfree SInNLm.
Proof
Both rules preserve the truth for \(\mu \) in \({\mathbf {M}}\), hence the validity. \(\square \)
This modeltheoretic proof of the cutelimination theorem is not constructive. A constructive, syntactic proof for SInNL is given in Buszkowski (2017a).
Theorem 3
SInNLm is strongly complete with respect to modal involutive residuated groupoids.
Proof
Let \(\Phi \) be a set of sequents. Every bunch \(\Gamma \) can be transformed in a formula \(F(\Gamma )\), according to the rules: \(F(A)=A\), \(F((\Gamma ,\Delta ))=F(\Gamma )\otimes F(\Delta )\), \(F(\langle \Gamma \rangle )=\Diamond F(\Gamma )\). In SInNLm every sequent \(\Gamma ;\Delta \) is deductively equivalent to \(F(\Gamma );F(\Delta )\). So we assume that all sequents in \(\Phi \) are of the latter form.
Now, \(\vdash \) denotes the provability in SInNLm. Notice that (\(\hbox {r}^{\sim \sim }\)), (\(\hbox {r}^{{}{}}\)) are derivable. For (\(\hbox {r}^{\sim \sim }\)), we derive \(\Gamma ;A^{\sim \sim }\) from \(A;\Gamma \), using \(A^{\sim };A^{\sim \sim }\) (valid, hence provable), by (cut\(^{}\)). For (\(\hbox {r}^{{}{}}\)), use \(A^{{}{}};A^{}\) and (cut\(^{\sim }\)).
 (P2)

If \(X\in M_{R}\) and \(A\in X\), then \([A]\subseteq X\).
Accordingly, \(A\in \mu (A)\) yields \([A]\subseteq \mu (A)\). Hence (3) entails (4).
If \((A;B)\in \Phi \), then \(A\in [B^{}]\) and \([A]\subseteq [B^{}]\), by (P2), hence \(\mu (A)\subseteq \mu (B)^{}\), by (4), (2). So all sequents from \(\Phi \) are true for \(\mu \). If \(\Phi \not \vdash \Gamma ;\Delta \), then \(\mu (\Gamma )\not \subseteq \mu (\Delta )^{}\), as in the proof of Theorem 2. \(\square \)
These logics can be augmented with additive connectives \(\wedge ,\vee \) and multiplicative constants 1, 0; see Buszkowski (2017a) for such systems without modalities. All results of Sects. 2 and 3 remain true for these extensions.
Although each sequent of SInNLm is divided in two parts by semicolon, this does not mean that the system is twosided. The sequent \(\Gamma ;\Delta \) can uniquely be represented as the bunch \((\Gamma ,\Delta )\). So semicolons can be replaced by commas and sequents defined as the bunches containing at least two formulas [like in Buszkowski (2016, 2017a)]. In this paper we write semicolon for the outermost comma in a sequent in order to emphasize its distinguished role: in opposition to other commas it is not interpreted as product (we follow de Groote and Lamarche 2002, where semicolons are used in a similar role). Nonetheless one cannot write \(\Gamma \Rightarrow \Delta \) for \(\Gamma ;\Delta \), since the sequent is not interpreted as \(\mu (\Gamma )\le \mu (\Delta )\). For the associative version of InNL (i.e. Involutive Lambek Calculus), an analogous sequent system operates with sequents in the form of finite sequences \(A_1,\ldots ,A_n\), where \(n\ge 2\) (no comma is distinguished). We have, for instance, \({{\mathbf {M}}},\mu \models A,B,C\) iff \(\mu (A\otimes B)\le \mu (C)^{}\) iff \(\mu (B\otimes C)\le \mu (A)^{\sim }\). Similarly, for SInNLm with 1, 0, sequents can be identified with bunches. One defines \({{\mathbf {M}}},\mu \models \Gamma \) iff \(\mu (\Gamma )\le 0\); see Buszkowski (2017a).
The truth condition \(\mu (\Gamma )\le 0\) is dual to \(1\le \mu (\Gamma )\), which is admitted for standard onesided systems for linear logics (in those systems, all commas in sequents are interpreted as \(\oplus \)). Our systems follow Lambek (1995) who studies an analogous system for Bilinear Logic. In relation to twosided systems with sequents \(\Gamma \Rightarrow \Delta \), the standard onesided systems employ sequents \(\Rightarrow \Delta \), whereas ours \(\Gamma \Rightarrow \) (precisely, this holds for our systems with 1, 0). Our systems are more compatible with the syntax of intuitionistic systems and more expedient for type grammars.^{2} Let us note that SInNLm can easily be transformed into a standard form. The axioms are (id) \(p^{(n+1)};p^{(n)}\). One interchanges \(\otimes \) and \(\oplus \) as well as \(\Diamond \) and \(\Box ^{\downarrow }\) in the rules for connectives and modifies the second premise in the cut rules to \(A^{\sim };\Delta \) in (cut\(^{\sim }\)) and \(\Delta ;A^{}\) in (cut\(^{}\)). All results of this paper can be proved for the standard SInNLm in essentially the same way or even inferred from our results, using natural symmetries, e.g. \(\Gamma ;\Delta \) is provable in SInNLm if and only if \(\Delta ^{\sim };\Gamma ^{\sim }\) is provable in its standard version. Here \(\Gamma ^{\sim }\) is recursively defined, using the last equation of the next paragraph.
At the end, we mention other systems, closely related to ours. Bastenhof (2013) studies different formal systems for InNL, called Nonassociative Bilinear Logic, among them a display system and two different, standard onesided sequent systems. In the latter systems negations are treated as connectives in the language of the system. \(A^{r}\) and \(A^{l}\) are written for our \(A^{\sim }\) and \(A^{}\), respectively, but these are not our metalanguage negations, e.g. \((p\otimes q)^{r}\) is a wellformed formula of these systems. In some rules the formula \(A^{rl}\) or \(A^{lr}\) in the premise is reduced to A in the conclusion; also \(A^{rr}\) and \(A^{ll}\) can be reduced to A, while moving to the other side of the sequent. Therefore, the cutfree systems do not possess the subformula property.^{3} Galatos and Jipsen (2013) introduce a twosided sequent system for InNL with 1, 0 and \(\wedge ,\vee \) (denoted by InGL), whose multiplicative connectives are \(\otimes ,\sim ,\) (product and two negations, written before formulas, e.g. \(A\)). Sequents are of the form \(\Gamma \Rightarrow \Delta \). (Since \(\oplus \) is not used, the commas in \(\Delta \) are never replaced by \(\oplus \); they are only used to manipulate negations.) The negations of bunches \(\Gamma ^{\sim }\), \(\Gamma ^{}\) are treated as structural operators (like our angle brackets). One assumes that these structural operators satisfy the laws of free involutive groupoids e.g. \(\Gamma ^{\sim }=\Gamma \), \((\Gamma ,\Delta )^{\sim }=(\Delta ^{\sim },\Gamma ^{\sim })\). Although this system possesses the subformula property, it is not easy to control the number of structural negations, applied in a proof. Our systems avoid this problem. Galatos and Jipsen (2013) does not consider phase spaces in our sense.
4 Studying InNLm with the Aid of InNLm(k)
Let a be an element of an involutive residuated groupoid. We use the notation \(a^{(n)}\) in the same meaning as in Sect. 3, e.g. \(a^{(2)}=a^{\sim \sim }\), \(a^{(2)}=a^{{}{}}\). Let k be an even positive integer. An involutive residuated groupoid is said to be kcyclic, if \(a^{(k)}=a\) for any \(a\in M\) (Galatos and Jipsen 2013).^{4} Notice that \(a^{}=a^{(k1)}\) in kcyclic algebras of this kind, since \(a^{\sim }=a=a^{(k)}=(a^{(k1)})^{\sim }\) and \(^{\sim }\) is a bijection, by (DN). In particular, ‘2cyclic’ means ‘cyclic’.
InNLm(k) is InNLm from Sect. 1 with the new axiom \(A^{(k)}\Leftrightarrow A\). This logic is strongly complete with respect to kcyclic modal involutive residuated groupoids. InNLm(2) amounts to CNLm.
We introduce a sequent system SInNLm(k). The atoms are of the form \(p^{(n)}\) for \(0\le n< k\). All axioms and rules are as for SInNLm, but n, \(n+1\) are computed modulo k. So the axioms are: \(p^{(n)};p^{(n+1)}\), for \(0\le n<k1\) and \(p^{(k1)};p\).
The metalanguage negations \(^{\sim },^{}\) are defined as in Sect. 3 (we compute \(n+1\) and \(n1\) modulo k). All syntactic equations from Sect. 3 remain true. We use the notation \(A^{(n)}\) for arbitrary formulas A in an obvious sense. We have \(A^{(k)}=A\), since k is even. We also obtain (1) for any valuation \(\mu \) in a kcyclic modal involutive residuated groupoid. Lemmas 4 and 5 remain true; now \(S_{0}\) arises from SInNLm(k) like the former \(S_{0}\) from SInNLm.
Theorem 4
The cutfree SInNLm(k) is weakly complete.
Proof
The whole proof of Theorem 2 can be repeated except that we cannot prove (at this moment) that the algebra \((M_{R},\otimes _{R},\backslash ,/,\Diamond _{R},\Box ^{\downarrow },^{\sim },^{},\subseteq )\) is kcyclic. We consider the subalgebra \(M^{\mu }_{R}\), consisting of \(\mu (A)\), for all formulas A. By (1), \(\mu (A)^{(k)}=\mu (A^{(k)})=\mu (A)\), hence \({{\mathbf {M}}}^{\mu }_{R}\) is kcyclic. If \(\not \vdash \Gamma ;\Delta \), then \({{\mathbf {M}}}^{\mu }_{R},\mu \not \models \Gamma ;\Delta \), and consequently, \(\Gamma ;\Delta \) is not valid. \(\square \)
Accordingly, (cut\(^{\sim }\)), (cut\(^{}\)) are admissible in the cutfree SInNLm(k). With these rules SInNLm(k) is strongly complete with respect to kcyclic modal involutive residuated groupoids. Again the proof of Theorem 3 can be repeated, and we consider \({{\mathbf {M}}}^{\mu }_{R}\) as above.
Lemma 6
For any sequent \(\Upsilon \) and \(m\in {{\mathbb {Z}}}\), \(\Upsilon \) is provable in SInNLm if and only if \(\tau (\Upsilon ,m)\) is provable in SInNLm.
Proof
Assume that \(\Upsilon \) is provable in SInNLm. In a proof of \(\Upsilon \) we substitute \(p^{(n+m)}\) for \(p^{(n)}\), for any atom \(p^{(n)}\). We obtain a proof of \(\tau (\Upsilon ,m)\). This yields the onlyif part, which entails the ‘if’ part, since \(\Upsilon =\tau (\tau (\Upsilon ,m),m)\). \(\square \)
Let \(\Upsilon \) be a sequent, and let m be the greatest positive integer n such that some atom \(p^{(n)}\) occurs in \(\Upsilon \); if there is none, we set \(m=0\). The provability of \(\Upsilon \) is equivalent to the provability of \(\tau (\Upsilon ,m)\), which contains no \(p^{(n)}\) with \(n<0\); such a sequent is said to be \(^{}\)free.
Lemma 7
Let \(\Upsilon \) be a \(^{}\)free sequent. Let m be the greatest integer n such that some atom \(p^{(n)}\) occurs in \(\Upsilon \). Let \(k>m+1\). Then, \(\Upsilon \) is provable in SInNLm if and only if \(\Upsilon \) is provable in SInNLm(k).
Proof
Assume that \(\Upsilon \) is provable in SInNLm. Then \(\Upsilon \) is valid in InNLm, and consequently, in kcyclic modal involutive residuated groupoids. By Theorem 4, \(\Upsilon \) is provable in SInNLm(k).
Assume that \(\Upsilon \) is provable in SInNLm(k). There exists a (cutfree) proof of \(\Upsilon \) in this system. Every formula in this proof is a subformula of a formula in \(\Upsilon \). Consequently, no atom \(p^{(k1)}\) appears in this proof, hence no axiom \(p^{(k1)};p\) is used. This proof is a proof in SInNLm. \(\square \)
Therefore, if a sequent \(\Upsilon \) is not provable in InNLm, then it is not valid in some kcyclic modal involutive residuated groupoid. An analogous result for InGL was obtained in Galatos and Jipsen (2013) with the aid of a twosided sequent system.
InNL(k) has similar properties as CNL, which is the same logic as InNL(2), although the sequent system for InNL(2), presented here, differs from those in de Groote and Lamarche (2002) and Buszkowski (2016). We prove four theorems on InNLm(k), analogous to some results for CNL in Buszkowski (2016).
Let T be a set of formulas. By a Tsequent we mean a sequent consisting of formulas from T. A proof consisting of Tsequents is called a Tproof. Now, \(\vdash \) stands for the provability in InNLm(k) and \(\vdash _{T}\) for the provability in InNLm(k), restricted to Tproofs. Again we assume that all sequents in \(\Phi \) are of the form A; B. We show an interpolation property for InNLm(k).
Theorem 5
Let T be closed under subformulas and \(^{\sim }\). If \(\Phi \vdash _{T} \Upsilon [\Delta _{0}]\), then there exists \(D\in T\) (an interpolant of \(\Delta _{0}\) in \(\Upsilon [\Delta _{0}]\)) such that \(\Phi \vdash _{T} \Upsilon [D]\) and \(\Phi \vdash _{T} \Delta _{0} \Rightarrow D\).
Proof
We proceed by induction on proofs in SInNLm(k) with \(\Phi \) (the assumptions). If \(\Delta _{0}\) is a formula, then \(D=\Delta _{0}\). Assume that \(\Delta _{0}\) is not a formula. Then, \(\Upsilon [\Delta _{0}]\) cannot be an axiom (Id), nor a sequent from \(\Phi \). For rules, we only discuss some cases. We consider \(\hbox {(r}\oplus \)2). If the active bunch \((A\oplus B,\Delta )\) is contained in \(\Delta _{0}\), then D is an interpolant of the trace of \(\Delta _{0}\) in the left premise; in particular, A is an interpolant of \((A\oplus B,\Delta )\). If \(\Delta _{0}\) is contained in \(\Delta \), then D is an interpolant of \(\Delta _{0}\) in the right premise. If \(\Delta _{0}\) is disjoint from the active bunch, then D is an interpolant of \(\Delta _{0}\) in the left premise. For \(\hbox {(r}\Box ^{\downarrow }\)), if \(\Delta _{0}=\langle \Box ^{\downarrow }A\rangle \), then \(D=A\). We consider (rShift), topdown, with premise \((\Gamma ,\Delta );\Theta \) and conclusion \(\Gamma ;(\Delta ,\Theta )\), where \(\Delta _{0} =(\Delta , \Theta )\). Then \(D=E^{\sim }\), where E is an interpolant of \(\Gamma \) in the premise; similarly, for (rmShift), topdown, if \(\Delta _{0}=\langle \Delta \rangle \). \(\square \)
Every finite set T is contained in a finite set \(T'\), closed under subformulas and \(^{\sim }\) (the metalanguage negation), hence also under \(^{}\), since \(A^{}=A^{(k1)}\). The smallest set c(T), containing T and being closed under subformulas and \(^{\sim }\), can be constructed in polynomial time in the size of T and k. We prove a version of the subformula property for InNLm(k) with assumptions.
Theorem 6
Let T be the set of all formulas which occur in \(\Upsilon \) or \(\Phi \). If \(\Phi \vdash \Upsilon \), then \(\Phi \vdash _{c(T)}\Upsilon \).
Proof
We outline the proof. One defines a phase space \((M,\cdot , f,R)\) like in the proof of Theorem 3 except that M is the free algebra generated by c(T) and \(\vdash \) is replaced with \(\vdash _{c(T)}\). We also define \([A]=\{\Gamma \in M:\Phi \vdash _{c(T)}\Gamma \Rightarrow A\}\) for any formula A (so \([A]=\emptyset \) for \(A\not \in c(T)\)). (1) holds for all formulas A and (2) for \(A\in c(T)\). In (P1) one assumes \(B\otimes C\in c(T)\) and in (P1m) \(\Diamond B\in c(T)\). (P2) holds for any A. \(\mu \) is defined in the same way. (4) holds for any \(A\in c(T)\). Assume that \(\Phi \vdash _{c(T)}\Upsilon \) does not hold. Then \(\Upsilon \) is not true for \(\mu \) in the subalgebra (defined as in the proof of Theorem 4) of the complex algebra of this phase space, but all sequents from \(\Phi \) are true for \(\mu \). This subalgebra is a kcyclic modal involutive residuated groupoid. Therefore \(\Phi \vdash \Upsilon \) does not hold. \(\square \)
For readers interested in models we note that this proof yields the strong finite model property^{5} for InNLm(k). We assume that \(\Phi \) is finite, hence T and c(T) are finite. We show that the complex algebra of this (infinite) phase space is finite. Every \(\phi _{R}\)closed set is an intersection of sets of the form \(\{\Gamma \}^{\sim }\). By Theorem 5, \(\{\Gamma \}^{\sim }\) is the union of some sets [D] for \(D\in c(T)\). We show it. Let \(\Delta \in \{\Gamma \}^{\sim }\). Then \(\Phi \vdash _{c(T)}\Gamma ;\Delta \), hence there is \(D\in c(T)\) such that \(\Phi \vdash _{c(T)}\Gamma ;D\) and \(\Phi \vdash _{c(T)}\Delta \Rightarrow D\). So \(\Delta \in [D]\) and \([D]\subseteq \{\Gamma \}^{\sim }\), by (P2). Consequently, \(M_{R}\) is finite.
Theorem 7
The languages generated by the type grammars based on InNLm(k) are precisely the (\(\epsilon \)free) contextfree languages.
Proof
This follows from Theorems 5 and 6. Let \(G=(\Sigma ,I,A_{0})\) be a type grammar based on InNLm(k). Let T denote the set of all formulas involved in I plus \(A_{0}\). By Theorem 5, every c(T)sequent \(\Gamma \Rightarrow A_{0}\) (i.e. \(A_{0}^{};\Gamma \)), provable in InNLm(k) and containing no angle brackets, can be proved on the basis of provable c(T)sequents of the form \((A_{1},A_{2})\Rightarrow B\) and \(A\Rightarrow B\) (special sequents) with the aid of (NLcut). This can be shown by induction on the number of commas in \(\Gamma \). If \(\Gamma \) contains at most two commas, the sequent is special. If \(\Gamma \) contains more commas, then \(\Gamma =\Theta [(A_1,A_2)]\). Let D be an interpolant of \((A_1,A_2)\). Then, \(\Gamma \Rightarrow A_0\) can be derived from \(\Theta [D]\Rightarrow A_0\) and \(A_1,A_2\Rightarrow D\) by (NLcut). Clearly \(\Theta [D]\) has less commas than \(\Gamma \). This yields a contextfree grammar equivalent to G. Its terminal alphabet is \(\Sigma \), the nonterminal symbols are the formulas from c(T), the production rules are the reversed, special c(T)sequents provable in InNLm(k) (i.e. \(B\rightarrow A_{1},A_{2}\) and \(B\rightarrow A\)), and \(A_{0}\) is the start symbol. So L(G) is contextfree. It is known that every \(\epsilon \)free contextfree language is generated by a type grammar based on NL (Buszkowski 2005), and NL can be replaced by InNLm(k), since InNLm(k) is a conservative extension of NL (see below). \(\square \)
Theorem 8
The finitary consequence relation for InNLm(k) is PTIME.
Proof
By a restricted sequent we mean a sequent of the form A; B, or (A, B); C, or A; (B, C), or \(\langle A\rangle ;B\), or \(A;\langle B\rangle \). Let T be a finite set of formulas. Let \(S^{T}\) denote SInNLm(k) (with the cut rules), augmented with a finite \(\Phi \) (consisting of Tsequents of the form A; B), whose all axioms and rules are limited to restricted c(T)sequents. One easily shows by induction on A that \(A;A^{\sim }\) and \(A^{};A\) are provable in \(S^{T}\) for any \(A\in c(T)\). We will show that all restricted c(T)sequents, provable in SInNLm(k) from \(\Phi \), are provable in \(S^{T}\).
 (I)

A restricted c(T)sequent is provable in S(T) iff it is provable in \(S^{T}\).
 (II)

S(T) possesses the interpolation property: if \(\Upsilon [\Delta _{0}]\) is provable, then there exists \(D\in c(T)\) such that \(\Upsilon [D]\) and \(\Delta _{0}\Rightarrow D\) (i.e. \(D^{},\Delta _{0}\)) are provable.
The ‘if’ part of (I) is obvious. The onlyif part of (I) is proved by induction on proofs in S(T), using the fact: if the conclusion of a cut rule is restricted, then both premises are restricted. (II) can also be proved by induction on proofs in S(T). (II) holds for axioms, e.g. if \(\Upsilon [\Delta _0]\) is (A, B); C with \(\Delta _0=(A,B)\), then \(D=C^{}\). Assume that \(\Upsilon [\Delta _0]\) is the conclusion of (cut\(^{\sim }\)). If \(\Delta _0\) occurs in a premise, we apply the induction hypothesis to this premise and apply (cut\(^{\sim }\)). If not, then the premises of (cut\(^{\sim }\)) are \(\Upsilon [\Theta [A]]\) and \(\Delta ;A^{\sim }\) with \(\Delta _0=\Theta [\Delta ]\). Then, D is an interpolant of \(\Theta [A]\) in the first premise. For (cut\(^{}\)), the reasoning is similar.
One proves: for any c(T)sequent \(\Upsilon \), \(\Upsilon \) is provable in S(T) iff \(\Phi \vdash _{c(T)}\Upsilon \). The onlyif part is obvious. For the ‘if’ part, one shows that all rules of InNLm(k) are admissible in S(T). We consider \(\hbox {(r}\Box ^{\downarrow }\)). Assume that \(\Upsilon [A]\) is provable in S(T) and \(\Box ^{\downarrow }A\in c(T)\). Since \(\langle \Box ^{\downarrow }A\rangle ;A^{\sim }\) is provable in \(S^{T}\), by \(A;A^{\sim }\) and \(\hbox {(r}\Box ^{\downarrow }\)), then from \(\Upsilon [A]\) one obtains \(\Upsilon [\langle \Box ^{\downarrow }A\rangle ]\), by (cut\(^{\sim }\)). We consider (rmShift), topdown. Assume that \(\langle \Gamma \rangle ;\Delta \) is provable in S(T). By (II), there exist \(D\in c(T)\) and \(E\in c(T)\) such that \(\langle D\rangle ;E\), \(D^{};\Gamma \) and \(E^{};\Delta \) are provable in S(T). By (I), \(\langle D\rangle ;E\) is provable in \(S^{T}\), hence \(D;\langle E\rangle \) is provable in \(S^{T}\), by (rmShift). Therefore \(\Gamma ;\langle \Delta \rangle \) is provable in S(T), by (cut\(^{}\)).
In order to verify whether \(\Phi \vdash \Gamma ;\Delta \) one replaces the sequent by \(F(\Gamma );F(\Delta )\) and defines T as the set of formulas occurring in the latter sequent or \(\Phi \). By Theorem 6, \(\Phi \vdash F(\Gamma );F(\Delta )\) iff \(\Phi \vdash _{c(T)}F(\Gamma );F(\Delta )\). The latter holds if and only if \(F(\Gamma );F(\Delta )\) is provable \(S^{T}\), by the preceding paragraph and (I). All sequents provable in \(S^{T}\) can be generated in polynomial time in the size of c(T), hence in k plus the size of \(\{\Gamma ;\Delta \}\cup \Phi \). \(\square \)
In particular, Theorems 5–8 hold for CNLm. Using Lemmas 6 and 7, we obtain the following results for InNLm.
Theorem 9
The type grammars based on InNLm generate the \(\epsilon \)free contextfree languages.
Proof
Let \(G=(\Sigma ,I, A_{0})\) be a type grammar based on InNLm. Let T be the set of types involved in I plus \(A_{0}^{}\). Let l be the greatest \(n\ge 0\) such that some atom \(p^{(n)}\) occurs in T (as a subtype). In G we replace each type A by \(\tau (A,l)\). This yields a grammar \(G'\) such that \(L(G)=L(G')\), by Lemma 6. \(T'\) denotes the set of types involved in \(G'\). Let m be the greatest \(n\ge 0\) such that some atom \(p^{(m)}\) occurs in \(T'\) (as a subtype). \(G_{1}\) is defined like \(G'\) except that InNLm is replaced with InNLm(k), where \(k=m+2\). By Lemma 7, \(L(G_{1})=L(G')\). So L(G) is contextfree, by Theorem 7. Like in the proof of Theorem 7, one shows that every \(\epsilon \)free contextfree language is generated by a type grammar based on InNLm. \(\square \)
The next result easily follows from Lemmas 6, 7 and Theorem 8. Notice that m, defined under the proof of Lemma 6, can be computed in polynomial time in the size of \(\Upsilon \).
Theorem 10
InNLm is PTIME.
Accordingly, a contextfree grammar equivalent to the given type grammar G based on InNLm can be constructed in polynomial time in the size of G. On the contrary, an analogous construction for the type grammars based on L (due to Pentus 1993) is exponential. Since L is NPcomplete (Pentus 2006), no polynomial construction exists, if \(\hbox {P}\,\ne \,\hbox {NP}\).
Let us note that the proofs of Theorems 7 and 8 cannot be adapted for InNLm, since the closure of a nonempty, finite T under negations and subformulas is infinite. Lemma 7 reduces the provability in the pure InNLm to that in InNLm(k). Therefore we could prove Theorems 9 and 10 for the pure InNLm only (without assumptions), whereas Theorem 7 could be proved for InNLm(k) with any finite \(\Phi \). InNLm and InNL do not possess the strong finite model property (Buszkowski 2017a). The complexity of the finitary consequence relations for InNLm and InNL remains an open problem.
Besides their significance in logic, consequence relations may also be useful in type grammars. A stronger logic (less efficient) can be approximated by a weaker logic (more efficient) by adding to the latter some particular instances of the laws provable in the former. For instance, Moortgat (1997) adds \((A\otimes B)\otimes \Diamond C\Rightarrow A\otimes (B\otimes \Diamond C)\) to NLm in order to parse a relative clause, but for this goal only an instance of this law is needed (for some fixed types A, B, C). If one adds new axioms to NLm, then the resulting logic may lack the efficiency of NLm, but a finite set of new assumptions (i.e. particular instances of these axioms) do not affect the efficiency. This remains true for CNLm, but the problem for InNLm is open.
NLm (resp. InNLm) is a strongly conservative extension of NL (resp. InNL). The consequence relation for the richer logic contains that for the poorer logic. Conversely, if \(\Phi \vdash \Upsilon \) does not hold in the latter, then it does not hold in the former, since every (resp. involutive) residuated groupoid can be augmented with \(\Diamond ,\Box ^{\downarrow }\), satisfying (URES), (DM), by setting \(\Diamond a=\Box ^{\downarrow }a=a\).
Footnotes
 1.
Product distributes over joins in both arguments and \(\backslash ,/\) distribute over meets in the upper argument and convert joins into meets in the lower argument (Galatos et al. 2007).
 2.
The rules for connectives in SInNLm correspond to the left introduction rules in NLm [for \(\oplus \), see (IRG3)].
 3.
 4.
If k is odd, this condition entails \(a\otimes b=b\oplus a\) and: \(a\le b\) iff \(a=b\).
 5.
This means: Every unprovable pattern \(\Phi \vdash \Upsilon \), where \(\Phi \) is finite, can be falsified in a finite model.
References
 Abrusci, V. M. (1991). Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic. Journal of Symbolic Logic, 56, 1403–1451.CrossRefGoogle Scholar
 Ajdukiewicz, K. (1935). Die syntaktische Konnexität. Studia Philosophica, 1, 1–27.Google Scholar
 BarHillel, Y., Gaifman, C., & Shamir, E. (1960). On categorial and phrase structure grammars. The Bulletin of the Research Council of Israel F, 9, 155–166.Google Scholar
 Bastenhof, A. (2013). Categorial symmetry. Ph.D. thesis, University of Utrecht.Google Scholar
 Buszkowski, W. (2005). Lambek calculus with nonlogical axioms. In C. Casadio, P. J. Scott, & R. A. G. Seely (Eds.), Language and grammar. CSLI Lecture Notes (Vol. 168, pp. 77–93). Stanford: CSLI Publications.Google Scholar
 Buszkowski, W. (2011). Interpolation and FEP for logics of residuated algebras. Logic Journal of IGPL, 19, 437–454.CrossRefGoogle Scholar
 Buszkowski, W. (2016). On classical nonassociative Lambek calculus. In M. Amblard, P. de Groote, S. Pogodalla, & C. Retoré (Eds.), Logical aspects of computational linguistics. LNCS (Vol. 10054, pp. 68–84). Berlin: Springer.Google Scholar
 Buszkowski, W. (2017a). Involutive nonassociative Lambek calculus: Sequent systems and complexity. Bulletin of the Section of Logic, 46(1–2), 75–91.Google Scholar
 Buszkowski, W. (2017b). Phase spaces for involutive nonassociative Lambek calculus. In R. Loukanova & K. Liefke (Eds.), Electronic proceedings of the workshop on logic and algorithms in computational linguistics (pp. 21–45). Stockholm: Stockholm University.Google Scholar
 Casadio, C. (2001). Noncommutative linear logic in linguistics. Grammars, 4(3), 167–185.CrossRefGoogle Scholar
 Casadio, C., & Lambek, J. (2002). A tale of four grammars. Studia Logica, 71(3), 315–329.CrossRefGoogle Scholar
 de Groote, Ph, & Lamarche, F. (2002). Classical nonassociative Lambek calculus. Studia Logica, 71(3), 355–388.CrossRefGoogle Scholar
 Galatos, N., & Jipsen, P. (2013). Residuated frames with applications to decidability. Transactions of American Mathematical Society, 365, 1219–1249.CrossRefGoogle Scholar
 Galatos, N., Jipsen, P., Kowalski, T., & Ono, H. (2007). Residuated lattices. An algebraic glimpse at substructural logics. Amsterdam: Elsevier.Google Scholar
 Girard, J.Y. (1987). Linear logic. Theoretical Computer Science, 50, 1–102.CrossRefGoogle Scholar
 Grishin, V. N. (1983). On a generalization of the Ajdukiewicz–Lambek system. In A. I. Mikhailov (Ed.), Studies in nonclassical logics and formal systems (pp. 315–343). Moscow: Nauka.Google Scholar
 Lafont, Y. (1997). The finite model property of various fragments of linear logic. Journal of Symbolic Logic, 62, 1202–1208.CrossRefGoogle Scholar
 Lambek, J. (1958). The mathematics of sentence structure. The American Mathematical Monthly, 65, 154–170.CrossRefGoogle Scholar
 Lambek, J. (1961). On the calculus of syntactic types. In R. Jakobson (Ed.), Structure of language and its mathematical aspects (pp. 166–178). Providence: AMS.CrossRefGoogle Scholar
 Lambek, J. (1995). Cut elimination for classical bilinear logic. Fundamenta Informaticae, 22, 53–67.Google Scholar
 Lambek, J. (1999). Type grammars revisited. In A. Lecomte, F. Lamarche, & G. Perrier (Eds.), Logical aspects of computational linguistics, LNAI 1582 (pp. 1–27). Berlin: Springer.Google Scholar
 Lin, Z. (2014). Nonassociative Lambek calculus with modalities: Interpolation, complexity and FEP. Logic Journal of The IGPL, 22, 494–512.CrossRefGoogle Scholar
 Moortgat, M. (1996). Multimodal linguistic inference. Journal of Logic, Language, and Information, 5, 349–385.CrossRefGoogle Scholar
 Moortgat, M. (1997). Categorial type logic. In J. van Benthem & A. ter Meulen (Eds.), Handbook of logic and language (pp. 93–177). Amsterdam: Elsevier, MIT Press.CrossRefGoogle Scholar
 Moortgat, M. (2009). Symmetric categorial grammar. Journal of Philosophical Logic, 38(6), 681–710.CrossRefGoogle Scholar
 Moot, R., & Retoré, C. (2012). The logic of categorial grammars. LNCS (Vol. 6850). Berlin: Springer.CrossRefGoogle Scholar
 Morrill, G. (1994). Type logical grammar. Categorial logic of signs. Dordrecht: Kluwer.CrossRefGoogle Scholar
 Pentus, M. (1993). Lambek grammars are contextfree. In Proceedings of the 8 IEEE symposium on logic in computer science (pp. 429–433).Google Scholar
 Pentus, M. (2006). Lambek calculus is NPcomplete. Theoretical Computer Science, 357, 186–201.CrossRefGoogle Scholar
 Restall, G. (2000). An introduction to substructural logics. New York: Routledge.CrossRefGoogle Scholar
 van Benthem, J. (1991). Language in action. Categories, lambdas and dynamic logic. Amsterdam: NorthHolland.Google Scholar
 Yetter, D. N. (1990). Quantales and (noncommutative) linear logic. Journal of Symbolic Logic, 55, 41–64.CrossRefGoogle Scholar
Copyright information
OpenAccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.