Diamond-free parts of intuitionistic modal logics

A post by Anupam and Sonia in 2022 ignited a surge of interest from the modal logic and proof theory communities: until then, it was commonly believed that different inuitionistic versions of modal logic $K$ agreed on their $\Diamond$ -free parts, but this turns out to be false. After 23 comments, 3 papers, 1 further blog post, and 1 hunt for an elusive PhD thesis, we can now finally provide a classification of $\Diamond$ -free parts.

An axiomatic playground

The best starting point is to read the previous post of Anupam and Sonia, but let us do a minimal recap. We consider extensions of intuitionistic logic $\mathit{IPL}$ by the necessitation rule $\dfrac A {\Box A}$ and some of the following axioms:

$\Box (A \to B) \to \Box A \to \Box B$
$\Box (A \to B) \to \Diamond A \to \Diamond B$
$\Diamond \bot \to \bot$
$\Diamond (A\vee B) \to \Diamond A \vee \Diamond B$
$(\Diamond A \to \Box B) \to \Box (A\to B)$

Definition 1. The logic $\mathit{CK}$ is given by axioms 1 and 2, and $\mathit{IK}$ is given by all the axioms 1-5.

Anupam and Sonia noticed that, contrary to popular belief, $\mathit{IK}$ proves more $\Diamond$ -free theorems than $\mathit{CK}$ , for instance $\neg \neg \Box \bot \to \Box \bot$ and $\neg \neg \Box p \to \Box \neg \neg p$ . More generally $\mathit{IK}$ validates the Goedel-Gentzen negative translation, in hindsight an expected property given its characterisation by an intuitionistic reading of the standard translation [1]. Among other things, this raised the obvious question:

Question 2. How do the logics between $\mathit{CK}$ and $\mathit{IK}$ , by the axioms 3-5, relate on their $\Diamond$ -free parts?

Three years later

Quite a lot has happened since that original post. Here is a short history:

A fascinating discussion in the commentary section of Anupam and Sonia’s post, with numerous conjectures attempting to make sense of the situation. In particular, it turns out that Carsten Grefe already had separations between $\mathit{CK}$ and $\mathit{IK}$ in the ’90s [2].
A paper by Anupam and Sonia [3] based on the post, furthermore providing a proof theory for the logic $\mathit{CK} + \{3,4\}$ . A consequence is that this logic is $\Diamond$ -free conservative over $\mathit{CK}$ .
A blog post by Timo Lang, who recovers the same result on $\Diamond$ -free conservativity of $\mathit{CK} + \{3,4\}$ over $\mathit{CK}$ by means of a remarkably simple interpretation: set $\Diamond A := \bot$ !
A paper by Jim de Groot, Ian Shillito and Ranald Clouston [4] providing modular birelational semantics for all extensions of $\mathit{CK}$ by axioms among $\{3,4,5\}$ . Along the way they showed that the logic $\mathit{CK} + \{4,5\}$ is $\Diamond$ -free conservative over $\mathit{CK}$ , among other results.
Anupam noticed in response to Timo’s post that the result for $\mathit{CK} + \{4,5\}$ can be obtained by another simple interpretation: set $\Diamond A := \top$ !
Besides all this a renewed interest in both syntactically and semantically motivated fragments and extensions of $\mathit{IK}$ in the years since, e.g. [5] [6] [7] [8] [9] [10] [11].

The astute reader will have noticed that almost every case of our initial question is now settled… except for $\mathit{IK}^N := \mathit{CK} + \{3,5\}$ . Unlike the other results, namely $\mathit{CK} + \{3,4\}$ and $\mathit{CK} +\{4,5\}$ , which were eventually simplified by interpretations, it is not at all clear if the analysis of this logic can be carried out at an axiomatic level. This brings us to the principal (and novel!) result of this post:

Theorem 3. The logic $\mathit{IK}^N = \mathit{CK} + \{3,5\}$ has $\Diamond$ -free part strictly between $\mathit{CK}$ and $\mathit{IK}$ .

