pith. sign in

arxiv: 2507.18798 · v4 · submitted 2025-07-24 · 💻 cs.LO

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

Victor Barroso-Nascimento This is my paper

Pith reviewed 2026-05-19 02:06 UTC · model grok-4.3

classification 💻 cs.LO
keywords higher-order Kripke modelsnested modelsintuitionistic modal logicfixed pointsaccessibility relationsIKMKnon-classical logics
0
0 comments X

The pith

Higher-order Kripke models nest lower-order models as worlds and use fixed points to interpret modalities for intuitionistic logics.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces higher-order Kripke models in which the worlds of an n-ary model consist only of (n-1)-ary models. Modal necessity and possibility are defined so that each depends only on the same world across accessible frames rather than on a separate evaluation. This construction is applied first to the intuitionistic modal logics IK and MK, then extended to other non-classical systems. The usual correspondence between conditions on accessibility relations and specific modal axioms remains intact. A reader would care because the approach keeps the semantics close to Kripke's original picture while handling logics that standard models interpret less directly.

Core claim

Higher-order Kripke models are defined recursively so that the set of objects in an n-ary model contains only (n-1)-ary models. Worlds function as fixed points for the modal operators, meaning that what is necessary or possible at a world in a frame is determined solely by what holds at the same world in the accessible frames. The framework therefore interprets intuitionistic modal logics IK and MK directly, and the standard link between frame conditions and modal axioms carries over without additional restrictions.

What carries the argument

Higher-order or nested Kripke models, in which worlds are lower-order models and modal operators receive fixed-point interpretations relative to the same world in accessible frames.

If this is right

  • Modal logics stronger than K are obtained by imposing requirements on the relations between frames.
  • The concept of an alternative world extends from classical models to any interpretation of the lower-order models.
  • The same construction generalizes naturally to other non-classical logics beyond IK and MK.
  • Standard soundness and completeness results for the target logics are expected to hold in the higher-order setting.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The recursive nesting could supply a uniform semantics that treats classical and intuitionistic modalities through different depths of embedding.
  • One could check whether specific frame conditions such as reflexivity produce unexpected validities when applied at higher orders.
  • Embedding ordinary models as the zero-order case suggests a route to hierarchical or self-referential modal semantics.

Load-bearing premise

The fixed-point interpretation of modalities in the nested models preserves soundness, completeness, and the standard correspondence between frame conditions and axioms without requiring additional restrictions or losing the ability to interpret the lower-order models consistently.

What would settle it

A concrete higher-order frame for IK in which the fixed-point definition of necessity fails to satisfy the distribution axiom while the accessibility relation satisfies the expected condition.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces higher-order (nested) Kripke models as a generalization of standard Kripke models for intuitionistic and non-classical modal logics. Standard models are treated as 0-ary; for n > 0, n-ary models have worlds consisting only of (n-1)-ary models. Modalities are interpreted via fixed points so that necessity and possibility at a world depend only on the same world in accessible frames. The central claim is that the standard correspondence between accessibility conditions and modal axioms carries over naturally to this setting, with focus on IK and MK (and generalization to other logics).

Significance. If the fixed-point construction is shown to preserve soundness, completeness, and the frame-axiom correspondence at every order without additional restrictions or inconsistencies, the work would provide a conceptually close extension of Kripke semantics that unifies modal interpretations across orders. This could strengthen semantic tools for non-classical modal logics by allowing higher-order nesting while retaining the original idea of alternatives.

major comments (2)
  1. [§3] §3 (Inductive definition of n-ary models and accessibility): The definition of the accessibility relation between n-ary models must explicitly ensure well-foundedness of the fixed-point evaluation for □ and ◇. Without this, the claim that the standard correspondence carries over to IK and MK risks imposing hidden frame constraints not required in the base (0-ary) case, undermining the preservation of soundness and completeness.
  2. [§5] §5 (Correspondence theorem for IK/MK): The proof that accessibility conditions correspond to axioms in the higher-order setting must verify that the nesting does not force non-standard properties on the underlying frames. The abstract's assertion that the association 'carries over naturally' is load-bearing and requires a concrete inductive argument addressing the skeptic's concern about circularity or extra restrictions.
