Decidable Kripke models of intuitionistic theories
Hajime Ishihara, Bakhadyr Khoussainov, Anil Nerode · Annals of Pure and Applied Logic · 1998
In this paper we introduce effectiveness into model theory of intuitionistic logic. The main result shows that any computable theory T of intuitionistic predicate logic has a Kripke model with decidable forcing such that for any sentence φ, φ is forced in the model if and only if φ is intuitionistically deducible from T.