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.

翻译：本文介绍了高阶（"嵌套"）克里普克模型，这是对克里普克模型的推广，无论在数学上还是概念上都与克里普克的原始思想高度接近。标准模型为0阶模型，而 n>0 的 n 阶模型是指其对象集（"可能世界"）仅包含 (n-1) 阶模型的模型。其核心思想在于将世界用作模态定义的固定点，即框架中某一世界中的必然性或可能性仅取决于可及框架中同一世界内的真值。本文主要处理直觉主义模态逻辑 IK 和 MK 这两个典型情况，并由此自然地推广至其他非经典逻辑。可及关系上的条件与模态公理之间的关联也在该框架中得到延续，因此可通过施加框架间关系的要求来获得比 K 更强的模态逻辑。正如克里普克模型为经典模型定义了"替代"概念，n 阶模型（n>0）也为 (n-1) 阶模型的任意解释定义了相同的概念。