Abstract
We introduce subsystems WLJ and SI of the intuitionistic propositional logic LJ, by weakening the intuitionistic implication. These systems are justifiable by purely constructive semantics. Then the intuitionistic implication with full strength is definable in the second order versions of these systems. We give a relationship between SI and a weak modal system WM. In Appendix the Kripke-type model theory for WM is given.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
E. W. Beth, The Foundations of Mathematics, Amsterdam, 1959.
M. Dummett, Elements of Intuitionism, Oxford University Press, 1977.
G. Gentzen, Investigations into Logical Deduction, in The Collected Papers of Gerhart Gentzen, translated by M. Szabo, North-Holland, 1969. Untersuchungen über das logische Schliessen, Mathematische Zeitschrift 39 (1935), pp. 176–210, 405–565.
G. Gentzen, The consistency proof of elementary number theory, ibid. Die WiSpruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen, 112 (1936), pp. 493–565.
M. Okada, On a theory of weak implication, to appear in Journal of Symbolic Logic 52 (1987), No. 4.
D. Prawitz, Natural Deduction, Stockholm, 1965.
G. Takeuti, Proof Theory, North-Holland, 1975.
Author information
Authors and Affiliations
Additional information
This work was partially supported by NSF Grant DCR85-13417
Rights and permissions
About this article
Cite this article
Okada, M. A weak intuitionistic propositional logic with purely constructive implication. Stud Logica 46, 371–382 (1987). https://doi.org/10.1007/BF00370647
Received:
Revised:
Issue Date:
DOI: https://doi.org/10.1007/BF00370647