The fact that $\mathit{IK}^N$ is strictly above $\mathit{CK}$ actually follows from validation of the Goedel-Gentzen translation: the axiom 4 is not required for that [3]. So in particular $\mathit{IK}^N$ has theorems $\lnot \lnot \Box \bot \to \Box \bot$ and $\lnot \lnot \Box p \to \Box \lnot \lnot p$ , which are not theorems of $\mathit{CK}$ . But how do we go about finding a separation between $\mathit{IK}^N$ and $\mathit{IK}$ ?

Fake diamonds

The most obvious place to look is the missing axiom, $4 : \Diamond (A\lor B ) \to \Diamond A \lor \Diamond B$ . As usual in intuitionistic logic, positives imply their negative encoding:

Lemma 4. $\mathit{CK} + 3 \vdash \Diamond A \to \neg \Box \neg A$ .

Proof. We reason in $\mathit{IK}^N$ :

$\begin{array}{lll}1. & \neg A\to A \to \bot & \text{by $\mathit{IPL}$} \\2. & \Box (\neg A \to A \to \bot) & \text{by necessitation} \\3. & \Box \neg A \to \Box (A \to \bot) & \text{by axiom $1$} \\4. & \Box \neg A \to \Diamond A \to \Diamond \bot & \text{by axiom $2$}\\5. & \Box \neg A \to \Diamond A \to \bot & \text{by axiom $3$} \\6. & \Diamond A \to \neg \Box \neg A & \text{by \mathit{IPL}}\end{array}$

Show proof.

Hide proof.

So the $\Diamond$ s on the RHS of $4$ may be replaced by $\Diamond^N := \lnot \Box \lnot$ . Now, if we replace the $\Diamond$ on the LHS by a $\Box$ we almost have a candidate separation. The only issue, of course, is that $\Box(A\lor B) \to \Diamond^N A \lor \Diamond^N B$ is not even classically true! This is because there may not be a world to go to at all. What we need here is a way to insist that there is such a world. What we need is $\Diamond \top$ … only without using $\Diamond$ . Fortunately there is a folklore trick for doing just that:

Proposition 5. $(A \to \Box p) \to \Box p$ is equiprovable with $\Diamond\top \to A$ in $\mathit{IK}$ , and with $A$ in $\mathit{CK}$ .

Proof sketch. $A \to (A\to \Box p) \to \Box p$ is already (an instance) of an $\mathit{IPL}$ theorem. In $\mathit{CK} + 5$ we have:

$\begin{array}{ll}(\top \to p) \to p & \text{by $\mathit{IPL}$} \\\Box ((\top \to p) \to p) & \text{by necessitation} \\\Box(\top \to p) \to \Box p & \text{by axiom $1$} \\(\Diamond \top \to \Box p) \to \Box p & \text{by axiom $5$} \\(\Diamond \top \to A) \to (A \to \Box p) \to \Box p & \text{by $\mathit{IPL}$}\end{array}$

In the other direction, we can exploit the fact that both $\mathit{CK}$ and $\mathit{IK}$ enjoy cut-free proof systems, so we can proceed by analysis of bottom-up cut-free proof search from $(A\to \Box p) \to \Box p$ .

Show proof sketch.

Hide proof sketch.

This trick is reminiscent of the Friedman-Dragalin translation, or of second-order encodings of the positives, only with a modal sensitivity. Indeed we use this idea to construct our separating $\Diamond$ -free formula:

$4' \quad := \qquad ((\Box (A \lor B) \to \Diamond^N A \lor \Diamond^N B) \to \Box p) \to \Box p$

Provability of this formula in $\mathit{IK}$ is routine, by now a variety of syntactic and semantic methods [12] [1] [13] [14]. For completeness, here is an axiomatic proof:

Proposition 6. $\mathit{IK} \vdash 4'$ .

