pith. sign in

arxiv: 2606.31879 · v1 · pith:ZMNHBVKQnew · submitted 2026-06-30 · 🧮 math.LO · cs.LO

Intuitionistic K is a Bisimulation-Invariant Fragment of Intuitionistic First-Order Logic

Jim de Groot , Jo\~ao Marcos , Rodrigo Stefanes This is my paper

Pith reviewed 2026-07-01 02:08 UTC · model grok-4.3

classification 🧮 math.LO cs.LO
keywords intuitionistic modal logicIKbisimulation invarianceintuitionistic first-order logicHennessy-Milner theoremmodel theoryLos theoremelementary embeddings
0
0 comments X

The pith

Intuitionistic modal logic IK is the bisimulation-invariant fragment of intuitionistic first-order logic.

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

The paper sets out to prove that the intuitionistic modal logic IK consists precisely of those properties expressible in intuitionistic first-order logic that remain unchanged when models are related by an IK-bisimulation. A sympathetic reader would care because this supplies a semantic test, based on model relations, for determining which first-order statements can be captured using the modal operators of IK. The work also supplies a Hennessy-Milner-style theorem that characterises IK formulas by their behaviour on bisimilar models and develops basic model theory for the intuitionistic first-order setting, including versions of Los's theorem, elementary embeddings and countable saturation.

Core claim

The authors define IK-bisimulation between the relational models of IK and prove that a sentence of intuitionistic first-order logic is equivalent to an IK formula if and only if it is invariant under all IK-bisimulations. They establish this equivalence by way of a Hennessy-Milner theorem and, as supporting results, construct intuitionistic analogues of classical model-theoretic notions such as Los's theorem, elementary embeddings and countable saturation.

What carries the argument

IK-bisimulation, a relation between relational models that preserves atomic propositions and the intuitionistic accessibility relations in both directions while respecting the modal satisfaction clauses.

If this is right

  • Any intuitionistic first-order formula preserved by IK-bisimulations can be rewritten as an equivalent IK formula.
  • IK satisfies a Hennessy-Milner property: two pointed models satisfy the same IK formulas precisely when they are IK-bisimilar.
  • Intuitionistic first-order logic admits elementary embeddings and countable saturation relative to the intuitionistic satisfaction relation.
  • An intuitionistic version of Los's theorem holds for ultraproducts of relational models.

Where Pith is reading between the lines

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

  • The same invariance technique could be applied to characterise other intuitionistic modal logics by defining appropriate bisimulations for each.
  • The developed intuitionistic model theory may transfer techniques for proving completeness or interpolation from the classical setting to the intuitionistic modal case.
  • The result suggests a route for studying expressivity questions in intuitionistic predicate logic by reduction to the simpler modal language IK.

Load-bearing premise

The relational semantics supplied for IK correctly represents the intended models against which bisimulation invariance should be measured.

What would settle it

An explicit intuitionistic first-order formula that is preserved by every IK-bisimulation yet is not equivalent to any formula of IK would refute the central claim.

read the original abstract

We define the notion of IK-bisimulation between the relational semantics for the intuitionistic modal logic IK, and prove that IK arises as the IK-bisimulation-invariant fragment of intuitionistic first-order logic. En route, we provide an intrinsic characterisation result of this logic by way of a Hennessy-Milner-style theorem and develop some intuitionistic first-order model theory, including intuitionistic analogues of Los's Theorem, elementary embeddings and countable saturation.

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

0 major / 2 minor

Summary. The paper defines IK-bisimulation between models equipped with the relational semantics for the intuitionistic modal logic IK and proves that IK coincides exactly with the IK-bisimulation-invariant fragment of intuitionistic first-order logic. It also establishes a Hennessy-Milner theorem characterizing IK and develops supporting intuitionistic first-order model theory, including analogues of Łoś's theorem, elementary embeddings, and countable saturation.

