The finite model property for BCK and BCIW

This paper shows that both implicational logicsBCK andBCIW have the finite model property. The proof of the finite model property forBCIW, which is equal to the relevant logicR , was originally given by the first author in his unpublished paper 6] in 1973. The finite model property forBCK can be obtained by modifying the proof of that forBCIW. Here, both of these proofs will be given in a unified form and the difference between them will be clarified. Further discussions will be given in the last section.The first author wishes to thank IIAS-SIS (Fujitsu Laboratories Ltd., Numazu) for 9 months hospitality in Japan, and for facilitating this research.Presented byJan Zygmunt