Proof. First let us establish in $\mathit{IK}$ indeed that $\Diamond \top$ suffices to prove $\Box (A\lor B) \to \Diamond^N A \lor \Diamond^N B$ :

$\begin{array}{ll}(A\lor B) \to \top \to A\lor B & \text{by $\mathit{IPL}$} \\\Box ((A\lor B) \to \top \to A\lor B) & \text{by necessitation} \\\Box (A\lor B) \to \Box (\top \to A\lor B) & \text{by axiom $1$} \\\Box (A\lor B) \to \Diamond \top \to \Diamond (A \lor B) & \text{by axiom $2$} \\\Box (A \lor B) \to \Diamond \top \to \Diamond A \lor \Diamond B & \text{by axiom $4$} \\\Box (A \lor B) \to \Diamond \top \to \Diamond^N A \lor \Diamond^N B & \text{by Lemma 4} \\\Diamond \top \to \Box (A\lor B) \to \Diamond^N A \lor \Diamond^N B & \text{by \mathit{IPL}} \\((\Box (A\lor B) \to \Diamond^N A \lor \Diamond^N B) \to \Box p) \to \Box p & \text{by proof of Proposition 5}\end{array}$

Note the crucial use of axiom $4$ above, rendering the proof outside $\mathit{IK}^N$ .

Show proof.

Hide proof.

For non-provability in $\mathit{IK}^N$ , it would be ideal if we could establish a similar result to Lemma 4, but for $\mathit{IK}^N$ , which would ultimately lead to purely a proof theoretic separation. There is one problem, however: we do not (yet) have a cut-free system for $\mathit{IK}^N$ , so it is not clear how to establish such a result. Of course, if we just want to establish a non-provability result, there is a more principled way of doing that, namely via model theory. Again, unfortunately, we do not have a developed model theory of $\mathit{IK}^N$ . Or, at least, we didn’t, until 2024…

Enter semantics

There are various birelational semantics for $\mathit{CK}$ [15] [16] [17]. Let us work with models of the form $(X, \leq, R, V)$ consisting of a set $X$ of worlds, a preorder $\leq$ on $X$ , a binary accessibility relation $R$ on $X$ , and a valuation $V$ that assigns to each proposition letter an upset $V(p)$ of $(X, \leq)$ . We may interpret formulas at worlds recursively by:

Propositional letters and connectives are interpreted as usual for Kripke semantics, wrt. $(X,\leq, V)$ .
$x \vDash \Box\phi$ if $\forall y \geq x \, \forall z \, (yRz \implies z \vDash \phi)$ .
$x \vDash \Diamond\phi$ if $\forall y \geq x\, \exists z \, (y R z \ \&\ z \vDash \phi)$ .

Two of the authors of this post, together with Ranald Clouston, developed a comprehensive set of frame correspondences for logics between $\mathit{CK}$ and $\mathit{IK}$ in [4]. They proposed one particularly gnarly condition:

Definition 7. Call $(X,\leq, R)$ special if, for all worlds $x, y, z$ s.t. $x R y \leq z$ there is a world $w$ s.t.:
$x \leq w R z$ ; and,
if $w \leq v$ then there is a world $u$ with $vR u \geq z$

By the results of De Groot, Shillito and Clouston we have:

Theorem 8 ([4]). $\mathit{IK}^N$ is sound and (strongly) complete for the class of special models.

This is exactly what we are after! We could now try to show that $\mathit{IK}^N \nvdash 4'$ by finding a countermodel! Unforunately it is quite difficult to wield the special condidition, not least because of its logical complexity: it is a $\Pi_4$ statement, while most other conditions ‘in the wild’ are $\Pi_2$ . It might take a long time to find such a model…

All a Vampire has is time

