Advertisement

On Involutive Nonassociative Lambek Calculus

  • Wojciech BuszkowskiEmail author
Open Access
Article
  • 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 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.

Keywords

Lambek calculus Linear logic Phase space Sequent system Type grammar Context-free grammar 

1 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 proof-theoretic 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 context-free 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 one-sided sequent system for InNL and proves the cut-elimination 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 model-theoretic proofs of the completeness and the cut-elimination 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 k-cyclic 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.

The unary modalities \(\Diamond ,\Box ^{\downarrow }\) satisfy (in algebras) the unary residuation law:
$$\begin{aligned} \text{(URES) } \Diamond a\le b\quad \text{ iff } a\le \Box ^{\downarrow }b\,, \end{aligned}$$
for all elements ab. NL with such modalities (NLm) was studied by Moortgat (1996, 1997) and its versions with special modal axioms and additive connectives by Lin (2014). These modalities were also considered by other authors; see Restall (2000). \(\Diamond ,\Box ^{\downarrow }\) are unary counterparts of Lambek connectives \(\otimes ,\backslash ,/\). In InNLm we also assume De Morgan laws for these modalities. Thus, the pair \(\Diamond ,\Box ^{\downarrow }\) behaves similarly as \(\otimes ,\oplus \), i.e. product and dual product (par).

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 multi-modal 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

We define the algebras corresponding to our logics. An algebra for NL is a residuated groupoid, i.e. an (ordered) algebra \((M,\otimes ,\backslash ,/,\le )\) such that \((M,\le )\) is a poset and \(\otimes ,\backslash ,/\) are binary operations on M, satisfying the residuation laws:
$$\begin{aligned} \text{(RES) } a\otimes b\le c\quad \text{ iff } b\le a\backslash c\quad \text{ iff } a\le c/b\,, \end{aligned}$$
for all \(a,b,c\in M\). The operation \(\otimes \) is called product, and \(\backslash ,/\) are its residuals.

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).

The following laws are valid in residuated groupoids:
(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\,\) (co-application 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).

A modal residuated groupoid is an algebra \((M,\otimes ,\backslash ,/,\Diamond ,\Box ^{\downarrow },\le )\) such that \((M,\otimes ,\backslash ,/,\le )\) is a residuated groupoid and \(\Diamond ,\Box ^{\downarrow }\) are unary operations on M, satisfying (URES). The following laws are valid in these algebras:
(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\).

The algebraic models for InNL are involutive residuated groupoids, i.e. algebras \((M,\otimes ,\backslash ,/,^{\sim },^{-},\le )\) such that \((M,\otimes ,\backslash ,/,\le )\) is a residuated groupoid and \(^{\sim }\), \(^{-}\) are unary, order reversing operations on M (this means: \(a\le b\) entails \(b^{\sim }\le a^{\sim }\) and \(b^{-}\le a^{-}\)), satisfying the double negation laws and the contraposition laws:
(DN)

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

(CON)

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

for all \(a,b\in M\). Notice that (CON) is equivalent to the following compatibility condition:
(COMP)

\(a\otimes b\le c^{-}\) iff \(b\otimes c\le a^{\sim }\), for all \(a,b,c\in M\).

An involutive residuated groupoid is said to be cyclic, if \(a^{\sim }=a^{-}\), for any element a. These algebras correspond to CNL.

(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^{-}\).

In any involutive residuated groupoid, \((a^{\sim }\otimes b^{\sim })^{-}=(a^{-}\otimes b^{-})^{\sim }\). For \(c\le (a^{\sim }\otimes b^{\sim })^{-}\) iff \(a^{\sim }\otimes b^{\sim }\le c^{\sim }\) iff \(c\otimes a^{\sim }\le b=b^{-\sim }\) iff \(b^{-}\otimes c\le a^{\sim -}=a^{-\sim }\) iff \(a^{-}\otimes b^{-}\le c^{-}\) iff \(c\le (a^{-}\otimes b^{-})^{\sim }\). One defines the dual product (par):
$$\begin{aligned} a\oplus b=(b^{\sim }\otimes a^{\sim })^{-}\,(=(b^{-}\otimes a^{-})^{\sim }) \end{aligned}$$
and obtains the following laws:
(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 }\).

We prove the first law (IRG2): \(c\le (b^{-}\otimes a)^{\sim }\) iff \(b^{-}\otimes a\le c^{-}\) iff \(a\le b^{-}\backslash c^{-}\) iff \(a\le b/c\) iff \(a\otimes c\le b\) iff \(c\le a\backslash b\).

Therefore, in involutive residuated groupoids, all operations can be expressed in terms of \(\otimes \) and negations. The one-sided sequent systems, considered later on, admit the language \(\otimes ,\oplus ,^{\sim },^{-}\) (negations at variables only).

The algebraic models for InNLm are modal involutive residuated groupoids, i.e. involutive residuated groupoids with \(\Diamond ,\Box ^{\downarrow }\), satisfying (URES) and the De Morgan laws for modalities:
(DMm)

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

We show that the first equation (DMm) is equivalent (on the basis of (URES) and laws for negations) to the following compatibility condition:
(COMPm)

\(\Diamond a\le b^{-}\) iff \(\Diamond b\le a^{\sim }\), for any elements ab,

which is an analogue of (COMP), if one thinks of \(\Diamond \) as a unary product. Assume the first equation (DMm). We have: \(\Diamond a\le b^{-}\) iff \(b\le (\Diamond a)^{\sim }=\Box ^{\downarrow }(a^{\sim })\) iff \(\Diamond b\le a^{\sim }\). Assume (COMPm). We have: \(b\le (\Diamond a)^{\sim }\) iff \(\Diamond a\le b^{-}\) iff \(\Diamond b\le a^{\sim }\) iff \(b\le \Box ^{\downarrow }(a^{\sim })\), which yields the first equation (DMm). In a similar way one shows that (COMPm) is equivalent to the second equation (DMm). Therefore both equations are equivalent, and one can assume only one of them in the definition from the preceding paragraph.

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.