minor comments (2)
  1. [§1] The introduction would benefit from a small concrete example contrasting a 1-ary model with a standard Kripke model to illustrate the fixed-point idea.
  2. [Throughout] Notation for 'objects' versus 'worlds' and 'frames' versus 'models' should be used consistently to avoid minor ambiguity in the higher-order case.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive report. The two major comments raise important points about rigor in the inductive definitions and proofs. We address each below and will revise the manuscript accordingly to strengthen the presentation while preserving the core technical claims.

read point-by-point responses

  1. Referee: [§3] §3 (Inductive definition of n-ary models and accessibility): The definition of the accessibility relation between n-ary models must explicitly ensure well-foundedness of the fixed-point evaluation for □ and ◇. Without this, the claim that the standard correspondence carries over to IK and MK risks imposing hidden frame constraints not required in the base (0-ary) case, undermining the preservation of soundness and completeness.

    Authors: We agree that making well-foundedness explicit would improve clarity. The inductive construction of n-ary models already proceeds by building from lower-order models, which ensures that the fixed-point equations for the modalities are well-founded by the finite nesting depth at each stage. However, to eliminate any ambiguity about potential hidden constraints, we will add an explicit clause to Definition 3.1 (or its equivalent) stating that accessibility relations are required to respect the well-founded order induced by the inductive construction. This addition does not impose new frame conditions beyond those already present in the 0-ary case; it merely renders the existing dependence on lower-order models overt. We will also include a short remark confirming that soundness and completeness proofs remain unaffected. revision: yes

  2. Referee: [§5] §5 (Correspondence theorem for IK/MK): The proof that accessibility conditions correspond to axioms in the higher-order setting must verify that the nesting does not force non-standard properties on the underlying frames. The abstract's assertion that the association 'carries over naturally' is load-bearing and requires a concrete inductive argument addressing the skeptic's concern about circularity or extra restrictions.

    Authors: The referee correctly identifies that the current argument in §5 would benefit from greater explicitness. We will expand the proof of the correspondence theorem (Theorem 5.3 and surrounding discussion) to include a full induction on the arity n. The inductive step will show that if the accessibility-axiom correspondence holds for (n-1)-ary models, then the fixed-point interpretation at level n preserves exactly the same frame conditions (reflexivity, transitivity, etc.) without introducing non-standard properties or circular dependencies. The base case (n=0) recovers the standard Kripke correspondence, and the inductive hypothesis ensures that nesting does not propagate extra restrictions. This addresses concerns about circularity directly. We will also update the abstract to reflect that the carry-over is established by this inductive argument rather than asserted as immediate. revision: yes

Circularity Check

0 steps flagged

Recursive model construction and fixed-point modal clauses are definitional extensions, not self-referential reductions.

full rationale

The paper defines 0-ary models as standard Kripke models and n-ary models inductively by letting worlds be (n-1)-ary models. Modal operators are interpreted via a fixed-point clause that evaluates necessity/possibility at w by reference to the same w in accessible frames. This is a direct generalization of the standard satisfaction clause rather than a derivation that presupposes its own conclusion. The claim that frame-axiom correspondences carry over is presented as following from the inductive construction; no equation or definition is shown to be equivalent to its target result by construction, and no load-bearing step reduces to a self-citation or fitted parameter. The derivation remains self-contained against the base Kripke semantics.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The claim rests on the background assumption that standard Kripke semantics and its correspondence theorems extend inductively to the nested case; no free parameters or new invented entities beyond the model definition itself are mentioned.

axioms (1)
  • standard math Kripke semantics and accessibility-axiom correspondence for modal logics
    The paper states that the association between conditions on accessibility relations and modal axioms carries over from the classical case.
invented entities (1)
  • n-ary Kripke models no independent evidence
    purpose: To provide a uniform semantics for nested modalities by making worlds themselves models of lower arity
    New semantic structure introduced to generalize standard Kripke models; no independent evidence outside the paper is supplied in the abstract.

pith-pipeline@v0.9.0 · 5745 in / 1430 out tokens · 37088 ms · 2026-05-19T02:06:45.339291+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

