Reverse mathematics and completeness theorems for intuitionistic logic (Q1422103)

This article investigates the mathematical logic of intuitionistic propositional and predicate calculi using the framework of reverse mathematics [\textit{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 \S{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)].