The formulas of NL are built from variables \(p,q,r,\ldots \) by means of connectives \(\otimes ,\backslash ,/\). One defines bunches: (i) every formula is a bunch, (ii) if \(\Gamma \) and \(\Delta \) are bunches, then \((\Gamma ,\Delta )\) is a bunch. Bunches can be treated as the elements of the free groupoid generated by the set of formulas. NL-sequents are of the form \(\Gamma \Rightarrow A\), where \(\Gamma \) is a bunch and A is a formula. A context is a bunch containing a special atom x (a place for substitution). We denote formulas by \(A,B,C,\ldots \), bunches by \(\Gamma ,\Delta ,\Theta \), and contexts by \(\Gamma [\,],\Delta [\,]\) etc. \(\Gamma [\Delta ]\) denotes the result of substituting \(\Delta \) for x in \(\Gamma [\,]\). The axioms and the inference rules of NL are as follows.
$$\begin{aligned}&\text{(NL-id) } A\Rightarrow A\;\; \text{(NL-cut) } \frac{\Gamma [A]\Rightarrow B\;\;\Delta \Rightarrow A}{\Gamma [\Delta ]\Rightarrow B}\\&{(\otimes \Rightarrow ) }\frac{\Gamma [(A,B)]\Rightarrow C}{\Gamma [A\otimes B]\Rightarrow C}\;\;{ (\Rightarrow \otimes ) }\frac{\Gamma \Rightarrow A\;\;\Delta \Rightarrow B}{(\Gamma ,\Delta )\Rightarrow A\otimes B}\\&{(\backslash \Rightarrow ) }\frac{\Gamma [B]\Rightarrow C\;\;\Delta \Rightarrow A}{\Gamma [(\Delta ,A\backslash B)]\Rightarrow C}\;\;{ (\Rightarrow \backslash ) }\frac{(A,\Gamma ) \Rightarrow B}{\Gamma \Rightarrow A\backslash B}\\&{(/\Rightarrow ) }\frac{\Gamma [A]\Rightarrow C\;\;\Delta \Rightarrow B}{\Gamma [(A/B,\Delta )]\Rightarrow C}\;\;{ (\Rightarrow /) }\frac{(\Gamma ,B)\Rightarrow A}{\Gamma \Rightarrow A/B} \end{aligned}$$
InNL can be presented as an extension of NL with new unary connectives \(^{\sim },^{-}\), new axioms:
$$\begin{aligned} \text{(a.DN) } A^{-\sim }\Leftrightarrow A\,,A^{\sim -}\Leftrightarrow A\,, \text{(a.CON) } A^{\sim }/B\Leftrightarrow A\backslash B^{-} \end{aligned}$$
(\(A\Leftrightarrow B\) means: \(A\Rightarrow B\) and \(B\Rightarrow A\)), and new inference rules:
$$\begin{aligned} \text{(r-CON) } \frac{A\Rightarrow B}{B^{\sim }\Rightarrow A^{\sim }}\;\;\;\frac{A\Rightarrow B}{B^{-}\Rightarrow A^{-}}\,. \end{aligned}$$
CNL can be obtained from InNL by adding the axioms \(A^{\sim }\Leftrightarrow A^{-}\) (or replace \(^{-}\) by \(^{\sim }\) in all axioms and rules).

Using Lindenbaum-Tarski 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).

NLm admits modalities \(\Diamond ,\Box ^{\downarrow }\) and bunches with a new structural operation \(\langle \,\rangle \). The definition of a bunch is extended by: (iii) if \(\Gamma \) is a bunch, then \(\langle \Gamma \rangle \) is a bunch. In algebras, \(\mu (\langle \Gamma \rangle )=\Diamond (\mu (\Gamma ))\). One adds the following rules for modalities.
$$\begin{aligned}&{(\Diamond \Rightarrow ) }\frac{\Gamma [\langle A\rangle ]\Rightarrow B}{\Gamma [\Diamond A]\Rightarrow B}\;\;{ (\Rightarrow \Diamond ) }\frac{\Gamma \Rightarrow A}{\langle \Gamma \rangle \Rightarrow \Diamond A}\\&{(\Box ^{\downarrow }\Rightarrow ) }\frac{\Gamma [A]\Rightarrow B}{\Gamma [\langle \Box ^{\downarrow }A\rangle ]\Rightarrow B}\;\;{ (\Rightarrow \Box ^{\downarrow }) }\frac{\langle \Gamma \rangle \Rightarrow A}{\Gamma \Rightarrow \Box ^{\downarrow }A} \end{aligned}$$
NL and NLm admit cut elimination: (NL-cut) is redundant in the pure logic (Lambek 1961; Moortgat 1996). NLm is strongly complete with respect to modal residuated groupoids. InNLm is obtained from NLm like InNL from NL, with the new axiom:
$$\begin{aligned} \text{(a.DM) } (\Diamond A)^{\sim }\Leftrightarrow \Box ^{\downarrow }(A^{\sim }), \end{aligned}$$
and similarly for CNLm. (Notice that (a.DM) for \(^{-}\) is derivable in InNLm, like in algebras.) These logics are strongly complete with respect to the corresponding algebras. InNL, CNL, InNLm, CNLm, presented in this form, do not admit cut elimination. For instance, \(p/q\Rightarrow (q\otimes p^{\sim })^{-}\) is valid (see (IRG2)), hence provable in InNL, but it is not an axiom and can be the conclusion of (NL-cut) only.

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 (NL-id) 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), Bar-Hillel 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 (NL-id) 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 multi-modal 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).

Let us consider an example from Moot and Retoré (2012). By (RGm), np can be lifted up to both \(\Box ^{\downarrow }_{n}\Diamond _{n}np\) and \(\Box ^{\downarrow }_{a}\Diamond _{a}np\), where the subscripts abbreviate nominative and accusative. We assign np to ‘John’ and ‘Mary’, \(\Box ^{\downarrow }_{n}\Diamond _{n}np\) to ‘he’ and ‘she’, \(\Box ^{\downarrow }_{a}\Diamond _{a}np\) to ‘him’ and ‘her’, and
$$\begin{aligned} (\Box ^{\downarrow }_{n}\Diamond _{n}np\backslash s)/\Box ^{\downarrow }_{a}\Diamond _{a}np \end{aligned}$$
to ‘likes’. The resulting grammar, based on NLm, assigns s to ‘John likes Mary’, ‘he likes her’, but not to ‘her likes Mary’, ‘Mary likes he’. Notice that the typing from the preceding paragraph does not work for ‘he likes her’ on the basis of NL, since the sequence \(s/(np\backslash s),(np\backslash s)/np,(s/np)\backslash s\) is not the yield of any \(\Gamma \) such that \(\Gamma \Rightarrow s\) is provable in NL.

