pith. sign in

arxiv: 2606.31870 · v1 · pith:TY5TCK3Knew · submitted 2026-06-30 · 💻 cs.LO · math.LO

Intuitionistic Monotone Modal Logic: Proof Theory and Semantics

Tiziano Dalmonte , Jim de Groot This is my paper

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

classification 💻 cs.LO math.LO
keywords intuitionistic modal logicmonotone modal logicneighbourhood semanticssequent calculuscut-eliminationdecidabilityconstructive models
0
0 comments X

The pith

Intuitionistic monotone modal logic IM receives a cut-eliminating sequent calculus adapted from classical M together with a semantics based on constructive neighbourhood models.

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

The paper develops both semantics and proof theory for the intuitionistic version of monotone modal logic IM. It characterises a family of natural extensions of IM through constructive neighbourhood models. A structured sequent calculus is obtained by adapting an existing system for the classical monotone modal logic M, and this calculus is used to establish decidability of IM. The construction also exhibits a parallel between the monotone and normal modal logics when moving from the classical to the intuitionistic setting.

Core claim

The central claim is that the structured calculus originally devised for classical monotone modal logic M can be lifted to the intuitionistic setting to obtain a sound and complete, cut-eliminating system for IM and its extensions; the same system simultaneously supplies a semantic characterisation of those extensions via constructive neighbourhood models and exhibits an analogy with the corresponding intuitionistic variants of normal modal logic K.

What carries the argument

The structured sequent calculus for classical monotone modal logic M, whose rules are adjusted for the intuitionistic base logic while retaining the encoding of monotonicity.

If this is right

  • IM and its natural extensions are decidable.
  • The calculus supplies a faithful proof-theoretic counterpart to the constructive neighbourhood semantics.
  • Structural analogies appear between the monotone logics M and the normal logics K once both are placed in an intuitionistic setting.
  • IM is justified as the proper intuitionistic analogue of classical monotone modal logic M.

Where Pith is reading between the lines

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

  • The same adaptation technique could be tested on other monotone modal axioms beyond those considered here.
  • Implementation of the calculus would immediately yield a decision procedure usable for automated reasoning in constructive settings.
  • The neighbourhood semantics may support new completeness results for combinations of IM with other intuitionistic modal principles.

Load-bearing premise

The structural rules and modal rules that work for classical monotone modal logic transfer to the intuitionistic base without breaking cut-elimination or soundness with respect to the new neighbourhood semantics.

What would settle it

An explicit sequent that is derivable in the proposed calculus but fails to be valid in every constructive neighbourhood model, or a derivation in which the cut rule cannot be eliminated.

Figures

Figures reproduced from arXiv: 2606.31870 by Jim de Groot, Tiziano Dalmonte.

Figure 1
Figure 1. Figure 1: The rules of CIM [PITH_FULL_IMAGE:figures/full_fig_p008_1.png] view at source ↗
read the original abstract

We study the recently introduced intuitionistic monotone modal logic IM. We first provide a semantic characterisation for a family of natural extensions of IM in terms of constructive neighbourhood models. We then present a calculus for IM and its extensions, obtained by adapting a structured calculus for the classical monotone modal logic M. Based on the calculus, we prove some preliminary results for IM, including its decidability. Our calculus also reveals an interesting analogy between constructive and intuitionistic variants of M and the corresponding variants of K, thereby further justifying IM as a faithful intuitionistic variant of M.

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

1 major / 0 minor

Summary. The paper claims to give a semantic characterisation of a family of natural extensions of the intuitionistic monotone modal logic IM via constructive neighbourhood models, to obtain a sequent calculus for IM and its extensions by adapting a structured calculus previously developed for classical monotone modal logic M, to derive preliminary meta-theoretic results including decidability, and to exhibit an analogy between the constructive/intuitionistic variants of M and the corresponding variants of K.

Significance. If the semantic characterisation and the adapted calculus are correct, the work supplies both a model theory and a cut-free proof system for IM together with a decidability result; these are concrete contributions to the study of intuitionistic modal logics and supply evidence that IM is a faithful intuitionistic counterpart to M.

