Abstract
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.
Similar content being viewed by others
References
A. R. Anderson andN. D. Belnap Jr,Entailment: The Logic of Relevance and Necessarity, vol. 1, Princeton University Press, 1975.
K. Došen,A brief survey of frames for the Lambek calculus,Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 38 (1992), pp. 179–187.
J. M. Dunn,Relevance logic and entailment, inHandbook of Philosophical Logic III, D. Gabbay and F. Guenthner (eds), D. Reidel Publ. Co., Dordrecht 1986, pp. 117–224.
J. Y. Girard,Linear logic,Theoretical Computer Science 50 (1987), pp. 1–102.
S. A. Kripke,The problem of entailment (abstract),Journal of Symbolic Logic 24 (1959), p. 324.
R. K. Meyer,Improved decision procedures for pure relevant logic. Unpublished manuscript, 1973.
H. Ono andY. Komori,Logics without the contraction rule,Journal of Symbolic Logic 50 (1985), pp. 169–201.
A. S. Troelstra,Lectures on Linear Logic, CSLI Lecture Notes No. 29, 1992.
Author information
Authors and Affiliations
Additional information
The first author wishes to thank IIAS-SIS (Fujitsu Laboratories Ltd., Numazu) for 9 months hospitality in Japan, and for facilitating this research.
Rights and permissions
About this article
Cite this article
Meyer, R.K., Ono, H. The finite model property for BCK and BCIW. Stud Logica 53, 107–118 (1994). https://doi.org/10.1007/BF01053025
Received:
Revised:
Issue Date:
DOI: https://doi.org/10.1007/BF01053025