Logics with linear negations are much richer, but they are conservative extensions of their negation-free 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 NL-sequent 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 co-application 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\).

In Casadio (2001) and Casadio and Lambek (2002), Noncommutative MLL, which amounts to InL (i.e. the associative InNL) with 1, is directly employed as a logic underlying type grammars (Lambek’s name: Bilinear Logic). Lambek (1999) considers Compact Bilinear Logic (CBL), where \(\otimes =\oplus \) and \(1=0\); the algebraic models are called pregroups and the resulting type grammars pregroup grammars. Lambek writes \(A^{r}\) for \(A^{\sim }\) and \(A^{l}\) for \(A^{-}\) (\(A^{r}\) is the right and \(A^{l}\) the left adjoint of A). Table 1 shows some sample types in NL, InNL, and CBL. Here n is the type of common noun, and ‘whom’ is typed for contexts like ‘boy whom Mary likes’.
Table 1

Some sample types in different formalisms

Word

NL-type

InNL-type

CBL-type

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 NP-complete (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 one-sided sequent system for InNLm; the cut-elimination theorem is proved in a model-theoretic 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

By a phase space we mean a frame \((M,\cdot ,f,R)\) such that \(\cdot \) and f are a binary and a unary operation on M and \(R\subseteq M^{2}\). For logics without \(\Diamond ,\Box ^{\downarrow }\) one omits f. For \(X\subseteq M\) we define:
$$\begin{aligned} X^{\sim }=\{b\in M:\forall _{a\in X}\,R(a,b)\},\quad X^{-}=\{a\in M:\forall _{b\in X}\,R(a,b)\}. \end{aligned}$$
This yields a Galois connection: \(X\subseteq Y^{\sim }\) iff \(Y\subseteq X^{-}\), for all \(X,Y\subseteq M\). Consequently, \(^{\sim },^{-}\) reverse \(\subseteq \) and \(X^{\sim - \sim }=X^{\sim }\), \(X^{-\sim -}=X^{-}\), for any \(X\subseteq M\). The operations \(\phi _{R}(X)=X^{-\sim }\) and \(\psi _{R}(X)=X^{\sim -}\) are closure operations on \({{\mathcal {P}}}(M)\). Recall that an operation C on \({{\mathcal {P}}}(M)\) is called a closure operation, if it satisfies: (C1) \(X\subseteq C(X)\), (C2) if \(X\subseteq Y\) then \(C(X)\subseteq C(Y)\), (C3) \(C(C(X))=C(X)\), for all \(X,Y\subseteq M\). A set \(X\subseteq M\) is said to be C-closed, if \(X=C(X)\) (equivalently: \(X=C(Y)\), for some \(Y\subseteq M\)). One easily shows that X is \(\phi _{R}\)-closed (resp. \(\psi _{R}\)-closed) if and only if \(X=Y^{\sim }\) (resp. \(X=Y^{-}\)) for some \(Y\subseteq M\).
Given a groupoid \((M,\cdot )\), \(f:M\mapsto M\) and \(X,Y\subseteq M\), one defines:
$$\begin{aligned} X\cdot Y= & {} \{a\cdot b: a\in X, b\in Y\},\\ X\backslash Y= & {} \{b\in M: X\cdot \{b\}\subseteq Y\},\quad X/Y=\{a\in M:\{a\}\cdot Y\subseteq X\}.\,\\ \Diamond X= & {} f[X]=\{f(a):a\in X\},\quad \Box ^{\downarrow }X=f^{-1}[X]=\{a\in M:f(a)\in X\}.\, \end{aligned}$$
\({{\mathcal {P}}}(M)\) with these operations and \(\subseteq \) is a modal residuated groupoid. (URES) amounts to the well-known equivalence: \(f[X]\subseteq Y\) iff \(X\subseteq f^{-1}[Y]\).

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 C-closed set X and any \(Y\subseteq M\), the sets \(Y\backslash X\) and X / Y are C-closed, and (C5) to: (C5\('\)) for any C-closed set X, \(\Box ^{\downarrow }X\) is C-closed (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 C-closed 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}\).

A phase space \((M,\cdot ,f,R)\) is called a phase space for InNLm, if \(\phi _{R}=\psi _{R}\) and the following conditions hold:
(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(af(b)).

It is called a phase space for CNLm, if (Shift) and (mShift) hold and R is symmetric. Phase spaces for InNL (resp. CNL) are defined in a similar way; one forgets f and omits (mShift).

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

Let \((M,\cdot ,R)\) be a phase space. (Shift) is equivalent to each of the following conditions:
(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 one-element 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\}^{-}\).

The restricted (i) follows from (i). Also (i) follows from the restricted (i), since for \(X=\{a_{i}\}_{i\in I}\), \(Y=\{b_{j}\}_{j\in J}\), we obtain:
$$\begin{aligned} X^{\sim }/Y=\left( \bigcap _{i\in I}\{a_{i}\}^{\sim }\right) \Big /Y=\bigcap _{i\in I}\bigcap _{j\in J}\{a_{i}\}^{\sim }/\{b_{j}\}=\bigcap _{i\in I}\bigcap _{j\in J}\{a_{i}\}\backslash \{b_{j}\}^{-}=X\backslash Y^{-}. \end{aligned}$$
Here we use the distributive laws1 for \(\cdot ,\backslash ,/\) and:
$$\begin{aligned} \left( \bigcup _{i\in I}Z_{i}\right) ^{\sim }=\bigcap _{i\in I}Z_{i}^{\sim },\quad \left( \bigcup _{j\in J}Z_{j}\right) ^{-}=\bigcap _{j\in J}Z_{j}^{-}. \end{aligned}$$
So (Shift) is equivalent to (i). The remaining equivalences can be proved in a similar way. \(\square \)

Lemma 2

Let \((M,\cdot ,f,R)\) be a phase space. (mShift) is equivalent to each of the following conditions:
(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 one-element sets X. We have: \(b\in (\Diamond \{a\})^{\sim }\) iff R(f(a), b) iff R(af(b)) iff \(f(b)\in \{a\}^{\sim }\) iff \(b\in \Box ^{\downarrow }(\{a\}^{\sim })\). Conversely, (mShift) follows from (i) for one-element sets. Furthermore, (i) for all one-element 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 right-hand 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.

Now, we have:
$$\begin{aligned} X^{\sim }=\left( \bigcup _{a\in X}\{a\}\right) ^{\sim }=\bigcap _{a\in X}\{a\}^{\sim }. \end{aligned}$$
\(X^{\sim }\) is an intersection of \(\psi _{R}\)-closed sets, hence it is \(\psi _{R}\)-closed. So every \(\phi _{R}\)-closed set is \(\psi _{R}\)-closed. In a similar way, one shows that every \(\psi _{R}\)-closed set is \(\phi _{R}\)-closed. Then \(M_{\phi _{R}}=M_{\psi _{R}}\), which yields \(\phi _{R}=\psi _{R}\), since \(\phi _{R}(X)\) is the smallest \(\phi _{R}\)-closed set containing X, and similarly for \(\psi _{R}(X)\). \(\square \)

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

Our notion of a phase space exhibits a modal character of linear negations. For \(X\subseteq M\), we have:
$$\begin{aligned} X^{\sim }= & {} \{b\in M: \forall _{a}(\lnot R(a,b) \Rightarrow a\not \in X)\},\\ X^{-}= & {} \{a\in M:\forall _{b}(\lnot R(a,b)\Rightarrow b\not \in X)\}. \end{aligned}$$
Consequently, if \(\Box \) is the necessity operation defined (in the standard way) for the Kripke frame \((M,R^{c})\), where \(R^{c}=M^{2}-R\), then \(X^{-}=\Box X^{c}\). In the logical notation: \(A^{-}\Leftrightarrow \Box \lnot A\). Here \(\lnot \), \(\Rightarrow \) and \(\Leftrightarrow \) stand for negation, implication and equivalence of classical logic. Analogously, \(A^{\sim }\Leftrightarrow \Box ^{\downarrow }\lnot A\), where \(\Box ^{\downarrow }\) is defined as above except that R is replaced by its converse. One can interpret InNL and other linear logics in classical multi-modal logics, but we will not elaborate on this issue. For a thorough discussion of Lambek logics within the modal framework see van Benthem (1991).

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)\}\).

If \(R=R_{O}\), for \(O\subseteq M\), then (Shift) amounts to the following equivalence:
(Shift-O)

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

Clearly, (Shift-O) holds, if \(\cdot \) is associative. Therefore, in the literature on linear logics, which assume the associativity of product, no constraint of this kind was considered.

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(ab) 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(ab) 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(xy) 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 one-sided 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 \).

