Relational semantics of the Lambek calculus extended with classical propositional logic (Q456962)

There are known different variants of Lambek calculus that is used as a formal system for deriving reduction laws of syntactic types. The authors consider nonassociative and associative Lambek calculus extended with propositional connectives (PLN and PL, respectively). There are two main results of the paper. The first of them is the completeness theorem of PLN with respect to relational semantics. A corollary from this theorem is that PLN is a conservative extension of nonassociative Lambek calulus and of classical propositional logic. The second result of the paper is the decidability of PLN. It follows from the finite model property (FMP) of relational semantics. The authors obtain the FMP for nonassociative Lambek calculus using a filtration technique.