Partially-elementary extension Kripke models: A characterization and applications

A Kripke model for a first order language is called a partially-elementary extension model if its accessibility relation is not merely a (weak) submodel relation but a stronger relation of being an elementary submodel with respect to some class of formulae. As a main result of the paper, we give a characterization of partially-elementary extension Kripke models. Throughout the paper we exploit a generalized version of the hierarchy of first order formulae introduced by W. Burr. We present some applications of partially-elementary extension Kripke models to subtheories of Heyting Arithmetic and provide examples of their models and prove some of their properties. For example, we show that finite models of subtheories in question need not be normal (in the sense of S. Buss). The presented results show that the properties of models of subtheories of Heyting Arithmetic differ much from the properties of models of the full theory.