Our sequent system is denoted by S-InNLm. Its cut-free fragment admits the axioms:
$$\begin{aligned} \text{(id) } p^{(n)};p^{(n+1)} \text{ for } \text{ all } \text{ variables } p \text{ and } n\in {{\mathbb {Z}}} \end{aligned}$$
and the inference rules:
$$\begin{aligned}&\text{(r- }\otimes ) \frac{\Upsilon [(A,B)]}{\Upsilon [A\otimes B]}\\&\text{(r- }\oplus 1) \frac{\Upsilon [B]\;\;\Delta ;A}{\Upsilon [(\Delta ,A\oplus B)]}\;\;\text{(r- }\oplus 2) \frac{\Upsilon [A]\;\;B;\Delta }{\Upsilon [(A\oplus B,\Delta )]}\\&\text{(r- }\Diamond ) \frac{\Upsilon [\langle A \rangle ]}{\Upsilon [\Diamond A]}\;\; \text{(r- }\Box ^{\downarrow }) \frac{\Upsilon [A]}{\Upsilon [\langle \Box ^{\downarrow }A\rangle ]}\\&\text{(r-Shift) } \frac{\underline{(\Gamma ,\Delta );\Theta }}{\Gamma ;(\Delta ,\Theta )}\;\; \text{(r-mShift) } \frac{\underline{\langle \Gamma \rangle ;\Delta }}{\Gamma ;\langle \Delta \rangle } \end{aligned}$$
The algebraic models are modal involutive residuated groupoids. We assume that every valuation \(\mu \) satisfies: \(\mu (p^{(n+1)})=\mu (p^{(n)})^{\sim }\), for any atom \(p^{(n)}\). \(\mu \) is extended for bunches as for the case of NLm. We define: \({\mathbf M},\mu \models \Gamma ;\Delta \) iff \(\mu (\Gamma )\le \mu (\Delta )^{-}\) (equivalently: \(\mu (\Delta )\le \mu (\Gamma )^{\sim }\)).
Negations are defined in metalanguage.
$$\begin{aligned}&(p^{(n)})^{\sim }=p^{(n+1)}\;\;(p^{(n)})^{-}=p^{(n-1)}\\&(A\otimes B)^{\sim }=B^{\sim }\oplus A^{\sim }\;\;(A\oplus B)^{\sim }=B^{\sim }\otimes A^{\sim } \text{(similarly } \text{ for } ^{-})\\&(\Diamond A)^{\sim }=\Box ^{\downarrow }(A^{\sim })\;\;(\Box ^{\downarrow }A)^{\sim }=\Diamond (A^{\sim })\, \text{(similarly } \text{ for } ^{-}) \end{aligned}$$
For example, \((p^{-})^{\sim }=p\), \((p^{-})^{-}=p^{{-}{-}}\), \((p\otimes q^{\sim })^{-}=q\oplus p^{-}\). S-InNLm is restricted to formulas in negation normal form: negations occur at variables only. Moreover all pairs \(^{\sim -}\) and \(^{-\sim }\) are eliminated. In metalanguage one can apply negations to arbitrary formulas. This facilitates the presentation of the system. Buszkowski (2016) shows a more involved system for CNL with negation as a legal connective.