In the last 30 years, first-order theorem proving has advanced at an extraordinary pace, transforming from experimental academic prototypes into highly optimized, world-class reasoning engines. Modern provers like Vampire, E, SPASS, and Prover9 can handle problems of a scale and complexity that would have been unthinkable just a few decades ago, combining sophisticated strategies, equality reasoning, and clever heuristics with blazing efficiency. They can solve thousands of benchmark problems in seconds, integrate seamlessly with SAT/SMT solvers, and even collaborate with interactive proof assistants to tackle deep mathematical theorems and industrial-scale verification tasks. The fact that fully automated systems can now prove results that once demanded immense human ingenuity is a remarkable testament to both the theoretical breakthroughs and the engineering brilliance of the field.ChatGPT on recent advances in automated theorem proving, (paraphrased and formatted), 30/09/2025.

Well said. And our esteemed colleague makes a good point. Not only is the property of being special first-order definable, so is the evaluation of a fixed modal formula in a model. So why not use an automated theorem prover (ATP) to help us? Indeed, one important point that our colleague misses is the sheer accessibility of theorem provers these days. In particular Geoff Sutcliffe‘s online TPTP world includes a portfolio of web-based tools to help specify, solve, and analyse problems in first-order logic. After just a few hours in this world (mostly learning the syntax), we had a working specification. It took Vampire 4.9’s finite model finder just 0.014s to successfully output the following model:

Here the dotted edges are oriented upwards and the preorder is given by their reflexive transitive closure. The solid arrows denote the accessibility relation $R$ . Let us call this model $\Psi$ .

Proposition 9. $\Psi$ is special, and does not satisfy 4′.

Together with Proposition 6, this completes the proof of our main Theorem 3, under completeness, Theorem 7. In fact the model above is the minimal such model, in the following sense:

there is no countermodel with fewer than 4 worlds;
among countermodels with 4 worlds, no countermodel has fewer than 4 $R$ -edges.

Both of these are established, once again, by Vampire [18] [19], this time finding appropriate refutations.

A more helpful model

$\Psi$ is far from an intuitive model. Even if a human might have found it with enough brute force work, the parallelisation of $R$ and $\leq$ edges is arguably not natural in the semantics of intuitionistic modal logic. Furthermore it is perhaps not ‘obvious’ why this model is special, formally speaking. A human would arguably seek to resolve the special condition in a more disciplined way. For what it is worth, let us give another model, this time found (independently) by honest human toil:

Again dotted edges are oriented upwards and the preorder is given by their reflexive transitive closure. Solid arrows, like before, denote the accessibility relation $R$ . Let us call this model $\Theta$ .

Proposition 10. $\Theta$ is special, and does not satisfy $4'$ .

Baby, let’s Rocq

In the last 40 years, interactive theorem proving has undergone extraordinary advances, transforming from niche academic tools into powerful, user-friendly systems that support the formal verification of highly complex mathematics and software. Proof assistants like Coq, Isabelle, Lean, and HOL have not only scaled to industrial applications—verifying compilers, operating systems, and cryptographic protocols—but have also enabled the formalization of deep mathematical results, such as the Odd Order Theorem and even parts of the Liquid Tensor Experiment. These developments demonstrate a remarkable synergy between automation, human-guided proof construction, and growing proof libraries, making interactive theorem proving a cornerstone of modern formal methods and a shining example of how logic and computation can push the boundaries of what is provably correct.
ChatGPT on recent advances in interactive theorem proving, (paraphrased and formatted), 01/10/2025.

We used quite a bit of heavy machinery here. Our birelational semantics were quite funky and, as we remarked, the ‘special’ frame condition is unusually complex, so in practice cumbersome to check. Even then one must verify the countermodels by hand or, in the case of Vampire, make sure human error has not creeped into the specification. Fortunately, however, in [4] De Groot, Shillito and Clouston went above and beyond the norms of the area: they fully mechanised their results in the Rocq proof assistant (previously Coq). This includes formalised soundness and completeness results for all the logics between $\mathit{CK}$ and $\mathit{IK}$ , in particular including Theorem 8 above, the adequacy of special frames for $\mathit{IK}^N$ .

