Reverse mathematics and completeness theorems for intuitionistic logic. (English) Zbl 1036.03008

This article investigates the mathematical logic of intuitionistic propositional and predicate calculi using the framework of reverse mathematics [S. G. Simpson, Subsystems of second order arithmetic, Berlin: Springer (1999; Zbl 0909.03048)]. Working in RCA\(_0\), the author shows that a version of the strong completeness theorem asserting the existence of a particular sort of Kripke model is equivalent to ACA\(_0\). The paper includes a proof that the saturation lemma for intuitionistic predicate logic is equivalent to WKL\(_0\). These results can also be found in §{3.2} of the author’s thesis [Model-theoretic studies on subsystems of second order arithmetic, Tohoku Mathematical Publications. 17. Sendai: Tohoku Univ. (2000; Zbl 0964.03059)].


03B20 Subsystems of classical logic (including intuitionistic logic)
03B30 Foundations of classical theories (including reverse mathematics)
03F35 Second- and higher-order arithmetic and fragments
03F55 Intuitionistic mathematics
Full Text: DOI


[1] Gabbay, D. M., Semantical Investigations in Heyting’s Intuitionistic Logic , vol. 148 of Synthese Library , D. Reidel Publishing Company, Dordrecht, 1981. · Zbl 0453.03001
[2] Ishihara, H., B. Khoussainov, and A. Nerode, ”Decidable Kripke models of intuitionistic theories”, Annals of Pure and Applied Logic , vol. 93 (1998), pp. 115–23. · Zbl 0924.03060 · doi:10.1016/S0168-0072(97)00057-2
[3] Simpson, S. G., Subsystems of Second Order Arithmetic , Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1999. · Zbl 0909.03048
[4] Troelstra, A. S., and D. van Dalen, Constructivism in Mathematics. Vol. I , vol. 121 of Studies in Logic and the Foundations of Mathematics , North-Holland Publishing Company, Amsterdam, 1988. · Zbl 0653.03040
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.