Notice that the rules of the cut-free S-InNLm 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 }\).

By induction on A, one easily proves \(A^{\sim -}=A\), \(A^{-\sim }=A\); also, if \(\mu \) is a valuation in a modal involutive residuated groupoid, then:
$$\begin{aligned} \mu (A^{\sim })=\mu (A)^{\sim },\;\;\mu (A^{-})=\mu (A)^{-}, \text{ for } \text{ any } \text{ formula } A. \end{aligned}$$
(1)
We define S-InNLm as the above system, enriched with the cut rules.
$$\begin{aligned} \text{(cut }^{\sim }) \frac{\Gamma [A]\;\;\Delta ;A^{\sim }}{\Gamma [\Delta ]}\;\; \text{(cut }^{-}) \frac{\Gamma [A]\;\;A^{-};\Delta }{\Gamma [\Delta ]} \end{aligned}$$
We want to prove that the cut-rules are admissible in the cut-free S-InNLm by a model-theoretic argument. We need an auxiliary system \(S_{0}\), which arises from S-InNLm, after one has replaced (r-Shift) with the following rules:
$$\begin{aligned} \text{(r- }\oplus 3) \frac{A;\Gamma \;\;B;\Delta }{A\oplus B;(\Delta ,\Gamma )}\;\; \text{(r- }\oplus 4) \frac{\Gamma ;A\;\;\Delta ;B}{(\Delta ,\Gamma );A\oplus B} \end{aligned}$$
and (r-mShift) with:
$$\begin{aligned} \text{(r- }\Box ^{\downarrow }1) \frac{A;\Gamma }{\Box ^{\downarrow }A;\langle \Gamma \rangle }\;\; \text{(r- }\Box ^{\downarrow }2) \frac{\Gamma ;A}{\langle \Gamma \rangle ;\Box ^{\downarrow }A}\,. \end{aligned}$$
Recall that a rule is derivable in a logic, if the conclusion is provable from the premise(s), and admissible, if the conclusion is provable whenever every premise is provable. (\(\hbox {r-}\oplus 3\)) is derivable in S-InNLm, by (\(\hbox {r-}\oplus 2\)) and (r-Shift), and (\(\hbox {r-}\oplus 4\)) is derivable, by (\(\hbox {r-}\oplus 1\)) and (r-Shift). Similarly, (\(\hbox {r-}\Box ^{\downarrow }1\)) and (\(\hbox {r-}\Box ^{\downarrow }2\)) are derivable, by (\(\hbox {r-}\Box ^{\downarrow }\)) and (r-mShift). By \(\vdash \) (resp. \(\vdash _{0}\)) we denote the provability in the cut-free S-InNLm (resp. \(S_{0}\)).

We need two proof-theoretic lemmas. The complete proofs of these lemmas for InNL can be found in Buszkowski (2017a).

Lemma 4

The rules (r-Shift), (r-mShift) 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 only-if 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 non-modal 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 only-if 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 \)

Consequently, \(\vdash \Upsilon \) if and only if \(\vdash _{0}\Upsilon \), for any sequent \(\Upsilon \). We need two new rules.
$$\begin{aligned} \text{(r- }^{\sim \sim }) \frac{A;\Gamma }{\Gamma ;A^{\sim \sim }}\;\; \text{(r- }^{{-}{-}}) \frac{\Gamma ;A}{A^{{-}{-}};\Gamma } \end{aligned}$$

Lemma 5

The rules (\(\hbox {r-}^{\sim \sim }\)), (\(\hbox {r-}^{{-}{-}}\)) are admissible in the cut-free S-InNLm.

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 non-modal 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 (r-mShift), hence \(\langle \Theta \rangle ;A^{\sim \sim }\), by the outer induction hypothesis. Then, \(\Theta ;\langle A^{\sim \sim }\rangle \), by (r-mShift), 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 S-InNLm, there would be problems for (r-Shift) and (r-mShift). For instance, if \(D;(\Gamma ,\Delta )\) arises from \((D,\Gamma );\Delta \) by (r-Shift), one cannot apply the inner induction hypothesis to the premise.

Corollary 1

\(\vdash A^{-};\Gamma \) if and only if \(\vdash \Gamma ; A^{\sim }\)

We write \(\Gamma \Rightarrow A\) for \(A^{-};\Gamma \) and define:
$$\begin{aligned}{}[A]=\{\Gamma :\,\vdash \Gamma \Rightarrow A\}. \end{aligned}$$
A sequent \(\Upsilon \) is said to be valid in InNLm, if \({{\mathbf {M}}},\mu \models \Upsilon \) for all modal involutive residuated groupoids \({\mathbf {M}}\) and all valuations \(\mu \) in \({\mathbf {M}}\). We prove that the cut-free S-InNLm is weakly complete. This proof resembles earlier proofs for different substructural logics (Lafont 1997; Galatos et al. 2007; Galatos and Jipsen 2013), but certain new arguments are needed (notice the usage of Corollary 1 in the proof).

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 (r-Shift) and (COMPm) for (r-mShift).

For the ‘if’ part, we construct a counter-model 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 (r-mShift).

