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

Fuente: arXiv
Guardado en:
Detalles Bibliográficos
Autor principal: Barroso-Nascimento, Victor
Formato: Preprint
Publicado: 2025
Materias:
Acceso en línea:
Etiquetas: Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
_version_ 1866913092487610368
author Barroso-Nascimento, Victor
author_facet Barroso-Nascimento, Victor
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2507_18798
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Higher-order Kripke models for intuitionistic and non-classical modal logics
Barroso-Nascimento, Victor
Logic in Computer Science
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.
title Higher-order Kripke models for intuitionistic and non-classical modal logics
topic Logic in Computer Science
url https://arxiv.org/abs/2507.18798