Extensions of Kripke models.

There are several ways to define the notion of submodel for Kripke models of intuitionistic first-order logic. In our approach, a Kripke model A is a submodel of a Kripke model B if the frame of A is a subframe of the frame of B and for each two corresponding worlds Aa and Ba of them, Aa is a classical submodel of Ba. In this case, B is called an extension of A. We characterize formulas that are preserved under taking extensions of Kripke models. [ABSTRACT FROM AUTHOR]