Higher-order Kripke models for intuitionistic and non-classical modal logics

This paper introduces higher-order (``nested") Kripke models, a generalization of Kripke models that is remarkably close to Kripke's original idea -- both mathematically and conceptually. Standard models are now $0$-ary models, whereas $n$-ary models for $n > 0$ are models whose set of objects (``possible worlds'') contain only $(n-1)$-ary models. A key idea is the use of worlds as fixed points for modal definitions, in the sense that what is necessary or possible in a world of a frame depends only on what is true in the same world on the accessible frames. This paper mainly deals with the paradigmatic cases of intuitionistic modal logics $IK$ and $MK$, from which the generalisation to other non-classical logics arises naturally. The association between conditions on accessibility relations and modal axioms also carries over to this framework, so modal logics stronger than $K$ can be obtained by imposing requirements on the relations between frames. Just like Kripke models define a concept of ``alternative'' for classical models, the $n$-ary models (for $n > 0$) defines the same concept for any interpretation of the $(n-1)$-ary models.