Building on this work we have formalised the main result of this post, Theorem 3. We exploited the mechanisation of the Kripke semantics to implement the second ‘human’ countermodel, and proved that it satisfies all the required conditions. To bring as much automation as possible in the case analysis, we implemented our models using booleans: points in the models are tuples of booleans, and relations are ultimately defined on equality between booleans, a breeze for Rocq. For what it is worth, we also mechanised the axiomatic $\mathit{IK}$ proof of $4'$ too. The previous formalisation of axiomatic reasoning tactics, in particular the deduction theorem, greatly facilitated this effort. Both the provability and non-provability result are established within the same project as the aforementioned soundness and completeness results of [4], ensuring the same definitions are used throughout.

Conclusions

We have now classified the $\Diamond$ -free parts of all intuitionistic modal logics between $\mathit{CK}$ and $\mathit{IK}$ by axioms among 3,4,5. Here is the classification, with red lines separating logics with distinct $\Diamond$ -free parts:

The positioning of $\mathit{IK}^N = \mathit{CK} + \{3,5\}$ , in the central band between the two red lines, is the main result of the post, Theorem 3 (all the others were previously known).

While this line of work might seem rather a curiosity, what is notable is the genuinely insightful research that has emerged from these questions. In just a few years we have considerably deepened our understanding of the proof theory and model theory of intuitionistic modal logics. Sometimes it is worth simply chasing curiosities, for the fruit along the way.

References

[1] A. Simpson, “The Proof Theory and Semantics of Intuitionistic Modal Logic,” PhD Thesis, 1994.
[Bibtex]

@PhdThesis{simpson:phd94,
author = "Alex Simpson",
title = "The Proof Theory and Semantics of Intuitionistic Modal Logic",
year = "1994",
school = "University of Edinburgh",
}

[2] C. Grefe, “Fischer Servi’s Intuitionistic Modal Logic and Its Extensions,” PhD Thesis, 1999.
[Bibtex]

