This short post is a follow-up to Sonia and Anupam’s blog post on constructive modal logics; I present a quick direct proof that the constructive modal logic is conservative over on the -free fragment. This was first discussed in the comment section to the aforementioned blog post (as an open problem), and eventually obtained in [1] as a corollary of cut-elimination in a nested sequent calculus for .

For the necessary background on constructive modal logics, please refer to the blog post. I only repeat the relevant axioms here:

is the extension of intuitionistic propositional logic () by and , where as rules we allow Modus Ponens and -Necessitation. As the name suggests, adds to this the axioms and .

Theorem.is conservative over on the -free fragment.

*Proof.* Let denote the result of replacing all -subformulas in by . Then by a simple induction on Hilbert-style derivations, we can show that implies . As for -free the conservativity result follows immediately.

The key observation in the induction is that turns the axioms , and into the formulas , and all of which are already theorems of . Moreover , and the rules of -Necessitation and Modus Ponens are closed under .

Note that the -translation of amounts to which is *not* a theorem of . This is to be expected: Otherwise we would get conservativity of over on the -free fragment, which is known to be false [1].

It seems to be unknown whether is conservative over on the -free fragment.

As a concluding remark, artificial interpretations such as are often the fastest way to show that a logic is consistent. For example, consider and let be the translation that maps -subformulas to and -subformulas to . Then by a simple induction,

. In particular is conservative over on the -free fragment (that is, on purely propositional formulas), and therefore does not prove .[Bibtex]

```
@inproceedings{das2023intuitionistic,
title={On intuitionistic diamonds (and lack thereof)},
author={Das, Anupam and Marin, Sonia},
booktitle={International Conference on Automated Reasoning with Analytic Tableaux and Related Methods},
pages={283--301},
year={2023},
organization={Springer}
}
```

I’ve said this to you already but…. this is really cool! Nice to see that such a simple translation does the job. In the paper you reference we consider some other translations like and which give, e.g., -free conservativity of over , but AFAIK the question is still open for -free conservativity. Note that the final sentence of Alex’s comment to our post suggests that such conservativity should

nothold.