Back and forth between first-order Kripke models

We introduce the notion of (bounded) bisimulation for first-order Kripke models. It is defined as a relation that satisfies certain zig-zag conditions involving back-and-forth moves between nodes of Kripke models and, simultaneously, between the domains of their underlying structures. As one of our main results, we prove that if two Kripke models bisimulate to a certain degree, then they are logically equivalent with respect to the class of formulae of the appropriate complexity. Two applications of the notion introduced in the paper are given. First, we consider bisimulations in the context of Kripke models of Heyting Arithmetic. Next, we discuss the notion of (bounded) elementary submodel of a Kripke model and provide a suitable example.