Significance. If the proofs are correct, the result supplies a van Benthem-style characterization theorem for IK, extending a classical model-theoretic insight to the intuitionistic modal setting. The accompanying development of intuitionistic model-theoretic machinery (Łoś theorem, saturation, embeddings) is a substantive contribution that may be reusable beyond the main theorem.

minor comments (2)
  1. [Abstract] The abstract states that proofs are supplied but gives no outline of the strategy; a one-sentence sketch of the main argument (e.g., how the Hennessy-Milner theorem is used to obtain the invariance direction) would improve readability without lengthening the abstract.
  2. Notation for the relational semantics (frames, valuations, accessibility) should be checked for uniform use between the definition of IK-bisimulation and the statement of the main invariance theorem.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of the paper, recognition of its significance as a van Benthem-style characterization result together with supporting model-theoretic developments, and recommendation to accept.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines IK-bisimulation directly on its relational semantics for IK and proves the van Benthem-style characterization that IK is precisely the invariant fragment of intuitionistic FOL. It supplies the supporting model theory (intuitionistic Łoś theorem, elementary embeddings, countable saturation, Hennessy-Milner theorem) internally rather than importing it via self-citation. No step reduces by construction to a fitted parameter, self-definition, or load-bearing prior result from the same authors; the derivation chain is self-contained.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the standard relational semantics of intuitionistic modal and first-order logic plus the newly introduced definition of IK-bisimulation; no free parameters or invented entities with independent evidence are visible from the abstract.

axioms (2)
  • domain assumption Intuitionistic first-order logic and IK are interpreted over relational structures
    The invariance result is stated with respect to the relational semantics mentioned in the abstract.
  • standard math Bisimulations preserve truth of modal formulas in the classical case
    The Hennessy-Milner-style theorem relies on this background fact adapted to the intuitionistic setting.

pith-pipeline@v0.9.1-grok · 5600 in / 1377 out tokens · 43431 ms · 2026-07-01T02:08:18.746549+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

