pith. sign in

arxiv: 2606.07348 · v1 · pith:L5IFWOYLnew · submitted 2026-06-05 · 💻 cs.LO · math.LO

Four intuitionistic modal connectives

Philippe Balbiani , \c{C}igdem Gencer This is my paper

Pith reviewed 2026-06-27 20:16 UTC · model grok-4.3

classification 💻 cs.LO math.LO
keywords intuitionistic modal logicmodal connectivesframe definabilityaxiomatizabilitydecidabilityKripke semantics
0
0 comments X

The pith

The minimal intuitionistic modal logic determined by all frames is decidable.

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

The paper introduces four modal connectives for intuitionistic logics: a diamond and box pair following one approach and another pair following a different approach. It studies which elementary properties of frames these connectives can define. Complete axiomatizations are provided for the logics valid on specific classes of frames, and a decision procedure is established for the weakest logic valid on every possible frame.

Core claim

Using Kripke semantics on frames that combine intuitionistic forcing with modal accessibility relations, the four connectives determine logics that are completely axiomatizable on various frame classes, including the proof that the minimal logic on the class of all frames is decidable.

What carries the argument

The four intuitionistic modal connectives (two diamonds and their dual boxes) interpreted on intuitionistic frames via standard Kripke semantics.

If this is right

  • The modal definability of elementary frame classes can be analyzed using these connectives.
  • Complete axiomatizations exist for the valid formulas on those frame classes.
  • The minimal logic on all frames admits a decision procedure.
  • These connectives allow distinguishing different modal behaviors within an intuitionistic setting.

Where Pith is reading between the lines

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

  • The decidability result may enable practical implementation of theorem provers for such logics.
  • Extensions to other classes of frames could yield further decidability or complexity results.
  • Connections to standard modal logics might be explored through translations or embeddings.
  • The choice of the two different diamond interpretations allows for more expressive power in defining frame properties.

Load-bearing premise

The Kripke-style semantics on frames correctly capture both the intuitionistic and modal aspects without unintended interactions.

What would settle it

A specific formula that is valid on all frames but not derivable in the proposed axiomatization, or an undecidable set of formulas in the minimal logic.

read the original abstract