@phdthesis{GrefeThesis,
title={Fischer Servi's Intuitionistic Modal Logic and Its Extensions},
author={Grefe, C.},
isbn={9783928973670},
series={Forschen und Wissen - Mathematik},
url={https://books.google.co.uk/books?id=cauEAAAACAAJ},
year={1999},
school={University of Berlin},
}

[3]

A. Das and S. Marin, “On Intuitionistic Diamonds (and Lack Thereof),” in Automated Reasoning with Analytic Tableaux and Related Methods – 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings, 2023, p. 283–301.
[Bibtex]

@inproceedings{DasMarin23:int-diamonds,
author = {Anupam Das and
Sonia Marin},
editor = {Revantha Ramanayake and
Josef Urban},
title = {On Intuitionistic Diamonds (and Lack Thereof)},
booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 32nd
International Conference, {TABLEAUX} 2023, Prague, Czech Republic,
September 18-21, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14278},
pages = {283--301},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-43513-3\_16},
doi = {10.1007/978-3-031-43513-3\_16},
timestamp = {Wed, 01 Nov 2023 08:59:02 +0100},
biburl = {https://dblp.org/rec/conf/tableaux/DasM23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

[4]

J. de Groot, I. Shillito, and R. Clouston, “Semantical Analysis of Intuitionistic Modal Logics between CK and IK,” CoRR, vol. abs/2408.00262, 2024.
[Bibtex]

@article{deGrootShillitoClouston24:iml-semantics,
author = {Jim de Groot and
Ian Shillito and
Ranald Clouston},
title = {Semantical Analysis of Intuitionistic Modal Logics between {CK} and
{IK}},
journal = {CoRR},
volume = {abs/2408.00262},
year = {2024},
url = {https://doi.org/10.48550/arXiv.2408.00262},
doi = {10.48550/ARXIV.2408.00262},
eprinttype = {arXiv},
eprint = {2408.00262},
timestamp = {Fri, 06 Sep 2024 21:01:55 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2408-00262.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

[5]

M. Biernacka, D. Biernacki, S. Lenglet, and A. Schmitt, “Optimizing a Non-Deterministic Abstract Machine with Environments.” 2024.
[Bibtex]

@inproceedings{Kavvos24,
doi = {10.4230/LIPICS.FSCD.2024.11},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.11},
author = {Biernacka, Małgorzata and Biernacki, Dariusz and Lenglet, Sergueï and Schmitt, Alan},
keywords = {Abstract machine, Explicit substitutions, Refocusing, Theory of computation → Abstract machines},
language = {en},
title = {Optimizing a Non-Deterministic Abstract Machine with Environments},
publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
year = {2024},
copyright = {Creative Commons Attribution 4.0 International license}
}

[6]

P. Balbiani, H. Gao, Ç. Gencer, and N. Olivetti, “Local Intuitionistic Modal Logics and Their Calculi,” in Automated Reasoning – 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II, 2024, p. 78–96.
[Bibtex]

@inproceedings{BalGaoGenOli24:loc-iml,
author = {Philippe Balbiani and
Han Gao and
{\c{C}}igdem Gencer and
Nicola Olivetti},
editor = {Christoph Benzm{\"{u}}ller and
Marijn J. H. Heule and
Renate A. Schmidt},
title = {Local Intuitionistic Modal Logics and Their Calculi},
booktitle = {Automated Reasoning - 12th International Joint Conference, {IJCAR}
2024, Nancy, France, July 3-6, 2024, Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
volume = {14740},
pages = {78--96},
publisher = {Springer},
year = {2024},
url = {https://doi.org/10.1007/978-3-031-63501-4\_5},
doi = {10.1007/978-3-031-63501-4\_5},
timestamp = {Thu, 22 Aug 2024 20:23:12 +0200},
biburl = {https://dblp.org/rec/conf/ijcar/BalbianiGGO24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

[7]

P. Balbiani, H. Gao, Ç. Gencer, and N. Olivetti, “A Natural Intuitionistic Modal Logic: Axiomatization and Bi-Nested Calculus,” in 32nd EACSL Annual Conference on Computer Science Logic, CSL 2024, February 19-23, 2024, Naples, Italy, 2024, p. 13:1–13:21.
[Bibtex]

@inproceedings{BalGaoGenOli24:nat-iml,
author = {Philippe Balbiani and
Han Gao and
{\c{C}}igdem Gencer and
Nicola Olivetti},
editor = {Aniello Murano and
Alexandra Silva},
title = {A Natural Intuitionistic Modal Logic: Axiomatization and Bi-Nested
Calculus},
booktitle = {32nd {EACSL} Annual Conference on Computer Science Logic, {CSL} 2024,
February 19-23, 2024, Naples, Italy},
series = {LIPIcs},
volume = {288},
pages = {13:1--13:21},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2024},
url = {https://doi.org/10.4230/LIPIcs.CSL.2024.13},
doi = {10.4230/LIPICS.CSL.2024.13},
timestamp = {Sun, 06 Oct 2024 20:59:03 +0200},
biburl = {https://dblp.org/rec/conf/csl/BalbianiGGO24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

[8] J. de Groot, Intuitionistic monotone modal logic via translation, 2025.
[Bibtex]

@misc{deGroot25:mon-iml,
title={Intuitionistic monotone modal logic via translation},
author={Jim de Groot},
year={2025},
eprint={2507.13746},
archivePrefix={arXiv},
primaryClass={math.LO},
url={https://arxiv.org/abs/2507.13746},
}

[9]

H. Gao and N. Olivetti, “Constructive Modal Logics: Bi-nested Calculi and Bi-relational Countermodels,” in Logic, Language, Information, and Computation – 31st International Workshop, WoLLIC 2025, Porto, Portugal, July 14-17, 2025, Proceedings, 2025, p. 211–227.
[Bibtex]

@inproceedings{GaoOli25:cml,
author = {Han Gao and
Nicola Olivetti},
editor = {Dexter Kozen and
Ruy J. G. B. de Queiroz},
title = {Constructive Modal Logics: Bi-nested Calculi and Bi-relational Countermodels},
booktitle = {Logic, Language, Information, and Computation - 31st International
Workshop, WoLLIC 2025, Porto, Portugal, July 14-17, 2025, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {15942},
pages = {211--227},
publisher = {Springer},
year = {2025},
url = {https://doi.org/10.1007/978-3-031-99536-1\_13},
doi = {10.1007/978-3-031-99536-1\_13},
timestamp = {Thu, 11 Sep 2025 20:25:44 +0200},
biburl = {https://dblp.org/rec/conf/wollic/GaoO25.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

[10] P. Balbiani and Ç. Gencer, Intuitionistic modal logics: a minimal setting, 2025.
[Bibtex]

@misc{BalGen25:iml-min,
title={Intuitionistic modal logics: a minimal setting},
author={Philippe Balbiani and Çigdem Gencer},
year={2025},
eprint={2502.19060},
archivePrefix={arXiv},
primaryClass={math.LO},
url={https://arxiv.org/abs/2502.19060},
}

[11] L. Pacheco, Collapsing Constructive and Intuitionistic Modal Logics, 2024.
[Bibtex]

@misc{Pacheco24:ckb,
title={Collapsing Constructive and Intuitionistic Modal Logics},
author={Leonardo Pacheco},
year={2024},
eprint={2408.16428},
archivePrefix={arXiv},
primaryClass={math.LO},
url={https://arxiv.org/abs/2408.16428},
}

[12] G. F. Servi, “Axiomatizations for some Intuitionistic Modal Logics,” Rendiconti del Seminario Matematico dell’ Università Politecnica di Torino, vol. 42, iss. 3, p. 179–194, 1984.
[Bibtex]

@article{fischer-servi:84,
author="Gis\`ele Fischer Servi",
title="Axiomatizations for some Intuitionistic Modal Logics",
journal="Rendiconti del Seminario Matematico dell' Universit\`a Politecnica di Torino",
volume= 42,
number=3,
pages="179--194",
year=1984
}

[13] S. Marin and L. Straßburger, “Label-free Modular Systems for Classical and Intuitionistic Modal Logics,” in Advances in Modal Logic 10, invited and contributed papers from the tenth conference on “Advances in Modal Logic,” held in Groningen, The Netherlands, August 5-8, 2014, 2014, p. 387–406.
[Bibtex]

@inproceedings{MarStr14:mod-nest-systems,
author = {Sonia Marin and
Lutz Stra{\ss}burger},
editor = {Rajeev Gor{\'{e}} and
Barteld P. Kooi and
Agi Kurucz},
title = {Label-free Modular Systems for Classical and Intuitionistic Modal
Logics},
booktitle = {Advances in Modal Logic 10, invited and contributed papers from the
tenth conference on "Advances in Modal Logic," held in Groningen,
The Netherlands, August 5-8, 2014},
pages = {387--406},
publisher = {College Publications},
year = {2014},
url = {http://www.aiml.net/volumes/volume10/Marin-Strassburger.pdf},
timestamp = {Tue, 16 Jan 2024 17:18:03 +0100},
biburl = {https://dblp.org/rec/conf/aiml/MarinS14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

[14]

S. Marin, M. Morales, and L. Straßburger, “A fully labelled proof system for intuitionistic modal logics,” J. Log. Comput., vol. 31, iss. 3, p. 998–1022, 2021.
[Bibtex]

@article{MarMorStr21:fully-labelled,
author = {Sonia Marin and
Marianela Morales and
Lutz Stra{\ss}burger},
title = {A fully labelled proof system for intuitionistic modal logics},
journal = {J. Log. Comput.},
volume = {31},
number = {3},
pages = {998--1022},
year = {2021},
url = {https://doi.org/10.1093/logcom/exab020},
doi = {10.1093/LOGCOM/EXAB020},
timestamp = {Wed, 29 Sep 2021 08:56:10 +0200},
biburl = {https://dblp.org/rec/journals/logcom/MarinMS21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

[15] M. Mendler and V. de Paiva, “Constructive CK for Contexts,” in Proceedings of the 2nd International Conference on Context Representation and Reasoning (CRR 2005), 2005, p. 1–13.
[Bibtex]

@inproceedings{MendlerDePaiva2005,
author = {Mendler, Michael and de Paiva, Valeria},
title = {{C}onstructive {CK} for {C}ontexts},
booktitle = {Proceedings of the 2nd International {C}onference on Context Representation and Reasoning ({CRR} 2005)},
editor = {Serafini, Luciano and Bouquet, Philippe},
year = {2005},
pages = {1--13},
publisher = {CEUR-WS},
series = {CEUR-WS Series},
volume = {136},
url = {https://ceur-ws.org/Vol-136/143.pdf}
}

[16] D. Wijesekera, “Constructive modal logics I,” Annals of Pure and Applied Logic, vol. 50, iss. 3, p. 271–301, 1990.
[Bibtex]

@article{wijesekera:apal90,
title={Constructive modal logics {I}},
author={Wijesekera, Duminda},
journal={Annals of Pure and Applied Logic},
volume={50},
number={3},
pages={271--301},
year={1990},
publisher={Elsevier}
}

[17]

N. Alechina, M. Mendler, V. de Paiva, and E. Ritter, “Categorical and Kripke Semantics for Constructive S4 Modal Logic,” in 10th CSL, 2001, p. 292–307.
[Bibtex]

@InProceedings{alechina:etal:csl01,
author = "Natasha Alechina and Michael Mendler and Valeria de Paiva and Eike Ritter",
title = "Categorical and {K}ripke Semantics for Constructive {S4} Modal Logic",
booktitle = "10th CSL",
series = "LNCS",
volume = "2142",
pages = "292--307",
publisher = "Springer",
year = "2001",
doi = "10.1007/3-540-44802-0_21",
}

[18] L. Kovács and A. Voronkov, “First-Order Theorem Proving and Vampire,” in Computer Aided Verification, Berlin, Heidelberg, 2013, p. 1–35.
[Bibtex]

@InProceedings{KovVor2013:Vampire,
author="Kov{\'a}cs, Laura
and Voronkov, Andrei",
editor="Sharygina, Natasha
and Veith, Helmut",
title="First-Order Theorem Proving and Vampire",
booktitle="Computer Aided Verification",
year="2013",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="1--35",
}

[19] F. Bártek, A. Bhayat, R. Coutelier, M. Hajdu, M. Hetzenberger, P. Hozzová, L. Kovács, J. Rath, M. Rawson, G. Reger, M. Suda, J. Schoisswohl, and A. Voronkov, “The Vampire Diary,” in Computer Aided Verification, Cham, 2025, p. 57–71.
[Bibtex]

@InProceedings{VampireDiary25,
author="B{\'a}rtek, Filip
and Bhayat, Ahmed
and Coutelier, Robin
and Hajdu, M{\'a}rton
and Hetzenberger, Matthias
and Hozzov{\'a}, Petra
and Kov{\'a}cs, Laura
and Rath, Jakob
and Rawson, Michael
and Reger, Giles
and Suda, Martin
and Schoisswohl, Johannes
and Voronkov, Andrei",
editor="Piskac, Ruzica
and Rakamari{\'{c}}, Zvonimir",
title="The Vampire Diary",
booktitle="Computer Aided Verification",
year="2025",
publisher="Springer Nature Switzerland",
address="Cham",
pages="57--71",
}

2 thoughts on “Diamond-free parts of intuitionistic modal logics”

Geoff Sutcliffe says:
October 3, 2025 at 12:54 pm
Are the TPTP format problems available? I’d like to add thgem to the TPTP problem library.
1. Anupam Das says:
  October 4, 2025 at 8:56 am
  Hi Geoff! We placed the specifications here. There are two versions, one with the minimal upper bound and the ‘no-bound’ version.