Higher-order Kripke models for intuitionistic and non-classical modal logics
Victor Barroso-Nascimento
TL;DR
The paper develops higher-order Kripke semantics as a natural extension of Kripke's original idea to give modal semantics for non-classical logics, focusing on intuitionistic modal logics $IK$ and the new logic $MK$. It defines $n$-ary and infinitary higher-order Kripke models and proves mappings that translate between the new general frameworks and traditional birelational semantics, establishing equivalences of validity. It also shows that the modular semantic clauses of $MK$ extend to other logics, and it discusses partial/homogeneous variants that realize $IK$ and $MK$, respectively, while conjecturing broad completeness results for infinitary higher-order models. Overall, the work provides a conceptually faithful, Kripke-like semantics that unifies and generalizes intuitionistic modal ideas and points toward a rich, modular theory for non-classical modalities with potential wide applicability.
Abstract
This paper introduces higher-order Kripke models, a generalization of standard Kripke models that is remarkably close to Kripke's original idea - both mathematically and conceptually. Standard Kripke models are now considered $0$-ary models, whereas an $n$-ary model for $n > 0$ is a model whose set of objects (''possible worlds'') contains only $(n-1)$-ary Kripke models. Models with infinitely many layers are also considered. This framework is obtained by promoting a radical change of perspective in how modal semantics for non-classical logics are defined: just like classical modalities are obtained through use of an accessibility relation between classical propositional models, non-classical modalities are now obtained through use of an accessibility relation between non-classical propositional models (even when they are Kripke models already). The paper introduces the new models after dealing specifically with the case of intuitionistic modal logic. It is shown that, depending on which intuitionistic $0$-ary propositional models are allowed, we may obtain $1$-ary models equivalent to either birelational models for $IK$ or for a new logic called $MK$. Those $1$-ary models have an intuitive reading that adds to the interpretation of intuitionistic models in terms of ''timelines'' the concept of ''alternative timelines''. More generally, $n$-ary models (for $n > 0$) can be read as defining a concept of ''alternative'' for any interpretation of the $(n-1)$-ary models. The semantic clauses for necessity and possibility of $MK$ are modular and can be used to obtain similar modal semantics for every non-classical logic, each of which can be provided with a similar intuitive reading. After intuitionistic modal logic is dealt with, the general structure of higher-order Kripke Models and some of its variants are defined, and a series of conjectures about their properties are stated.