Bisimulation reducts and submodels of intuitionistic first-order Kripke models

Abstract

We consider elementary submodels of a given intuitionistic Kripke model K meant as models that share the same theory with K and result in restricting the frame of K and/or replacing some of its worlds with their elementary substructures. We introduce the notion of bisimulation reduct of the Kripke model wich allows us to construct elementary submodels of given Kripke models in the sense of the definition above. As it was observed by A. Visser in [6], the notion of submodel can be desined for intuitionistic sirst-order Kripke models in several different ways. We can either consider models on the same frame, where the worlds of submodels are substructures of the worlds of the original model, or we can define a submodel to be the result of restricting the frame of the given model, or we can combine both of these operations. All of these possibilities were considered in the literature, see [1], [6] and [2] respectively, however it seems that we should accept the third notion as the correct one. The reason for that is, that not only such defined notion of submodel coincides with the classical notion of substructure in the case of the simplest Kripke model, but also because the well-known classical Tarski- łoś preservation theorem concerning substructures becomes a particular case of the result proven in [2]; i.e. the class of the formulas that are preserved under Kripke submodels is the class of an intuitionistic variant of universal formulas.