Abstract

We prove the finite model property (fmp) for BCI and BCI with additive conjunction, which answers some open questions in Meyer and Ono [11]. We also obtain similar results for some restricted versions of these systems in the style of the Lambek calculus [10, 3]. The key tool is the method of barriers which was earlier introduced by the author to prove fmp for the product-free Lambek calculus [2] and the commutative product-free Lambek calculus [4].