The finite model property for BCI and related systems (Q2563452)

This paper answers problems posed by Meyer and Ono in proving the finite model property (\(A\) is provable if \(A\) is valid in every finite model) for BCI logic, BCI logic with conjunction and some restricted versions of these systems in the style of the lambda calculus. The author uses the ``method of barriers'' which he introduced to prove the same property for the product free lambda calculus and the commutative product free lambda calculus.