Nonassociative Lambek Calculus with Additives and Context-Free Languages, Francez Festschrift, O. Grunberg et al

Abstract. We study Nonassociative Lambek Calculus with additives ∧,∨, satisfying the distributive law (Distributive Full Nonassociative Lambek Calculus DFNL). We prove that categorial grammars based on DFNL, also enriched with assumptions, generate context-free lan-guages. The proof uses proof-theoretic tools (interpolation) and a con-struction of a finite model, earlier employed in [11] in the proof of Finite Embeddability Property (FEP) of DFNL; our paper is self-contained, since we provide a simplified version of the latter proof. We obtain anal-ogous results for different variants of DFNL, e.g. BFNL, which admits negation ¬ such that ∧,∨, ¬ satisfy the laws of boolean algebra, and HFNL, corresponding to Heyting algebras with an additional residua-tion structure. Our proof also yields Finite Embeddability Property of boolean-ordered and Heyting-ordered residuated groupoids. The paper joins proof-theoretic and model-theoretic techniques of modern logic with standard tools of mathematical linguistics.