32 extracted references · 20 canonical work pages

  1. [1]

    Part II: Binary bisimulation and definability

    Sergio Abriola, María Emilia Descotte & Santiago Figueira (2017): Model theory of XPath on data trees. Part II: Binary bisimulation and definability. Information and Computation 255, pp. 195–223, doi:10.1016/j.ic.2017.01.002

    work page doi:10.1016/j.ic.2017.01.002 2017

  2. [2]

    Studia Logica 104(5), pp

    Guillermo Badia (2016): Bi-simulating in bi-intuitionistic logic. Studia Logica 104(5), pp. 1037–1050, doi:10.1007/s11225-016-9664-1

    work page doi:10.1007/s11225-016-9664-1 2016

  3. [3]

    In:Methods for Modalities 2 (M4M-2), pp

    GianluigiBellin,ValeriadePaiva&EikeRitter(2001): ExtendedCurry-Howardcorrespondenceforabasic constructive modal logic. In:Methods for Modalities 2 (M4M-2), pp. 1–15

    2001

  4. [4]

    Cambridge University Press, 2001

    Patrick Blackburn, Maarten de Rijke & Yde Venema (2001):Modal Logic. Cambridge University Press, Cambridge, doi:10.1017/CBO9781107050884

    work page doi:10.1017/cbo9781107050884 2001

  5. [5]

    Journal of Applied Non-Classical Logics20(3), pp

    Balder ten Cate, Gaëlle Fontaine & Tadeusz Litak (2010):Some modal aspects of XPath. Journal of Applied Non-Classical Logics20(3), pp. 139–171, doi:10.3166/jancl.20.139-171. 482 Intuitionistic K is a Bisimulation-Invariant Fragment of Intuitionistic First-Order Logic

    work page doi:10.3166/jancl.20.139-171 2010

  6. [6]

    Chang & H

    C. Chang & H. Jerome Keisler (1973):Model Theory. Elsevier, North-Holland

    1973

  7. [7]

    de Paiva (2003): Natural deduction and context as (constructive) modality

    ValeriadePaiva(2003): Naturaldeductionandcontextas(constructive)modality .In: ProceedingsCONTEXT 2003, pp. 116–129, doi:10.1007/3-540-44958-2_10

    work page doi:10.1007/3-540-44958-2_10 2003

  8. [8]

    Annals of Pure and Applied Logic170(5), pp

    Sebastian Enqvist, Fatemeh Seifan & Yde Venema (2019):Completeness for 𝜇-calculi: a coalgebraic approach. Annals of Pure and Applied Logic170(5), pp. 578–641, doi:10.1016/j.apal.2018.12.004

    work page doi:10.1016/j.apal.2018.12.004 2019

  9. [9]

    JournalofSymbolicLogic 51(1),pp.166–179, doi:10.2307/2273953

    WilliamB.Ewald(1986): Intuitionistictenseandmodallogic . JournalofSymbolicLogic 51(1),pp.166–179, doi:10.2307/2273953

    work page doi:10.2307/2273953 1986

  10. [10]

    Part I: Bisimulation and characterization

    Diego Figueira, Santiago Figueira & Carlos Areces (2015): Model theory of XPath on data trees. Part I: Bisimulation and characterization. Journal of Artificial Intelligence Research53, pp. 271–314, doi:10.1613/jair.4658

    work page doi:10.1613/jair.4658 2015

  11. [11]

    Rendiconti del Seminario Matematico Università e Politecnico di Torino42

    Gisèle Fischer Servi (1984):Axiomatizations for some intuitionistic modal logics. Rendiconti del Seminario Matematico Università e Politecnico di Torino42

    1984

  12. [12]

    Mendelsohn (2023):First-Order Modal Logic, 2nd edition

    Melvin Fitting & Richard L. Mendelsohn (2023):First-Order Modal Logic, 2nd edition. Springer

    2023

  13. [13]

    Gabbay (1972):Model Theory for Intuitionistic Logic

    Dov M. Gabbay (1972):Model Theory for Intuitionistic Logic. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik18, pp. 49–54, doi:10.1002/malq.19720180402

    work page doi:10.1002/malq.19720180402 1972

  14. [14]

    arxiv:2512.15496

    Jim de Groot, João Marcos & Rodrigo Stefanes (2025):Intrinsic and relative characterization results for logics with negative modalities. arxiv:2512.15496

    work page arXiv 2025

  15. [15]

    In: Proceedings of the 26th WoLLIC, Springer, pp

    Jim de Groot & Dirk Pattinson (2019):Hennessy-Milner properties for (modal) bi-intuitionistic logic. In: Proceedings of the 26th WoLLIC, Springer, pp. 161–176, doi:10.1007/978-3-662-59533-6_10

    work page doi:10.1007/978-3-662-59533-6_10 2019

  16. [16]

    Master’s thesis, University of Amsterdam

    Helle Hvid Hansen (2003):Monotonic Modal Logics. Master’s thesis, University of Amsterdam

    2003

  17. [17]

    Logical Methods in Computer Science5, doi:10.2168/LMCS-5(2:2)2009

    HelleHvidHansen,ClemensKupke&EricPacuit(2009): NeighbourhoodStructures: Bisimilarityandbasic model theory. Logical Methods in Computer Science5, doi:10.2168/LMCS-5(2:2)2009

    work page doi:10.2168/lmcs-5(2:2)2009 2009

  18. [18]

    Journalof the ACM32(1), pp

    MatthewHennessy&RobinMilner(1985): Algebraiclawsfornondeterminismandconcurrency . Journalof the ACM32(1), pp. 137–161, doi:10.1145/2455.2460

    work page doi:10.1145/2455.2460 1985

  19. [19]

    In: Proceedings of the 20th MFCS, Springer, pp

    David Janin & Igor Walukiewicz (1995): Automata for the modal 𝜇-calculus and related results. In: Proceedings of the 20th MFCS, Springer, pp. 552–562

    1995

  20. [20]

    Journal of Logic and Compu- tation7(4), pp

    Natasha Kurtonina & Maarten De Rijke (1997):Simulating without negation. Journal of Logic and Compu- tation7(4), pp. 501–522, doi:10.1093/logcom/7.4.501

    work page doi:10.1093/logcom/7.4.501 1997

  21. [21]

    Marković (1979):Model Theory for Intuitionistic Logic

    Zoran M. Marković (1979):Model Theory for Intuitionistic Logic. Ph.D. thesis, University of Pennsylvania

    1979

  22. [22]

    In:Proceedings CRR 2005

    Michael Mendler & Valeria de Paiva (2005):Constructive CK for contexts. In:Proceedings CRR 2005

    2005

  23. [23]

    Springer

    Robin Milner (1980):A Calculus of Communicating Systems. Springer

    1980

  24. [24]

    The Review of Symbolic Logic6(2), pp

    GrigoryK.Olkhovikov(2013): Model-theoreticcharacterizationofintuitionisticpropositionalformulas . The Review of Symbolic Logic6(2), pp. 348–365, doi:10.1017/S1755020312000342

    work page doi:10.1017/s1755020312000342 2013

  25. [25]

    In Peter Deussen, editor: The- oretical Computer Science: Proceedings of the 5th GI-Conference, LNCS 104, Springer, pp

    David Park (1981): Concurrency and automata on infinite sequences. In Peter Deussen, editor: The- oretical Computer Science: Proceedings of the 5th GI-Conference, LNCS 104, Springer, pp. 167–183, doi:10.1007/BFb0017309

    work page doi:10.1007/bfb0017309 1981

  26. [26]

    Anna Patterson (1997):Bisimulation and propositional intuitionistic logic. In A. Mazurkiewicz & J. Win- kowski, editors:Proceedings of the 8th CONCUR, Springer, pp. 347–360, doi:10.1007/3-540-63141-0_24

    work page doi:10.1007/3-540-63141-0_24 1997

  27. [27]

    In: Proceedings of the 1st TARK, pp

    Gordon Plotkin & Colin Stirling (1986):A framework for intuitionistic modal logics (extended abstract). In: Proceedings of the 1st TARK, pp. 399–406

    1986

  28. [28]

    Simpson (1994): The Proof Theory and Semantics of Intuitionistic Modal Logic

    Alex K. Simpson (1994): The Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.D. thesis, University of Edinburgh

    1994

  29. [29]

    Johan Van Benthem (1976):Modal Correspondence Theory. Ph.D. thesis, University of Amsterdam

    1976

  30. [30]

    Wijesekera (1990): Constructive Modal Logics I

    Duminda Wijesekera (1990):Constructive Modal Logics I. Annals of Pure and Applied Logic50, pp. 271–301, doi:10.1016/0168-0072(90)90059-B. J. de Groot, J. Marcos & R. Stefanes 483

    work page doi:10.1016/0168-0072(90)90059-b 1990

  31. [31]

    Wijesekera & A

    Duminda Wijesekera & Anil Nerode (2005):Tableaux for constructive concurrent dynamic logic. Annals of Pure and Applied Logic135(1-3), pp. 1–72, doi:10.1016/j.apal.2004.12.001

    work page doi:10.1016/j.apal.2004.12.001 2005

  32. [32]

    Frank Wolter & Michael Zakharyaschev (1999):Intuitionistic modal logic. In Andrea Cantini, Ettore Casari &PierluigiMinari,editors: LogicandFoundationsofMathematics: SelectedcontributedpapersoftheTenth International Congress of Logic, Methodology and Philosophy of Science, Florence, August 1995, Springer, Dordrecht, pp. 227–238, doi:10.1007/978-94-017-2109-7_17

    work page doi:10.1007/978-94-017-2109-7_17 1999