Non-commutative linear logic in linguistics (Q700787)

Classical non-commutative linear logic have been investigated by \textit{V. M. Abrusci} [J. Symb. Log. 56, No. 4, 1403--1451 (1991; Zbl 0746.03044); Lond. Math. Soc. Lect. Note Ser. 222, 271--296 (1995; Zbl 0828.03028)], while non-commutative intuitionistic linear logic (NILL), restricted to the multiplicative fragment, was first introduced in the \textit{syntactic calculus} of \textit{J. Lambek} [Am. Math. Mon. 65, 154--170 (1958; Zbl 0080.00702)], where the basic connectives of syntactic calculus, the tensor product \(\cdot\), the left division \(\backslash\) and the right division \(/\), respectively correspond to the multiplicative conjunction and the two implications (linear post-implication and linear retro-implication) of NILL so that the synthetic calculus corresponds precisely to the multiplicative, exponential-free, fragment of NILL. In standard categorical grammar [\textit{K. Ajdukiewicz}, Stud. Philos. 1, 1--27 (1935; Zbl 0015.33702); \textit{Y. Bar-Hillel}, in: Language and Information 61--74 (1964); Language 29, 47--58 (1953; Zbl 0156.25402)], the communication between linguistic expressions is essentially obtained by means of function-argument relation, being unable to derive discontinuous domains or long-distance relations, while Lambek's syntactic calculus allows a dynamic treatment of linguistic resources by means of flexible systems of inference rules such as the type raising rule. This paper proposes a new way of looking at the formal resources of the syntactic calculus by taking advantage of the logical properties of classical noncommutative linear logic with particular reference to its multiplicative \(\backslash\) and exponential-free fragment (MNLL), a conservative extension of the syntactic calculus. Although MNLL has formulations both in the two-sided sequent calculus and in the one-sided sequent calculus, the author works in the one-sided sequent calculus, because the chosen system enjoys cut-elimination, allowing the introduction of planar proof nets that are significantly appropriate for the geometric representations of linguistic environments. It is shown that the multiplicative system MNLL offers a suitable environment for the formal analysis of natural language, due to its classical setting allowing the de Morgan laws and the laws for the two negations. The calculus in this paper is essentially syntactic, missing both the prosodic and semantic dimensions that are necessary for the foundation of a complete type logical grammar.