For any formula A, we have: \([A]=\{\Gamma :\,R(A^{-},\Gamma )\}=\{\Gamma :\,R(\Gamma ,A^{\sim })\}\), by Corollary 1, which yields:
$$\begin{aligned}{}[A]=\{A^{-}\}^{\sim }=\{A^{\sim }\}^{-},\quad [A^{\sim }]=\{A\}^{\sim },\quad [A^{-}]=\{A\}^{-}. \end{aligned}$$
(2)
Consequently, [A] is \(\phi _{R}\)-closed and \(\psi _{R}\)-closed, for any formula A. Then, for any A, \(\{A\}^{\sim }\) is \(\psi _R\)-closed and \(\{A\}^{-}\) is \(\phi _R\)-closed. We obtain \(\phi _{R}=\psi _{R}\), by Lemma 3. So \((M,\cdot ,f,R)\) is a phase space for InNLm.
By Theorem 1, the algebra \((M_{R},\otimes _{R},\backslash ,/,\Diamond _{R},\Box ^{\downarrow },^{\sim },^{-},\subseteq )\) is a modal involutive residuated groupoid. We define a valuation \(\mu \).
$$\begin{aligned}&\mu (p)=[p]\\&\mu (p^{(n+1)})=\mu (p^{(n)})^{\sim } \text{ for } n\ge 0,\;\;\mu (p^{(n-1)})=\mu (p^{(n)})^{-} \text{ for } n\le 0 \end{aligned}$$
By induction on the number of connectives in A, we prove:
$$\begin{aligned} A\in \mu (A)\subseteq [A] \text{ for } \text{ any } \text{ formula } A\,. \end{aligned}$$
(3)
\(A=p^{(n)}\). We proceed by induction on |n|. For \(n=0\), we have \(\mu (p)=[p]\) and \(p\in [p]\), since \(p;p^{\sim }\) is an axiom. Assume (3) for \(n\ge 0\). From \(\mu (p^{(n)})\subseteq [p^{(n)}]=\{p^{(n+1)}\}^{-}\) (use (2)) we obtain \(\{p^{(n+1)}\}^{-\sim }\subseteq \mu (p^{(n)})^{\sim }=\mu (p^{(n+1)})\) (use (1)), and \(p^{(n+1)}\in \phi _{R}(\{p^{(n+1)}\})=\{p^{(n+1)}\}^{-\sim }\), hence \(p^{(n+1)}\in \mu (p^{(n+1)})\). From \(\{p^{(n)}\}\subseteq \mu (p^{(n)})\) we obtain \(\mu (p^{(n+1)})\subseteq \{p^{(n)}\}^{\sim }=[p^{(n+1)}]\) (use (1), (2)). In a similar way, assuming (3) for \(n\le 0\), we obtain (3) for \(n-1\).
\(A=B\otimes C\). We need the following property.
(P1)

If \(X\in M_{R}\) and \((B,C)\in X\), then \(B\otimes C\in X\).

Assume that \(X\in M_{R}\) and \((B,C)\in X\). Fix Y such that \(X=Y^{\sim }\). For all \(\Gamma \in Y\), \(\vdash \Gamma ;(B,C)\), hence \(\vdash \Gamma ;B\otimes C\), by \(\hbox {(r-}\otimes \)). So \(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]\).

\(A=\Diamond B\). We need an analogue of (P1); the proof is left to the reader.
(P1m)

if \(X\in M_{R}\) and \(\langle B\rangle \in X\), then \(\Diamond B\in X\).

By the induction hypothesis, (3) holds for B. From \(B\in \mu (B)\) we get \(\langle B\rangle \in \Diamond \mu (B)\subseteq \Diamond _{R}\mu (B)=\mu (A)\). So \(A\in \mu (A)\), by (P1m). Also \(\mu (B)\subseteq [B]=\{B^{-}\}^{\sim }\). Hence for all \(\Gamma \in \mu (B)\), \(\vdash B^{-};\Gamma \). By \(\hbox {(r-}\Box ^{\downarrow }1\)), \(\vdash \Box ^{\downarrow }(B^{-});\langle \Gamma \rangle \). Consequently, \(\Diamond (\mu (B))\subseteq \{(\Diamond B)^{-}\}^{\sim }=[\Diamond B]\), which yields \(\mu (A)=\Diamond _{R}(\mu (B))\subseteq [A]\).

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 cut-free S-InNLm.

Proof

Both rules preserve the truth for \(\mu \) in \({\mathbf {M}}\), hence the validity. \(\square \)

This model-theoretic proof of the cut-elimination theorem is not constructive. A constructive, syntactic proof for S-InNL is given in Buszkowski (2017a).

Theorem 3

S-InNLm 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 S-InNLm 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 S-InNLm. 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 }\)).

We consider a phase space \((M,\cdot ,f,R)\), defined as in the proof of Theorem 2 except that: \(R(\Gamma ,\Delta )\) iff \(\Phi \vdash \Gamma ;\Delta \). We define \([A]=\{\Gamma :\,\Phi \vdash \Gamma \Rightarrow A\}\), where \(\Gamma \Rightarrow A\) is as above. The equations (2) hold. Accordingly, \((M,\cdot ,f,R)\) is a phase space for InNLm. We consider the modal involutive residuated groupoid \(M_{R}\) and the valuation \(\mu \), defined there. One proves (3), and its stronger form:
$$\begin{aligned} \mu (A)=[A] \text{ for } \text{ any } \text{ formula } A. \end{aligned}$$
(4)
We need the following property.
(P2)

If \(X\in M_{R}\) and \(A\in X\), then \([A]\subseteq X\).

