On Intuitionistic Diamonds (and Lack Thereof)
Anupam Das, Sonia Marin · Lecture notes in computer science · 2023
Abstract A variety of intuitionistic versions of modal logic $$ K $$ have been proposed in the literature. An apparent misconception is that all these logics coincide on their $$\Box $$ -only (or $$\Diamond $$ -free) fragment, suggesting some robustness of ‘ $$\Box $$ -only intuitionistic modal logic’. However in this work we show that this is not true, by consideration of negative translations from classical modal logic: Fischer Servi’s $$ IK $$ proves strictly more $$\Diamond $$ -free theorems than Fitch’s $$ CK $$ , and indeed $$i K $$ , the minimal $$\Box $$ -normal intuitionistic modal logic. On the other hand we show that the smallest extension of $$i K $$ by a normal $$\Diamond $$ is in fact conservative over $$i K $$ (over $$\Diamond $$ -free formulas). To this end, we develop a novel proof calculus based on nested sequents for intuitionistic propositional logic due to Fitting. Along the way we establish a number of new metalogical results.