A note on conservativity in constructive modal logics

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 $CK+k_3+k_5$ is conservative over $CK$ on the $\Diamond$ -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 $CK+k_3+k_5$ .

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

$k_1:\qquad \Box(A\rightarrow B)\rightarrow (\Box A\rightarrow\Box B)$
$k_2:\qquad \Box(A\rightarrow B)\rightarrow (\Diamond A\rightarrow\Diamond B)$
$k_3:\qquad \Diamond(A\lor B)\rightarrow (\Diamond A\lor\Diamond B)$
$k_4:\qquad (\Diamond A\rightarrow \Box B)\rightarrow \Box(A\rightarrow B)$
$k_5:\qquad \Diamond\bot\rightarrow\bot$

$CK$ is the extension of intuitionistic propositional logic ( $IPL$ ) by $k_1$ and $k_2$ , where as rules we allow Modus Ponens and $\Box$ -Necessitation. As the name suggests, $CK+k_3+k_5$ adds to this the axioms $k_3$ and $k_5$ .

Theorem. $CK+k_3+k_5$ is conservative over $CK$ on the $\Diamond$ -free fragment.

Proof. Let $A^\tau$ denote the result of replacing all $\Diamond$ -subformulas in $A$ by $\bot$ . Then by a simple induction on Hilbert-style derivations, we can show that $CK+k_3+k_5\vdash A$ implies $CK\vdash A^\tau$ . As $A^\tau=A$ for $\Diamond$ -free $A$ the conservativity result follows immediately.

The key observation in the induction is that $\tau$ turns the axioms $k_2$ , $k_3$ and $k_5$ into the formulas $(\Box A^\tau\rightarrow\Box B^\tau)\rightarrow(\bot\rightarrow\bot)$ , $\bot\rightarrow\bot\lor\bot$ and $\bot\rightarrow\bot$ all of which are already theorems of $IPL$ . Moreover $k_1$ , $IPL$ and the rules of $\Box$ -Necessitation and Modus Ponens are closed under $\tau$ .

Note that the $\tau$ -translation of $k_4$ amounts to $(\bot\rightarrow\Box B^\tau)\rightarrow\Box (A^\tau\rightarrow B^\tau)$ which is not a theorem of $CK$ . This is to be expected: Otherwise we would get conservativity of $IK$ over $CK$ on the $\Diamond$ -free fragment, which is known to be false [1].

It seems to be unknown whether $IK=CK+k_3+k_4+k_5$ is conservative over $CK+k_4+k_5$ on the $\Diamond$ -free fragment.

As a concluding remark, artificial interpretations such as $\tau$ are often the fastest way to show that a logic is consistent. For example, consider $IK$ and let $\sigma$ be the translation that maps $\Box$ -subformulas to $\top$ and $\Diamond$ -subformulas to $\bot$ . Then by a simple induction, $IK\vdash A$ implies $IPL\vdash A^\sigma$ . In particular $IK$ is conservative over $IPL$ on the $\{\Box,\Diamond\}$ -free fragment (that is, on purely propositional formulas), and therefore $IK$ does not prove $\bot$ .

[1] A. Das and S. Marin, “On intuitionistic diamonds (and lack thereof),” in International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, 2023, p. 283–301.
[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}
}

3 thoughts on “A note on conservativity in constructive modal logics”

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 $\Diamond \mapsto \neg \Box \neg$ and $\vee \mapsto \neg \wedge \neg$ which give, e.g., $\{\Diamond,\vee\}$ -free conservativity of $\mathsf{IK}$ over $\mathsf{CK}+k_4+k_5$ , but AFAIK the question is still open for $\Diamond$ -free conservativity. Note that the final sentence of Alex’s comment to our post suggests that such conservativity should not hold.

I wanted to point out that de Groot, Shillito and Clouston have a new preprint out exploring the relationships between $\Diamond$ -free fragments semantically (rather than proof-theoretically):

https://arxiv.org/abs/2408.00262 .

One pertinent reflection from this is what happens when one sets $\Diamond A := \top$ , as opposed to $\bot$ as in your post. It is not hard to see that this lifts to an interpretation of $\mathit{CK} + k_3 + k_4$ into $\mathit{CK}$ , and so even $\mathit{CK} + k_3 + k_4$ is $\Diamond$ -free conservative over $\mathit{CK}$ (and so $\mathit{iK}$ too).

Thank you Anupam for pointing out this preprint, you are right that the trick with setting $\Diamond A:=\top$ works here. It is only the combination of $k_4$ and $k_5$ which rules out a trivial interpretation of $\Diamond$ .

3 thoughts on “A note on conservativity in constructive modal logics”

Leave a Reply Cancel reply