Reverse Mathematics and Completeness Theorems for Intuitionistic Logic
Takeshi Yamazaki · Notre Dame Journal of Formal Logic · 2001
In this paper, we investigate the logical strength of completeness theorems for intuitionistic logic along the program of reverse mathematics. Among others we show that $\sf {ACA}_0$ is equivalent over $\sf {RCA}_0$ to the strong completeness theorem for intuitionistic logic: any countable theory of intuitionistic predicate logic can be characterized by a single Kripke model.