In this paper we compare grammatical inference in the context of simple and of mixed Lambek systems. Simple Lambek systems are obtained by taking the logic of residuation for a family of multiplicative connectives /,,\, together with a package of structural postulates characterizing the resource management properties of the connective.Different choices for Associativity and Commutativity yield the familiar logics NL, L, NLP, LP. Semantically, a simple Lambek system is a unimodal logic: the connectives get a Kripke style interpretation in terms (...) of a single ternary accessibility relation modeling the notion of linguistic composition for each individual system.The simple systems earch have their virtues in linguistic analysis. But none of them in isolation provides a basis for a full theory of grammar. In the second part of the paper, we consider two types of mixed Lambek systems. (shrink)

We will give here a purely algebraic proof of the cut elimination theorem for various sequent systems. Our basic idea is to introduce mathematical structures, called Gentzen structures, for a given sequent system without cut, and then to show the completeness of the sequent system without cut with respect to the class of algebras for the sequent system with cut, by using the quasi-completion of these Gentzen structures. It is shown that the quasi-completion is a generalization of the MacNeille completion. (...) Moreover, the finite model property is obtained for many cases, by modifying our completeness proof. This is an algebraic presentation of the proof of the finite model property discussed by Lafont [12] and Okada-Terui [17]. (shrink)

We prove Finite Embeddability Property for the class of residuated groupoids. The problem whether the class has FEP was left open by Blok and van Alten in "On the finite embeddability property for residuated ordered groupoids", Transactions of the AMS 357, pp. 4141--4157. We combine proof theoretic and algebraic methods.

A residuated algebra is a generalization of a residuated groupoid; instead of one basic binary operation with residual operations \,/, it admits finitely many basic operations, and each n-ary basic operation is associated with n residual operations. A logical system for RAs was studied in e.g. [6, 8, 15, 16] under the name: Generalized Lambek Calculus GL. In this paper we study GL and its extensions in the form of sequent systems. We prove an interpolation property which allows to replace (...) a substructure of the antecedent structure by a single formula in a provable sequent. Together with model constructions, based on nuclei [13], interpolation leads to proofs of Finite Embeddability Property for different classes of RAs, as e.g. all RAs, distributive lattice-ordered RAs, boolean RAs, Heyting RAs and double RAs. (shrink)

Nonassociative Lambek Calculus (NL) is a syntactic calculus of types introduced by Lambek [8]. The polynomial time decidability of NL was established by de Groote and Lamarche [4]. Buszkowski [3] showed that systems of NL with finitely many assumptions are decidable in polynomial time and generate context-free languages; actually the P-TIME complexity is established for the consequence relation of NL. Adapting the method of Buszkowski [3] we prove an analogous result for Nonassociative Lambek Calculus with unit (NL1). Moreover, we show (...) that any Lambek grammar based on NL1 (with assumptions) can be transformed into an equivalent context-free grammar in polynomial time. (shrink)