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

TL;DR

This paper develops higher-order Kripke models for intuitionistic and non-classical modal logics, extending traditional models to include nested worlds that are models themselves, enabling richer semantic frameworks.

Contribution

It introduces a novel hierarchy of nested Kripke models that closely align with Kripke's original ideas and generalize to non-classical modal logics.

Findings

Higher-order models generalize standard Kripke models.

Worlds as fixed points depend only on true statements within the same world.

Framework applies to intuitionistic modal logics like IK and MK.

Abstract

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.