Kripke Models for Intuitionistic Theories with Decidable Atomic Formulas


Zoran Marković


Some intuitionistic theories, notably Heyting's Arithmetic, have decidable atomic formulas. We show that in Kripke models of such theories, classical structures at the nodes of a Kripke model satisfy a significant fragment of corresponding theories. In particular, all consequences which are in prenex normal form hold classically.