major comments (1)
  1. [calculus and meta-theory section] The central claim that the structured calculus for classical M can be directly adapted while preserving cut-elimination and soundness with respect to constructive neighbourhood models is load-bearing for the decidability result. The manuscript must therefore supply an explicit case analysis (in the section presenting the calculus and its meta-theory) showing that the intuitionistic propositional rules do not interfere with the neighbourhood conditions when the modal rules are applied; without this verification the subformula property and consequent decidability remain unconfirmed.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their thorough review and for highlighting an important point regarding the presentation of our meta-theoretic results. We respond to the major comment below.

read point-by-point responses

  1. Referee: [calculus and meta-theory section] The central claim that the structured calculus for classical M can be directly adapted while preserving cut-elimination and soundness with respect to constructive neighbourhood models is load-bearing for the decidability result. The manuscript must therefore supply an explicit case analysis (in the section presenting the calculus and its meta-theory) showing that the intuitionistic propositional rules do not interfere with the neighbourhood conditions when the modal rules are applied; without this verification the subformula property and consequent decidability remain unconfirmed.

    Authors: We agree that an explicit case analysis would strengthen the verification that the intuitionistic propositional rules do not interfere with the neighbourhood conditions. Although the cut-elimination argument proceeds by induction on cut-formula complexity and the subformula property is inherited from the standard intuitionistic rules together with the modal rules adapted from the classical setting, the current manuscript presents this only implicitly. In the revised version we will insert a dedicated paragraph (or short subsection) in the meta-theory section that enumerates the relevant cases, confirming that applications of the intuitionistic rules preserve the neighbourhood-frame conditions required for soundness and that no new principal formulas are introduced that would violate the subformula property. revision: yes

Circularity Check

0 steps flagged

No circularity: independent semantic characterisation and adaptation of classical calculus

full rationale

The paper's chain consists of (1) defining constructive neighbourhood models for extensions of IM and (2) adapting a structured sequent calculus originally developed for classical M, then proving cut-elimination, soundness, and decidability for the new system. These steps are presented as constructions with explicit proofs; no equation or result is shown to reduce by definition to its own input, no fitted parameter is relabelled as a prediction, and no load-bearing uniqueness theorem is imported solely via self-citation. The adaptation is treated as a non-trivial transfer whose preservation properties are verified rather than assumed by construction. This is the normal case of an honest non-finding.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claims rest on standard background axioms of intuitionistic propositional logic and the definition of monotone modal operators; no free parameters or invented entities are introduced in the abstract.

axioms (1)
  • standard math Standard axioms and rules of intuitionistic propositional logic
    Background framework for the intuitionistic modal extension IM.

pith-pipeline@v0.9.1-grok · 5612 in / 1085 out tokens · 40040 ms · 2026-07-01T03:03:07.454891+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

