2025/07/24 by Victor Barroso-Nascimento, Barroso-Nascimento, Victor
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Multi-Agent Systems and Negotiation
paper · pdf · doi:10.48550/arxiv.2507.18798
openalex publication_date 2025/07/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01
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.