Logic, Language, Information, and Computation: 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, July 2-5, 2019, Proceedings
Language and relational models, or L-models and R-models, are two natural classes of models for the Lambek calculus. Completeness w.r.t. L-models was proved by Pentus and completeness w.r.t. R-models by Andréka and Mikulás. It is well known that adding both additive conjunction and disjunction together yields incompleteness, because of the distributive law. The product-free Lambek calculus enriched with conjunction only, however, is complete w.r.t. L-models (Buszkowski) as well as R-models (Andréka and Mikulás). The situation with disjunction turns out to be the opposite: we prove that the product-free Lambek calculus enriched with disjunction only is incomplete w.r.t. L-models as well as R-models. If the empty premises are allowed, the product-free Lambek calculus enriched with conjunction only is still complete w.r.t. L-models but in which the empty word is allowed. Both versions are decidable (PSPACE-complete in fact). Adding the multiplicative unit to represent explicitly the empty word within the L-model paradigm changes the situation in a completely unexpected way. Namely, we prove undecidability for any L-sound extension of the Lambek calculus with conjunction and with the unit, whenever this extension includes certain L-sound rules for the multiplicative unit, to express the natural algebraic properties of the empty word. Moreover, we obtain undecidability for a small fragment with only one implication, conjunction, and the unit, obeying these natural rules. This proof proceeds by the encoding of two-counter Minsky machines.
The Lambek calculus was introduced as a mathematical description of natural languages. The original Lambek calculus is NP-complete (Pentus), while its product-free fragment with only one implication is polynomially decidable (Savateev). We consider Lambek calculus with the additional connectives: conjunction and disjunction. It is known that this system is PSPACE-complete (Kanovich, Kanazawa). We prove, in contrast with the polynomial-time result for the product-free Lambek calculus with one implication, that the derivability problem is still PSPACE-complete even for a very small fragment (∖,∧), including one implication and conjunction only. PSPACE-completeness is also provided for the (∖,∨) fragment, which includes only one implication and disjunction. Categorial grammars based on the original Lambek calculus generate exactly the class of context-free languages (Gaifman, Pentus). The class of languages generated by Lambek grammars extended with conjunction is known to be closed under intersection (Kanazawa), and therefore includes all finite intersections of context-free languages and, moreover, images of such intersections under alphabetic homomorphisms. We show that the same closure under intersection holds for Lambek grammars extended with disjunction, even for our small (∖,∨) fragment.
We present a sequent calculus for the weak Grzegorczyk logic 𝖦𝗈 allowing non-well-founded proofs and obtain the cut-elimination theorem for it by constructing a continuous cut-elimination mapping acting on these proofs.