61 extracted references · 40 canonical work pages

  1. [1]

    Alechina, M

    N. Alechina, M. Mendler, V . de Paiva & E. Ritter (2001):Categorical and Kripke Semantics for Constructive S4 Modal Logic. In L. Fribourg, editor: Proceedings CSL 2001, Springer, Berlin, Heidelberg, pp. 292–307, doi:10.1007/3-540-44802-0_21

    work page doi:10.1007/3-540-44802-0_21 2001

  2. [2]

    R. Alur, T. A. Henzinger & O. Kupferman (2002): Alternating-Time Temporal Logic. Journal of the ACM 49(5), pp. 672–713, doi:10.1145/585265.585270

    work page doi:10.1145/585265.585270 2002

  3. [3]

    Arisaka, A

    R. Arisaka, A. Das & L. Strassburger (2015): On Nested Sequents for Constructive Modal Logics . Logical Methods in Computer Science 11, doi:10.2168/LMCS-11(3:7)2015

    work page doi:10.2168/lmcs-11(3:7)2015 2015

  4. [4]

    Artemov & T

    S. Artemov & T. Protopopescu (2016): Intuitionistic epistemic logic. The Review of Symbolic Logic 9(2), pp. 266––298, doi:10.1017/S1755020315000374

    work page doi:10.1017/s1755020315000374 2016

  5. [5]

    Bellin, V

    G. Bellin, V . de Paiva & E. Ritter (2001): Extended Curry-Howard correspondence for a basic constructive modal logic. In: Methods for Modalities II

    2001

  6. [6]

    Boži ´c & K

    M. Boži ´c & K. Došen (1984):Models for normal intuitionistic modal logics. Studia Logica 43, pp. 217–245, doi:10.1007/BF02429840

    work page doi:10.1007/bf02429840 1984

  7. [7]

    R. A. Bull (1965): A modal extension of intuitionist logic . Notre Dame Journal of Formal Logic 6(2), pp. 142–146, doi:10.1305/ndjfl/1093958154

    work page doi:10.1305/ndjfl/1093958154 1965

  8. [8]

    R. A. Bull (1965): Some modal calculi based on IC . In J.N. Crossley & M.A.E. Dummett, editors: For- mal Systems and Recursive Functions , Elsevier, Amsterdam, North Holland, pp. 3–7, doi:10.1016/S0049- 237X(08)71680-X

    work page doi:10.1016/s0049- 1965

  9. [9]

    R. A. Bull (1966): MIPC as the Formalisation of an Intuitionist Concept of Modality . The Journal of Sym- bolic Logic 31(4), pp. 609–616, doi:10.2307/2269696

    work page doi:10.2307/2269696 1966

  10. [10]

    B. F. Chellas (1980): Modal Logic: An Introduction. Cambridge University Press, Cambridge

    1980

  11. [11]

    Dalmonte (2022): Wijesekera-style constructive modal logics

    T. Dalmonte (2022): Wijesekera-style constructive modal logics. In D. Fernández-Duque, A. Palmigiano & S. Pinchinat, editors: Proceedings AiML 2022 , College Publications, England, pp. 281–303. Available at http://www.aiml.net/volumes/volume14/19-Dalmonte.pdf

    2022

  12. [12]

    Dalmonte (2025): Minimal modal logics, constructive modal logics and their relations

    T. Dalmonte (2025): Minimal modal logics, constructive modal logics and their relations . The Review of Symbolic Logic 18, pp. 463–504, doi:10.1017/S1755020325000097

    work page doi:10.1017/s1755020325000097 2025

  13. [13]

    Dalmonte, C

    T. Dalmonte, C. Grellois & N. Olivetti (2020): Intuitionistic Non-normal Modal Logics: A General Frame- work. Journal of Philosophical Logic 49, pp. 833–882, doi:10.1007/s10992-019-09539-3

    work page doi:10.1007/s10992-019-09539-3 2020

  14. [14]

    Dalmonte, B

    T. Dalmonte, B. Lellmann, N. Olivetti & E. Pimentel (2021):Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity . Journal of Logic and Computation 31, pp. 67–111, doi:10.1093/logcom/exaa072

    work page doi:10.1093/logcom/exaa072 2021

  15. [15]

    Davies & F

    R. Davies & F. Pfenning (1996): A modal analysis of staged computation. In: Proceedings SIGPLAN 1996, Association for Computing Machinery, New York, p. 258–270, doi:10.1145/237721.237788

    work page doi:10.1145/237721.237788 1996

  16. [16]

    Davies & F

    R. Davies & F. Pfenning (2001): A modal analysis of staged computation . Journal of the ACM 48(3), pp. 555–604, doi:10.1145/382780.382785

    work page doi:10.1145/382780.382785 2001

  17. [17]

    W. B. Ewald (1986): Intuitionistic tense and modal logic . Journal of Symbolic Logic 51(1), pp. 166–179, doi:10.2307/2273953

    work page doi:10.2307/2273953 1986

  18. [18]

    Visser (1996): Bisimulations, model descriptions and propositional quantifiers

    M. Fairtlough & M. Mendler (1997): Propositional Lax Logic. Information and Computation 137, pp. 1–33, doi:10.1006/inco.1997.2627

    work page doi:10.1006/inco.1997.2627 1997

  19. [19]

    Fischer Servi (1977): On modal logic with an intuitionistic base

    G. Fischer Servi (1977): On modal logic with an intuitionistic base . Studia Logica , pp. 141–149, doi:10.1007/BF02121259

    work page doi:10.1007/bf02121259 1977

  20. [20]

    Fischer Servi (1980): Semantics for a Class of Intuitionistic Modal Calculi

    G. Fischer Servi (1980): Semantics for a Class of Intuitionistic Modal Calculi . In D. Chiara & M. Luisa, editors: Italian Studies in the Philosophy of Science , Springer, Dordrecht, Netherlands, pp. 59–72, doi:10.1007/978-94-009-8937-5_5

    work page doi:10.1007/978-94-009-8937-5_5 1980

  21. [21]

    Frittella (2014): Monotone Modal Logic & Friends

    S. Frittella (2014): Monotone Modal Logic & Friends. Ph.D. thesis, Universite d’Aix-Marseille. T. Dalmonte & J. de Groot 297

    2014

  22. [22]

    D. M. Gabbay, A. Kurucz, F. Wolter & M. Zakharyaschev (2003):Many-Dimensional Modal Logics: Theory and Applications. Elsevier Science B.V

    2003

  23. [23]

    Garg & F

    D. Garg & F. Pfenning (2006): Non-Interference in Constructive Authorization Logic. In: Proceedings CSFW 2006, pp. 283–296, doi:10.1109/CSFW.2006.18

    work page doi:10.1109/csfw.2006.18 2006

  24. [24]

    R. I. Goldblatt (1981): Grothendieck Topology as Geometric Modality. Mathematical Logic Quarterly 27, pp. 495–529, doi:10.1002/malq.19810273104

    work page doi:10.1002/malq.19810273104 1981

  25. [25]

    R. I. Goldblatt (1987): Logics of Time and Computation. Center for the Study of Language and Information, USA

    1987

  26. [26]

    R. I. Goldblatt (1993): Mathematics of Modality. CSLI publications, Stanford, California

    1993

  27. [27]

    de Groot (2026): Intuitionistic monotone modal logic via translation

    J. de Groot (2026): Intuitionistic monotone modal logic via translation . Journal of Logic and Computation 36, pp. 1–39, doi:10.1093/logcom/exag017

    work page doi:10.1093/logcom/exag017 2026

  28. [28]

    de Groot, I

    J. de Groot, I. Shillito & R. Clouston (2025): Semantical Analysis of Intuitionistic Modal Logics between CK and IK. In: Proceedings LICS 2025, pp. 169–182, doi:10.1109/LICS65433.2025.00020

    work page doi:10.1109/lics65433.2025.00020 2025

  29. [29]

    de Groot (2022): Goldblatt-Thomason theorems for modal intuitionistic logics

    J. de Groot (2022): Goldblatt-Thomason theorems for modal intuitionistic logics . In D. Fernández-Duque, A. Palmigiano & S. Pinchinat, editors: Proceedings AiML 2022, pp. 467–490. Available at http://www. aiml.net/volumes/volume14/28-deGroot.pdf

    2022

  30. [30]

    de Groot & D

    J. de Groot & D. Pattinson (2020): Modal Intuitionistic Logics as Dialgebraic Logics. In: Proceedings LICS 2020, Association for Computing Machinery, New York, pp. 355––369, doi:10.1145/3373718.3394807

    work page doi:10.1145/3373718.3394807 2020

  31. [31]

    H. H. Hansen (2003): Monotonic modal logics . Master’s thesis, Institute for Logic, Language and Com- putation, University of Amsterdam. Available at https://eprints.illc.uva.nl/id/eprint/108/2/ PP-2003-24.text.pdf

    2003

  32. [32]

    H. H. Hansen & C. Kupke (2004): A Coalgebraic Perspective on Monotone Modal Logic. Electronic Notes in Theoretical Computer Science 106, pp. 121–143, doi:10.1016/j.entcs.2004.02.028

    work page doi:10.1016/j.entcs.2004.02.028 2004

  33. [33]

    Hirai (2010): An intuitionistic epistemic logic for sequential consistency on shared memory

    Y . Hirai (2010): An intuitionistic epistemic logic for sequential consistency on shared memory . In E. M. Clarke & A. V oronkov, editors: Proceedings LPAR 2010 , Springer, Berlin, Heidelberg, pp. 272—-289, doi:10.1007/978-3-642-17511-4_16

    work page doi:10.1007/978-3-642-17511-4_16 2010

  34. [34]

    Hudelmaier (1993): An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic

    J. Hudelmaier (1993): An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic. Journal of Logic and Computation 3(1), pp. 63–75, doi:10.1093/logcom/3.1.63

    work page doi:10.1093/logcom/3.1.63 1993

  35. [35]

    Hughes (2000): Generalising monads to arrows

    J. Hughes (2000): Generalising monads to arrows. Science of Computer Programming 37(1-3), pp. 67–111, doi:10.1016/S0167-6423(99)00023-4

    work page doi:10.1016/s0167-6423(99)00023-4 2000

  36. [36]

    Jäger & M

    G. Jäger & M. Marti (2016): Intuitionistic common knowledge or belief . Journal of Applied Logic 18, pp. 150–163, doi:10.1016/j.jal.2016.04.004

    work page doi:10.1016/j.jal.2016.04.004 2016

  37. [37]

    Lellmann & E

    B. Lellmann & E. Pimentel (2019): Modularisation of Sequent Calculi for Normal and Non-normal Modali- ties. ACM Transactions on Computational Logic 20, pp. 1–46, doi:10.1145/3288757

    work page doi:10.1145/3288757 2019

  38. [38]

    Lindley, P

    S. Lindley, P. Wadler & J. Yallop (2011): Idioms are Oblivious, Arrows are Meticulous, Mon- ads are Promiscuous . Electronic Notes in Theoretical Computer Science 229(5), pp. 97–117, doi:10.1016/j.entcs.2011.02.018

    work page doi:10.1016/j.entcs.2011.02.018 2011

  39. [39]

    Litak & A

    T. Litak & A. Visser (2018): Lewis meets Brouwer: Constructive strict implication. Indagationes Mathemat- icae 29(1), pp. 36–90, doi:10.1016/j.indag.2017.10.003

    work page doi:10.1016/j.indag.2017.10.003 2018

  40. [40]

    McCarthy (1993): Notes on Formalizing Context

    J. McCarthy (1993): Notes on Formalizing Context. In: Proceedings IJCAI 1993, pp. 555–560

    1993

  41. [41]

    McCarthy & S

    J. McCarthy & S. Buva ˇc (1994): Formalizing Context (Expanded Notes) . Available at http:// jmc.stanford.edu/articles/formalizing-context/formalizing-context.pdf. Technical Note STAN-CS-TN-94-13, Stanford University

    1994

  42. [42]

    Mendler & V

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

    2005

  43. [43]

    ACM Transactions on Computational Logic 9(3), pp

    Aleksandar Nanevski, Frank Pfenning & Brigitte Pientka (2008): Contextual modal type theory . ACM Transactions on Computational Logic 9(3), pp. 1–49. 298 Intuitionistic Monotone Modal Logic: Proof Theory and Semantics

    2008

  44. [44]

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

    V . de Paiva (2003): Natural deduction and context as (constructive) modality . In: Proceedings CONTEXT 2003, pp. 116–129, doi:10.1007/3-540-44958-2_10

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

  45. [45]

    Foundations of Computation Theory

    R. Parikh (1985): The Logic of Games and Its Applications. In: Selected Papers of the International Confer- ence on “Foundations of Computation Theory” on Topics in the Theory of Computation, Elsevier, USA, pp. 111—-139

    1985

  46. [46]

    Pauly (2001): Logic for Social Software

    M. Pauly (2001): Logic for Social Software. Ph.D. thesis, University of Amsterdam

    2001

  47. [47]

    Pauly (2002): A modal logic for coalitional power in games

    M. Pauly (2002): A modal logic for coalitional power in games . Journal of Logic and Computation 12, pp. 149––166, doi:10.1093/logcom/12.1.149

    work page doi:10.1093/logcom/12.1.149 2002

  48. [48]

    A. M. Pitts (1991): Evaluation logic. In G. Birtwistle, editor: Proceedings of the IVth Higher Order Work- shop 1990, Springer, Berlin, Heidelberg, pp. 162–189

    1991

  49. [49]

    Plotkin & C

    G. Plotkin & C. Stirling (1986): A Framework for Intuitionistic Modal Logics: Extended Abstract . In: Proceedings TARK 1986, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, pp. 399–406

    1986

  50. [50]

    Proietti (2012): Intuitionistic Epistemic Logic, Kripke Models and Fitch’s Paradox

    C. Proietti (2012): Intuitionistic Epistemic Logic, Kripke Models and Fitch’s Paradox. Journal of Philosoph- ical Logic 41(5), pp. 877–900, doi:10.1007/s10992-011-9207-1

    work page doi:10.1007/s10992-011-9207-1 2012

  51. [51]

    Santocanale & Y

    L. Santocanale & Y . Venema (2010): Uniform Interpolation for Monotone Modal Logic . In L. D. Beklem- ishev, V . Goranko & V . B. Shehtman, editors:Proceedings AIML 2010, College Publications, England, pp. 350–370. Available at http://www.aiml.net/volumes/volume8/Santocanale-Venema.pdf

    2010

  52. [52]

    A. K. Simpson (1994): The Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.D. thesis, Univer- sity of Edinburgh

    1994

  53. [53]

    Sotirov (1984): Modal theories with intuitionistic logic

    V . Sotirov (1984): Modal theories with intuitionistic logic. In: Mathematical Logic, Proceedings of the Con- ference on Mathematical Logic Dedicated to the Memory of A. A. Markov (1903–1979), Sofia, September 22–23, 1980, pp. 139–171

    1984

  54. [54]

    Straßburger (2013): Cut Elimination in Nested Sequents for Intuitionistic Modal Logics

    L. Straßburger (2013): Cut Elimination in Nested Sequents for Intuitionistic Modal Logics . In F. Pfenning, editor: Proceedings FOSSACS 2013 , Springer, Berlin, Heidelberg, pp. 209–224, doi:10.1007/978-3-642- 37075-5_14

    work page doi:10.1007/978-3-642- 2013

  55. [55]

    A. A. Tabatabai, R. Iemhoff & R. Jalali (2022): Uniform Lyndon interpolation for in- tuitionistic monotone modal logic . Available at http://www.aiml.net/volumes/volume14/ 09-AkbarTabatabai-Iemhoff-Jalali.pdf

    2022

  56. [56]

    A. S. Troelstra & H. Schwichtenberg (2000): Basic proof theory , 2 edition. Cambridge University Press, Cambridge, doi:10.1017/CBO9781139168717

    work page doi:10.1017/cbo9781139168717 2000

  57. [57]

    Wansing (1994): Sequent Calculi for Normal Modal Propositional Logics

    H. Wansing (1994): Sequent Calculi for Normal Modal Propositional Logics. Journal of Logic and Compu- tation 4, pp. 125–142, doi:10.1093/logcom/4.2.125

    work page doi:10.1093/logcom/4.2.125 1994

  58. [58]

    Wijesekera (1990): Constructive Modal Logics I

    D. Wijesekera (1990): Constructive Modal Logics I . Annals of Pure and Applied Logic 50, pp. 271–301, doi:10.1016/0168-0072(90)90059-B

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

  59. [59]

    Wijesekera & A

    D. Wijesekera & A. Nerode (2005): Tableaux for constructive concurrent dynamic logic. Annals of Pure and Applied Logic 135, pp. 1–72, doi:10.1016/j.apal.2004.12.001

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

  60. [60]

    Williamson (1992): On intuitionistic modal epistemic logic

    T. Williamson (1992): On intuitionistic modal epistemic logic . Journal of Philosophy 21(1), pp. 63–89. Available at https://www.jstor.org/stable/30226465

    work page arXiv 1992

  61. [61]

    Wolter & M

    F. Wolter & M. Zakharyaschev (1999): Intuitionistic Modal Logic . In A. Cantini, E. Casari & P. Minari, editors: Logic and Foundations of Mathematics: Selected Contributed Papers of the Tenth International Congress of Logic, Methodology and Philosophy of Science , Springer, Dordrecht, Netherlands, pp. 227– 238, doi:10.1007/978-94-017-2109-7_17

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