We introduce the syntax and the semantics of intuitionistic modal logics based on a diamond connective \`a la Prenosil, its dual box connective, a diamond connective \`a la Wijesekera and its dual box connective. We analyze the modal definability of some elementary classes of frames. We study the complete axiomatizability of the sets of valid formulas determined by these classes of frames. We prove the decidability of the minimal intuitionistic modal logic determined by the class of all frames.

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 introduces the syntax and Kripke-style semantics for intuitionistic modal logics using four connectives: a diamond operator à la Prenosil with its dual box, and a diamond operator à la Wijesekera with its dual box. It analyzes the modal definability of elementary classes of frames, examines the complete axiomatizability of the valid formulas determined by these frame classes, and proves the decidability of the minimal intuitionistic modal logic valid on the class of all frames.

Significance. If the results hold, the work contributes to intuitionistic modal logic by systematically comparing two families of modal operators and their duals, with results on frame definability and axiomatizability. The decidability proof for the minimal logic on all frames is a substantive contribution, as it addresses a core computational property in this setting and aligns with established Kripke semantics that extend intuitionistic logic.

minor comments (2)
  1. [Abstract] Abstract: the claim of a decidability proof would be strengthened by a one-sentence indication of the method (e.g., filtration, tableau, or reduction to known decidable logics).
  2. The paper should explicitly state whether the four connectives are interdefinable or independent in the minimal logic, as this bears on the scope of the axiomatizability results.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of the manuscript and for recommending minor revision. No specific major comments were included in the report.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper introduces four intuitionistic modal connectives with Kripke-style semantics, analyzes frame definability, proves complete axiomatizability for certain classes, and establishes decidability of the minimal logic on all frames. These are standard proof-theoretic and model-theoretic results in modal logic. No self-definitional equations, fitted parameters renamed as predictions, load-bearing self-citations, or ansatzes smuggled via prior work are present in the abstract or described claims. The derivation chain relies on independent semantic and syntactic analysis rather than reducing to its own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

Based on abstract only; the main additions are the four connectives themselves, resting on standard background assumptions from modal logic.

axioms (1)
  • standard math Kripke frame semantics for modal operators
    Invoked implicitly when defining the semantics of the four connectives on frames.
invented entities (2)
  • Diamond connective à la Prenosil and its dual box no independent evidence
    purpose: Extend intuitionistic logic with modal operators
    New syntactic and semantic elements introduced in the paper
  • Diamond connective à la Wijesekera and its dual box no independent evidence
    purpose: Extend intuitionistic logic with modal operators
    New syntactic and semantic elements introduced in the paper

pith-pipeline@v0.9.1-grok · 5597 in / 1341 out tokens · 33886 ms · 2026-06-27T20:16:05.947607+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

39 extracted references · 2 canonical work pages

  1. [1]

    Alechina, N., Mendler, M., de Paiva, V ., Ritter, E.:Categorical and Kripke seman- tics for constructiveS4modal logic.InCSL 2001.Springer (2001) 292–307

    2001

  2. [2]

    Arisaka, R., Das, A., Straßburger, L.:On nested sequents for constructive modal logics.Logical Methods in Computer Science11(2015) 1–33

    2015

  3. [3]

    Balbiani, P., Gao, H., Gencer, C ¸ ., Olivetti, N.:A natural intuitionistic modal lo- gic: axiomatization and bi-nested calculus.In32nd EACSL Annual Conference on Computer Science Logic.LIPICS (2024) 13:1–13:21

    2024

  4. [4]

    Balbiani, P., Gao, H., Gencer, C ¸ ., Olivetti, N.:Local intuitionistic modal logics and their calculi.InAutomated Reasoning.Springer (2024) 78–96. 35

    2024

  5. [5]

    Balbiani, P., Gencer, C ¸ .:Intuitionistic modal logics: a minimal setting.Studia Logica (2026) doi.org/10.1007/s11225-025-10224-7

    work page doi:10.1007/s11225-025-10224-7 2026

  6. [6]

    Balbiani, P., Tinchev, T.:Undecidable problems for modal definability.Journal of Logic and Computation27(2017) 901–920

    2017

  7. [7]

    Ballarin, R.:Modern origins of modal logic.InThe Stanford Encyclo- pedia of Philosophy (Fall 2023 Edition).Metaphysics Research Lab (2023) plato.stanford.edu/archives/fall2023/entries/logic-modal-origins/

    2023

  8. [8]

    Bierman, G., de Paiva, V .:On an intuitionistic modal logic.Studia Logica65 (2000) 383–416

    2000

  9. [9]

    Bo ˇzi´c, M., Doˇsen, K.:Models for normal intuitionistic modal logics.Studia Logica 43(1984) 217–245

    1984

  10. [10]

    Chagrov, A., Zakharyaschev, M.:Modal Logic.Oxford University Press (1997)

    1997

  11. [11]

    Dalmonte, T., Grellois, C., Olivetti, N.:Terminating calculi and countermodels for constructive modal logics.InAutomated Reasoning with Analytic Tableaux and Related Methods.Springer (2021) 391–408

    2021

  12. [12]

    Davey, B., Priestley, H.:Introduction to Lattices and Order.Cambridge Univer- sity Press (2002)

    2002

  13. [13]

    Fischer Servi, G.:Axiomatizations for some intuitionistic modal logics.Rendi- conti del Seminario Matematico Universit `a e Politecnico di Torino42(1984) 179– 194

    1984

  14. [14]

    Volume1.Elsevier (2009)

    Gabbay, D., Shehtman, V ., Skvortsov, D.:Quantification in Nonclassical Logic. Volume1.Elsevier (2009)

    2009

  15. [15]

    Ganzinger, H., Meyer, C., Veanes, M.:The two-variable guarded fragment with transitive relations.InFourteenth Annual IEEE Symposium on Logic in Computer Science.IEEE (1999) 24–34

    1999

  16. [16]

    Girlando, M., Kuznets, R., Marin, S., Morales, M., Straßburger, L.:Intuitionis- ticS4is decidable.In38th Annual ACM/IEEE Symposium on Logic in Computer Science.IEEE (2023) 10.1109/LICS56636.2023.10175684

    work page doi:10.1109/lics56636.2023.10175684 2023

  17. [17]

    Springer (2024) 47–63

    Girlando, M., Kuznets, R., Marin, S., Morales, M., Straßburger, L.:A simple loopcheck for intuitionisticK.InLogic, Language, Information, and Computation. Springer (2024) 47–63

    2024

  18. [18]

    InAdvances in Modal Logic.College Publications (2020) 269–288

    Gor ´e, R., Shillito, I.:Bi-intuitionistic logics: a new instance of an old problem. InAdvances in Modal Logic.College Publications (2020) 269–288

    2020

  19. [19]

    InAdvances in Modal Logic.CSLI Publications (1996) 85–98

    Grefe, C.:Fischer Servi’s intuitionistic modal logic has the finite model property. InAdvances in Modal Logic.CSLI Publications (1996) 85–98. 36

    1996

  20. [20]

    de Groot, J., Shillito, I., Clouston, R.:Duality for constructive modal logics: from Sahlqvist to Goldblatt-Thomason.arXiv (2026) 2601.03762

    Pith/arXiv arXiv 2026

  21. [21]

    Hasimoto, Y .:Finite model property for some intuitionistic modal logics.Bulletin of the Section of Logic30(2001) 87–97

    2001

  22. [22]

    Hodges, W.:Model Theory.Cambridge University Press (1993)

    1993

  23. [23]

    Hughes, G., Cresswell, M.:A New Introduction to Modal Logic.Routledge (1996)

    1996

  24. [24]

    Kalm ´ar, L.:Zur ¨uckf¨uhrung des Entscheidungsproblems auf den Fall von Formeln mit einer einzigen, bin¨aren, Funktionsvariablen.Compositio Mathematica4(1937) 137–144

    1937

  25. [25]

    Kripke, S.:Semantical analysis of intuitionistic logicI.In:Formal Systems and Recursive Functions.Elsevier (1965) 92–130

    1965

  26. [26]

    Logic Journal of the IGPL27(2019) 596–623

    Lin, Z., Ma, M.:Gentzen sequent calculi for some intuitionistic modal logics. Logic Journal of the IGPL27(2019) 596–623

    2019

  27. [27]

    Marin, S., Morales, M., Straßburger, L.:A fully labelled proof system for intuitio- nistic modal logics.Journal of Logic and Computation31(2021) 998–1022

    2021

  28. [28]

    Olivetti, N.:A journey in intuitionistic modal logic: normal and non-normal modalities.InLATD 2022 and MOSAIC Kick Off Conference.University of Salerno (2022) 12–13

    2022

  29. [29]

    (editors):Intuitionistic Modal Logic 2017.Journal of Applied Logics8(2021) special issue

    de Paiva, V ., Artemov, S. (editors):Intuitionistic Modal Logic 2017.Journal of Applied Logics8(2021) special issue

    2017

  30. [30]

    Plotkin, G., Stirling, C.:A framework for intuitionistic modal logics.InTheoret- ical Aspects of Reasoning About Knowledge.Morgan Kaufmann Publishers (1986) 399–406

    1986

  31. [31]

    Volume 10.College Publications (2014) 423–438

    P ˇrenosil, A.:A duality for distributive unimodal logic.InAdvances in Modal Logic. Volume 10.College Publications (2014) 423–438

    2014

  32. [32]

    Rauszer, C.:An Algebraic and Kripke-Style Approach to a Certain Extension of Intuitionistic Logic.PWN — Polish Scientific Publishers (1980)

    1980

  33. [33]

    Doctoral thesis at the University of Edinburgh (1994)

    Simpson, A.:The Proof Theory and Semantics of Intuitionistic Modal Logic. Doctoral thesis at the University of Edinburgh (1994)

    1994

  34. [34]

    Sotirov, V .:Modal theories with intuitionistic logic.InMathematical Logic.Pub- lishing House of the Bulgarian Academy of Sciences (1984) 139–171

    1984

  35. [35]

    Takano, M.:Finite model property for an intuitionistic modal logic.Nihonkai Mathematical Journal14(2003) 125–132

    2003

  36. [36]

    Wechler, W.:Universal Algebra for Computer Scientists.Springer (1992). 37

    1992

  37. [37]

    Wijesekera, D.:Constructive modal logics I.Annals of Pure and Applied Logic 50(1990) 271–301

    1990

  38. [38]

    Wolter, F.:On logics with coimplication.Journal of Philosophical Logic27 (1998) 353–387

    1998

  39. [39]

    Wolter, F., Zakharyaschev, M.:The relation between intuitionistic and classical modal logics.Algebra and Logic36(1997) 73–92. 38

    1997