33 extracted references · 33 canonical work pages

  1. [1]

    149 (1963), pp

    Alan Anderson and Nuel Belnap, First degree entailments , Mathematische Annalen, vol. 149 (1963), pp. 302–319. 42 VICTOR BARROSO-NASCIMENTO UNIVERSITY COLLEGE LONDON

    work page 1963

  2. [2]

    Gianluigi Bellin, Valeria De Paiva,and Eike Ritter, Extended curry-howard correspondence for a basic constructive modal logic , Proceedings of methods for modalities, vol. 2, 2001

    work page 2001

  3. [3]

    43 (1984), no

    Milan Boˇzi´c and Kosta Doˇsen, Models for normal intuitionistic modal logics , Studia Logica, vol. 43 (1984), no. 3, pp. 217–245

    work page 1984

  4. [4]

    Alexander Chagrov and Michael Zakharyaschev, Modal logic, Oxford Uni- versity Press, New York, 1997

    work page 1997

  5. [5]

    Chellas, Modal logic: An introduction , Cambridge University Press, 1980

    Brian F. Chellas, Modal logic: An introduction , Cambridge University Press, 1980

    work page 1980

  6. [6]

    5 (1976), no

    Bernd Dahn, Neighbourhood semantics and generalized kripke models , Bulletin of the Section of Logic , vol. 5 (1976), no. 1, pp. 2–7

    work page 1976

  7. [7]

    Jim de Groot, Ian Shillito, and Ranald Clouston , Semantical analysis of intuitionistic modal logics between ck and ik , 2025

    work page 2025

  8. [8]

    44 (1985), no

    Kosta Doˇsen, Models for stronger normal intuitionistic modal logics , Studia Logica, vol. 44 (1985), no. 1, pp. 39–70

    work page 1985

  9. [9]

    19 (1978), no

    Gis`ele Fischer-Servi, The finite model property for MIPQ and some conse- quences., Notre Dame Journal of Formal Logic , vol. 19 (1978), no. 4, pp. 687 – 692

    work page 1978

  10. [10]

    , Axiomatizations for some intuitionistic modal logics, Rend. Sem. Mat. Univers. Politecn. Torino , vol. 42 (1984), pp. 179 – 194

    work page 1984

  11. [11]

    Zalta and Uri Nodelman, editors), Metaphysics Research Lab, Stanford Uni- versity, Spring 2024 ed., 2024

    James Garson, Modal Logic, The Stanford encyclopedia of philosophy (Ed- ward N. Zalta and Uri Nodelman, editors), Metaphysics Research Lab, Stanford Uni- versity, Spring 2024 ed., 2024

    work page 2024

  12. [12]

    40 (1975), no

    Martin Gerson , The inadequacy of the neighbourhood semantics for modal logic, The Journal of Symbolic Logic , vol. 40 (1975), no. 2, pp. 141–148

    work page 1975

  13. [13]

    Gheorghiu, Proof-theoretic semantics for first-order logic, 2024

    Alexander V. Gheorghiu, Proof-theoretic semantics for first-order logic, 2024

    work page 2024

  14. [14]

    38 (1931), no

    Kurt G¨odel, ¨Uber formal unentscheidbare s¨ atze der principia mathematica und verwandter systeme i, Monatshefte f¨ ur Mathematik und Physik, vol. 38 (1931), no. 1, pp. 173–198

    work page 1931

  15. [15]

    Zalta, editor), Metaphysics Research Lab, Stanford University, Summer 2022 ed., 2022

    Siegfried Gottwald, Many-Valued Logic, The Stanford encyclopedia of phi- losophy (Edward N. Zalta, editor), Metaphysics Research Lab, Stanford University, Summer 2022 ed., 2022

    work page 2022

  16. [16]

    42 (1982), no

    Allen Hazen, On a possible misinterpretation of kripke’s semantics for intu- itionistic logic, Analysis, vol. 42 (1982), no. 3, pp. 128–133

    work page 1982

  17. [17]

    161 (2010), no

    Danko Ilik, Gyesik Lee, and Hugo Herbelin , Kripke models for classical logic, Annals of Pure and Applied Logic , vol. 161 (2010), no. 11, pp. 1367–1378

    work page 2010

  18. [18]

    Kreisel, Mathematical significance of consistency proofs , The Journal of Symbolic Logic, vol

    G. Kreisel, Mathematical significance of consistency proofs , The Journal of Symbolic Logic, vol. 23 (1958), no. 2, pp. 155–182

    work page 1958

  19. [19]

    24 (1959), no

    Saul Kripke, A completeness theorem in modal logic, The Journal of Symbolic Logic, vol. 24 (1959), no. 1, pp. 1–14

    work page 1959

  20. [20]

    Kripke , Semantical analysis of intuitionistic logic , Formal systems and recursive functions (Michael Dummett and J

    Saul A. Kripke , Semantical analysis of intuitionistic logic , Formal systems and recursive functions (Michael Dummett and J. N. Crossley, editors), North Holland, 1963, pp. 92–130

    work page 1963

  21. [21]

    73 (2008), no

    Charles McCarty, Completeness and incompleteness for intuitionistic logic , The Journal of Symbolic Logic , vol. 73 (2008), no. 4, pp. 1315–1327

    work page 2008

  22. [22]

    85 (2007), no

    Yutaka Miyazaki, Kripke incomplete logics containing ktb, Studia Logica: An International Journal for Symbolic Logic , vol. 85 (2007), no. 3, pp. 303–317

    work page 2007

  23. [23]

    Eric Pacuit , Neighborhood semantics for modal logic , Springer, Cham, Switzerland, 2017

    work page 2017

  24. [24]

    53 (1988), no

    Gordon Plotkin and Colin Stirling , A framework for intuitionistic modal logics, The Journal of Symbolic Logic , vol. 53 (1988), no. 2, pp. 669–669. HIGHER-ORDER KRIPKE MODELS FOR INTUITIONISTIC AND NON-CLASSICAL MODAL LOGICS 43

    work page 1988

  25. [25]

    Graham Priest, An introduction to non-classical logic: From if to is , 2nd ed., Cambridge Introductions to Philosophy, Cambridge University Press, 2008

    work page 2008

  26. [26]

    1 (2008), no

    , Many-valued modal logics: A simple approach: Many-valued modal log- ics: A simple approach , Review of Symbolic Logic , vol. 1 (2008), no. 2, pp. 190–203

    work page 2008

  27. [27]

    26 (2017), no

    Greg Restall, First degree entailment, symmetry and paradox, Logic and Log- ical Philosophy , vol. 26 (2017), no. 1, pp. 3–18

    work page 2017

  28. [28]

    of the IGPL , vol

    Tor Sandqvist , Base-extension semantics for intuitionistic sentential logic , Logic J. of the IGPL , vol. 23 (2015), no. 5, pp. 719–731

    work page 2015

  29. [29]

    25 (2016), p

    Wagner Sanz, A criticism of kripke’s semantic for intuitionistic logic , O Que Nos Faz Pensar , vol. 25 (2016), p. 99

    work page 2016

  30. [30]

    36 (1977), no

    Gis`ele Fischer Servi, On modal logic with an intuitionistic base , Studia Log- ica: An International Journal for Symbolic Logic , vol. 36 (1977), no. 3, pp. 141–149

    work page 1977

  31. [31]

    Simpson, The proof theory and semantics of intuitionistic modal logic , Ph.D

    Alex K. Simpson, The proof theory and semantics of intuitionistic modal logic , Ph.D. thesis , College of Science and Engineering, School of Informatics, 1994

    work page 1994

  32. [32]

    41 (1976), no

    Wim Veldman, An intuitionistic completeness theorem for intuitionistic predi- cate logic, The Journal of Symbolic Logic , vol. 41 (1976), no. 1, pp. 159–166

    work page 1976

  33. [33]

    50 (1990), no

    Duminda Wijesekera, Constructive modal logics i , Annals of Pure and Ap- plied Logic, vol. 50 (1990), no. 3, pp. 271–301. E-mail: victorluisbn@gmail.com

    work page 1990