Assume that \(X\in M_{R}\) and \(A\in X\). Fix Y such that \(X=Y^{\sim }\). Then, \(\Phi \vdash \Gamma ;A\) for all \(\Gamma \in Y\), and consequently, \(\Phi \vdash \Gamma ;\Delta \) for all \(\Gamma \in Y\), \(\Delta \in [A]\) (use (cut\(^{-}\))). So \([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 S-InNLm is divided in two parts by semicolon, this does not mean that the system is two-sided. 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 S-InNLm 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 one-sided 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 two-sided systems with sequents \(\Gamma \Rightarrow \Delta \), the standard one-sided 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 S-InNLm 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 S-InNLm in essentially the same way or even inferred from our results, using natural symmetries, e.g. \(\Gamma ;\Delta \) is provable in S-InNLm 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 one-sided 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 well-formed 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 cut-free systems do not possess the subformula property.3 Galatos and Jipsen (2013) introduce a two-sided 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 k-cyclic, if \(a^{(k)}=a\) for any \(a\in M\) (Galatos and Jipsen 2013).4 Notice that \(a^{-}=a^{(k-1)}\) in k-cyclic algebras of this kind, since \(a^{-\sim }=a=a^{(k)}=(a^{(k-1)})^{\sim }\) and \(^{\sim }\) is a bijection, by (DN). In particular, ‘2-cyclic’ 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 k-cyclic modal involutive residuated groupoids. InNLm(2) amounts to CNLm.

We introduce a sequent system S-InNLm(k). The atoms are of the form \(p^{(n)}\) for \(0\le n< k\). All axioms and rules are as for S-InNLm, but n, \(n+1\) are computed modulo k. So the axioms are: \(p^{(n)};p^{(n+1)}\), for \(0\le n<k-1\) and \(p^{(k-1)};p\).

The metalanguage negations \(^{\sim },^{-}\) are defined as in Sect. 3 (we compute \(n+1\) and \(n-1\) 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 k-cyclic modal involutive residuated groupoid. Lemmas 4 and 5 remain true; now \(S_{0}\) arises from S-InNLm(k) like the former \(S_{0}\) from S-InNLm.

Theorem 4

The cut-free S-InNLm(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 k-cyclic. 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 k-cyclic. 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 cut-free S-InNLm(k). With these rules S-InNLm(k) is strongly complete with respect to k-cyclic modal involutive residuated groupoids. Again the proof of Theorem 3 can be repeated, and we consider \({{\mathbf {M}}}^{\mu }_{R}\) as above.

Now it can be shown that \(M_{R}\) in the proof of Theorem 4 is k-cyclic. Since the cut rules are admissible, then (4) holds. This yields \([A]^{(n)}=\mu (A)^{(n)}=\mu (A^{(n)})=[A^{(n)}]\), for any \(n\in {{\mathbb {Z}}}\), hence \([A]^{(k)}=[A]\), for any formula A. For any bunch \(\Gamma \), \(\{\Gamma \}^{\sim }=\{F(\Gamma )\}^{\sim }\), by the \(\otimes \)-rules, \(\hbox {(r-}\Diamond \)) and the cut rules. Consequently \(\{\Gamma \}^{\sim }=[F(\Gamma )^{\sim }]\), by (2). Let \(X\in M_{R}\). We fix Y such that \(X=Y^{\sim }\). Clearly \(Y^{\sim }=\bigcap _{\Gamma \in Y}\{\Gamma \}^{\sim }=\bigcap _{\Gamma \in Y}[F(\Gamma )^{\sim }]\). Since the negations in \(M_{R}\) satisfy (DN), they satisfy the infinite De Morgan laws in the complete lattice \(M_{R}\). In particular: \((\bigwedge _{i\in I}X_{i})^{\sim }=\bigvee _{i\in I}X_{i}^{\sim }\) and \((\bigvee _{i\in I}X_{i})^{\sim }=\bigwedge _{i\in I}X_{i}^{\sim }\), where \(\bigwedge _{i\in I}X_{i}=\bigcap _{i\in I}X_{i}\) and \(\bigvee _{i\in I}X_{i}=\phi _{R}(\bigcup _{i\in I}X_{i})\). So \((\bigwedge _{i\in I}X_{i})^{(k)}=\bigwedge _{i\in I}(X_{i})^{(k)}\), since k is even. Therefore:
$$\begin{aligned} X^{(k)}=\left( \bigwedge _{\Gamma \in Y}[F(\Gamma )^{\sim }]\right) ^{(k)}=\bigwedge _{\Gamma \in Y}[F(\Gamma )^{\sim }]^{(k)}=\bigwedge _{\Gamma \in Y}[F(\Gamma )^{\sim }]=X. \end{aligned}$$
We return to S-InNLm. For any sequent \(\Upsilon \) and \(m\in {\mathbb Z}\), by \(\tau (\Upsilon ,m)\) we denote the sequent arising from \(\Upsilon \), after one has replaced each atom \(p^{(n)}\) by \(p^{(n+m)}\).

Lemma 6

For any sequent \(\Upsilon \) and \(m\in {{\mathbb {Z}}}\), \(\Upsilon \) is provable in S-InNLm if and only if \(\tau (\Upsilon ,m)\) is provable in S-InNLm.

Proof

Assume that \(\Upsilon \) is provable in S-InNLm. 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 only-if 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 S-InNLm if and only if \(\Upsilon \) is provable in S-InNLm(k).

Proof

Assume that \(\Upsilon \) is provable in S-InNLm. Then \(\Upsilon \) is valid in InNLm, and consequently, in k-cyclic modal involutive residuated groupoids. By Theorem 4, \(\Upsilon \) is provable in S-InNLm(k).

Assume that \(\Upsilon \) is provable in S-InNLm(k). There exists a (cut-free) proof of \(\Upsilon \) in this system. Every formula in this proof is a subformula of a formula in \(\Upsilon \). Consequently, no atom \(p^{(k-1)}\) appears in this proof, hence no axiom \(p^{(k-1)};p\) is used. This proof is a proof in S-InNLm. \(\square \)

Therefore, if a sequent \(\Upsilon \) is not provable in InNLm, then it is not valid in some k-cyclic modal involutive residuated groupoid. An analogous result for InGL was obtained in Galatos and Jipsen (2013) with the aid of a two-sided 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 T-sequent we mean a sequent consisting of formulas from T. A proof consisting of T-sequents is called a T-proof. Now, \(\vdash \) stands for the provability in InNLm(k) and \(\vdash _{T}\) for the provability in InNLm(k), restricted to T-proofs. Again we assume that all sequents in \(\Phi \) are of the form AB. 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 S-InNLm(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 (r-Shift), top-down, 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 (r-mShift), top-down, 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^{(k-1)}\). 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 k-cyclic 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 property5 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) context-free 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 (NL-cut). 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 (NL-cut). Clearly \(\Theta [D]\) has less commas than \(\Gamma \). This yields a context-free 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 context-free. It is known that every \(\epsilon \)-free context-free 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 AB, or (AB); C, or A; (BC), or \(\langle A\rangle ;B\), or \(A;\langle B\rangle \). Let T be a finite set of formulas. Let \(S^{T}\) denote S-InNLm(k) (with the cut rules), augmented with a finite \(\Phi \) (consisting of T-sequents of the form AB), 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 S-InNLm(k) from \(\Phi \), are provable in \(S^{T}\).

For this goal we consider a system S(T), whose axioms are all sequents provable in \(S^{T}\) and the only rules are (cut\(^{\sim }\)), (cut\(^{-}\)), limited to c(T)-sequents. Like in the proof of Theorem 3, one shows that (\(\hbox {r-}^{\sim \sim }\)) and (\(\hbox {r-}^{{-}{-}}\)) are derivable in S(T), if the premise is a c(T)-sequent. We need the following properties.
(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 only-if 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 (AB); 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 only-if 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 (r-mShift), top-down. 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 (r-mShift). 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 58 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 context-free 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 context-free, by Theorem 7. Like in the proof of Theorem 7, one shows that every \(\epsilon \)-free context-free 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 P-TIME.

Accordingly, a context-free 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 NP-complete (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 ABC). 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\).

Furthermore, InNL (resp. InNLm) is a strongly conservative extension of NL (resp. NLm), but this requires a more involved proof. Using phase spaces for CNL, Buszkowski (2016) shows that CNL is strongly conservative over NL, and consequently, InNL is so, since it is an intermediate logic. In a similar way one can prove that CNLm (hence also InNLm, InNLm(k)) is a strongly conservative extension of NLm. We omit the proof. We only note that the sequent system for CNL in Buszkowski (2016) is different from S-InNL(2). In particular, it admits the symmetry rule.
$$\begin{aligned} \text{(r-sym) } \frac{\Gamma ;\Delta }{\Delta ;\Gamma } \end{aligned}$$
This rule is admissible in the cut-free S-InNLm(2) and derivable in S-InNLm(2). Using (r-Shift), (r-mShift) and (r-sym), one can transform every sequent \(\Upsilon [A]\) into a unique sequent of the form \(A;\Theta \). This plays an essential role in the omitted proof.

Footnotes

  1. 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. 2.

    The rules for connectives in S-InNLm correspond to the left introduction rules in NLm [for \(\oplus \), see (IRG3)].

  3. 3.

    Theorem 4.4.2 in Bastenhof (2013) is an analogue of our Corollary 2 for one of those systems, but its proof is not fully correct.

  4. 4.

    If k is odd, this condition entails \(a\otimes b=b\oplus a\) and: \(a\le b\) iff \(a=b\).

  5. 5.

    This means: Every unprovable pattern \(\Phi \vdash \Upsilon \), where \(\Phi \) is finite, can be falsified in a finite model.

References

  1. 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
  2. Ajdukiewicz, K. (1935). Die syntaktische Konnexität. Studia Philosophica, 1, 1–27.Google Scholar
  3. Bar-Hillel, 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
  4. Bastenhof, A. (2013). Categorial symmetry. Ph.D. thesis, University of Utrecht.Google Scholar
  5. 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
  6. Buszkowski, W. (2011). Interpolation and FEP for logics of residuated algebras. Logic Journal of IGPL, 19, 437–454.CrossRefGoogle Scholar
  7. 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
  8. Buszkowski, W. (2017a). Involutive nonassociative Lambek calculus: Sequent systems and complexity. Bulletin of the Section of Logic, 46(1–2), 75–91.Google Scholar
  9. 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
  10. Casadio, C. (2001). Non-commutative linear logic in linguistics. Grammars, 4(3), 167–185.CrossRefGoogle Scholar
  11. Casadio, C., & Lambek, J. (2002). A tale of four grammars. Studia Logica, 71(3), 315–329.CrossRefGoogle Scholar
  12. de Groote, Ph, & Lamarche, F. (2002). Classical non-associative Lambek calculus. Studia Logica, 71(3), 355–388.CrossRefGoogle Scholar
  13. Galatos, N., & Jipsen, P. (2013). Residuated frames with applications to decidability. Transactions of American Mathematical Society, 365, 1219–1249.CrossRefGoogle Scholar
  14. Galatos, N., Jipsen, P., Kowalski, T., & Ono, H. (2007). Residuated lattices. An algebraic glimpse at substructural logics. Amsterdam: Elsevier.Google Scholar
  15. Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science, 50, 1–102.CrossRefGoogle Scholar
  16. Grishin, V. N. (1983). On a generalization of the Ajdukiewicz–Lambek system. In A. I. Mikhailov (Ed.), Studies in non-classical logics and formal systems (pp. 315–343). Moscow: Nauka.Google Scholar
  17. Lafont, Y. (1997). The finite model property of various fragments of linear logic. Journal of Symbolic Logic, 62, 1202–1208.CrossRefGoogle Scholar
  18. Lambek, J. (1958). The mathematics of sentence structure. The American Mathematical Monthly, 65, 154–170.CrossRefGoogle Scholar
  19. 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
  20. Lambek, J. (1995). Cut elimination for classical bilinear logic. Fundamenta Informaticae, 22, 53–67.Google Scholar
  21. 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
  22. Lin, Z. (2014). Non-associative Lambek calculus with modalities: Interpolation, complexity and FEP. Logic Journal of The IGPL, 22, 494–512.CrossRefGoogle Scholar
  23. Moortgat, M. (1996). Multimodal linguistic inference. Journal of Logic, Language, and Information, 5, 349–385.CrossRefGoogle Scholar
  24. 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
  25. Moortgat, M. (2009). Symmetric categorial grammar. Journal of Philosophical Logic, 38(6), 681–710.CrossRefGoogle Scholar
  26. Moot, R., & Retoré, C. (2012). The logic of categorial grammars. LNCS (Vol. 6850). Berlin: Springer.CrossRefGoogle Scholar
  27. Morrill, G. (1994). Type logical grammar. Categorial logic of signs. Dordrecht: Kluwer.CrossRefGoogle Scholar
  28. Pentus, M. (1993). Lambek grammars are context-free. In Proceedings of the 8 IEEE symposium on logic in computer science (pp. 429–433).Google Scholar
  29. Pentus, M. (2006). Lambek calculus is NP-complete. Theoretical Computer Science, 357, 186–201.CrossRefGoogle Scholar
  30. Restall, G. (2000). An introduction to substructural logics. New York: Routledge.CrossRefGoogle Scholar
  31. van Benthem, J. (1991). Language in action. Categories, lambdas and dynamic logic. Amsterdam: North-Holland.Google Scholar
  32. Yetter, D. N. (1990). Quantales and (non-commutative) linear logic. Journal of Symbolic Logic, 55, 41–64.CrossRefGoogle Scholar

Copyright information

© The Author(s) 2018

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.

Authors and Affiliations

  1. 1.The Adam Mickiewicz University in PoznańPoznanPoland

Personalised recommendations