Brouwer meets Kripke: constructivising modal logic

Posted on August 19, 2022August 30, 2022 by Anupam Das and Sonia Marin

Intuitionistic logic and modal logic each admit meaningful projections of classical theories. While intuitionistic logic can interpret classical logic by a host of $\neg \neg$ translations, thus yielding computational interpretations, modal logic can be employed to understand notions of provability and truth. However, the enrichment of intuitionistic logic by modalities is far less canonical than its classical counterpart, giving rise to two prevailing approaches. In this post we survey the state of the art and revisit the role of intuitionistic modal logic in providing computational interpretations for classical modal logic.

Usual (propositional) modal logic extends the language of classical propositional logic by two modalities, $\Box$ and $\Diamond$ , informally representing ‘necessity’ and ‘possibility’ respectively. This informality is made precise by its well-known relational semantics. This semantics gives rise to the so-called ‘standard translation‘, allowing us to distill the normal modal logic $\mathsf K$ as a well-behaved fragment of the first-order logic (FOL):

Theorem. $\mathsf K$ is precisely the bisimulation-invariant fragment of FOL with a single binary relation.

Notably, in the classical setting $\Box$ and $\Diamond$ are De Morgan dual, just like $\forall$ and $\exists$ : we have that $\Diamond A = \neg \Box \neg A$ . However, in light of the association with FOL above, one would naturally expect an intuitionistic counterpart of modal logic not to satisfy any such reduction. In particular, while the usual axiomatisation of $\mathsf K$ simply extends propositional logic by the axiom and rule,

$k: \ \Box(A \to B) \to (\Box A \to \Box B)\qquad\qquad\mathit{nec}:\ \frac{A}{\Box A}$

notice that such an axiomatisation cannot be adequate for an intuitionistically based version of modal logic, which does not admit inter-reducibility of $\Box$ and $\Diamond$ . In particular, such an axiomatisation tells us nothing about $\Diamond$ !

Two main protagonists

The pursuit of a reasonable definition for an ‘intuitionistic’ modal logic goes back decades, including (but not limited to) works such as [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] [13] [14] [15] [16]. See [17] or [18] for a survey.

Ultimately two particular axiomatisations have received the lion’s share of attention from the community. To understand these, let us first list the following (classical) consequences of the $k$ axiom above:

$\begin{array}{rl}k_1: & \Box (A \to B) \to (\Box A \to \Box B) \\k_2: & \Box (A \to B) \to (\Diamond A \to \Diamond B) \\k_3: & \Diamond (A \vee B) \to (\Diamond A \vee \Diamond B) \\k_4: & (\Diamond A \to \Box B) \to \Box(A\to B) \\k_5: & \Diamond \bot \to \bot\end{array}$

Definition. $\mathsf{CK}$ is the extension of intuitionistic propositional logic (IPL) by $\mathit{nec}$ , $k_1$ and $k_2$ . $\mathsf{IK}$ is the extension of IPL by $\mathit{nec}$ and all the axioms above.

It seems that Fitch [1] was the first one to propose a way to treat $\Diamond$ in an intuitionistic setting by considering $\mathsf{CK}$ which has since become prominent in modal type theory. $\mathsf{CK}$ enjoys a rather natural proof-theoretic formulation that simply adapts the sequent calculus for $\mathsf K$ according to the usual intuitionistic restriction: each sequent may have just one formula on the RHS. What is more, cut-elimination for this simple calculus is just a specialisation of the classical case.

$\mathsf{IK}$ was introduced by [11] and is equivalent to the one proposed by [9], or even by [12] in the context of intuitionistic tense logic. In [17], Simpson gives logical arguments in favour of $\mathsf{IK}$ , namely as a logic that corresponds to intuitionistic FOL along the same standard translation that lifts $\mathsf K$ to classical FOL. The price to pay, however, is steep: there is no known cut-free sequent calculus complete for $\mathsf{IK}$ . On the other hand, Simpson demonstrates how the relational semantics of classical modal logic may be leveraged to recover a labelled sequent calculus, exemplifying the utility of pursuing an ‘intuitionistic standard translation’. The cut-elimination theorem, this time, specialises the cut-elimination theorem for intuitionistic FOL.

A most curious inadequacy

As we mentioned, $\mathsf{CK}$ has been the logic of choice for those working on the computational side of proof theory, vis à vis the ‘Curry-Howard‘ analogy. Indeed we now have several computational treatments of $\mathsf{CK}$ :

Categorical semantics [19]
(Dual-context) type theories [20], [21]
Cut-elimination via nested sequents [22]
Game semantics [23]

However there is an elephant in the room: at least one major utility of intuitionistic logic is that it is a constructive logic that can nonetheless interpret all of classical logic, e.g. via the Goedel-Gentzen (GG) $\neg\neg$ translation. In this way we can compose the former and the latter to recover a computational interpretation of classical logic. Choosing the right $\neg \neg$ translation here (e.g. GG) further facilitates the obtention of witnesses and computational content from classical modal logic. One could argue that this would be a reasonable property to ask for in any computationally oriented version of modal logic. However, it is not difficult to show:

Observation. $\mathsf{CK}$ does not validate the Goedel-Gentzen translation. In particular, it does not prove $\neg \neg \Box \neg p \to \Box \neg p$ .

Note that the proof of this result is very simple: it is clear that there is no cut-free proof of the given sequent, indeed since there is no correct rule to apply, and so there cannot be any proof at all, thanks to cut-elimination for $\mathsf{CK}$ .

A common misconception

On the other hand, it is very simple to show that $\mathsf{IK}$ does indeed validate the GG translation, unsurprisingly since it can simply be construed as an appropriate fragment of intuitionistic FOL. The argument is a simple induction on formula structure, but as an example let us give a proof of the separating sequent from the above Observation in the Hilbert system:

$\begin{array}{ll}\Box \neg p \to \Box \neg p & \text{identity} \\\Box \neg p \to (\Diamond p \to \Diamond \bot) & \text{by $k_2$} \\\Box \neg p \to (\Diamond p \to \bot) & \text{by $k_5$}\\\neg \neg \Box \neg p \to (\Diamond p \to \bot) & \text{since $\vdash \neg \Box \neg p \to \neg \neg \neg \Box \neg p$}\\\neg \neg \Box \neg p \to (\Diamond p \to \Box \bot) & \text{since $\vdash \bot \to \Box \bot$}\\\neg \neg \Box \neg p \to \Box \neg p & \text{by $k_4$}\end{array}$

This brings us to one of the main points of this post. It seems to be widely accepted that $\mathsf{CK}$ and $\mathsf{IK}$ do not differ on formulas that are $\Diamond$ -free, in particular that $\mathsf{IK}$ is conservative over $\mathsf{CK}$ in the language $\{\bot, \neg, \to, \Box\}$ . This might stem from the fact that many authors used the name ‘ $\mathsf{IK}$ ‘ indistinctively in early works, for what we have been calling $\mathsf{CK}$ , for its $\Diamond$ -free fragment, or just any constructively flavoured versions of $\mathsf{K}$ they were using. In the citation below for example, the authors are actually talking about what is now called $\mathsf{CK}$ :

We pursue an analogous correspondence for a basic intuitionistic (or constructive) modal logic $\mathsf{IK}$ with both necessity and possibility. […] We call this system $\mathsf{IK}_\Box$ for the $\Box$ -only fragment of $\mathsf{IK}$ .Bellin et al., 2001

In the intuitionistic modal Bible that constitutes Alex Simpson’s (unpublished!) PhD thesis, another statement on page 47 might have partly caused the confusion:

Only when the $\Diamond$ connective is added do the differences in the semantics become apparent. The logic [axiomatised by adding only $k_1$ and $\mathit{nec}$ to IPL] is uncontroversially the intuitionistic analogue of $\mathsf K$ in the $\Diamond$ -free fragment.Simpson, 1994

However, in light of the derivation and theorem above, these approximative statements are, at best, misleading.

Proposition. $\mathsf{CK}$ and $\mathsf{IK}$ are not the same on their $\Diamond$ -free fragments.

Whither, proof theorists?

Let us return to the pursuit for a computationally meaningful version of modal logic that can reasonably interpret the usual classical modal logic $\mathsf K$ . It looks like $\mathsf{IK}$ fits the bill! It inherits a computational interpretation from that of intuitionistic FOL, and interprets classical modal logic $\mathsf K$ via the usual GG translation.

Question. Why is there so much work on computational interpretations of $\mathsf{CK}$ and so little on $\mathsf{IK}$ ?

Let us point out, however, that Simpson already gives in his thesis a termination and confluence proof for a version of intuitionistic natural deduction specialised to $\mathsf{IK}$ . One may construe such deductions as terms in a natural way, thus inheriting a bona fide ‘Curry-Howard correspondence’ for $\mathsf{IK}$ , and so for classical $\mathsf K$ too under the GG translation. In fact this correspondence can be used to interpret labelled sequent proofs too, under the guise of realisability, giving rise to a semantics for $\mathsf{IK}$ alternative to its usual ‘birelational semantics‘.

Other translations and extensions

Let us point out that others have already observed the inadequacy of the GG translation with respect to $\mathsf{CK}$ , in particular in [24] where a host of other $\neg\neg$ translations were considered too. Naturally, translations such as the Kolmogorov translation remain validated by $\mathsf{CK}$ . However an unfortunate consequence of these translations is that they do not admit extensions of modal logics by fixed points, e.g. with a global modality $\Box^* A = A \wedge \Box \Box^*A$ . The problem here is that the $\neg\neg$ translation of the LHS and the RHS may not be again an instance of the fixed point equation, unless the translation at hand indeed commutes with $\Box$ and $\Box^*$ . Let us point out that this is no problem for GG since both $\Box$ and $\Box^*$ are negative, and thus induces a reduction of classical modal logic with global modalities to the corresponding extension of $\mathsf{IK}$ .

One might wonder what can be said about the relation between $\mathsf{CK}$ and $\mathsf{IK}$ furthermore in the $\{\Diamond, \neg, \bot\}$ -free fragment. A first attempt to eliminate negation (or $\bot$ ) would be to apply Friedman’s A translation. However recall that, under the standard translation, propositional letters are construed as predicate symbols with a free variable and are not closed, so we cannot get such a separation ‘for free’. Formalising the relationship between $\mathsf{CK}$ and $\mathsf{IK}$ on this fragment is, unfortunately, beyond the scope of this (now already rather long) post.

References

[1] F. B. Fitch, “Intuitionistic Modal Logic with Quantifiers,” Portugaliae Mathematica, vol. 7, iss. 2, p. 113–118, 1948.
[Bibtex]

@article{fitch:pm48,
author={Frederic B. Fitch},
title={Intuitionistic Modal Logic with Quantifiers},
journal={Portugaliae Mathematica},
volume={7},
number={2},
pages={113--118},
year={1948},
}

[2] H. B. Curry, “The elimination theorem when modality is present1,” The Journal of Symbolic Logic, vol. 17, iss. 4, p. 249–265, 1952.
[Bibtex]

@article{curry:52jsl,
title={The elimination theorem when modality is present1},
author={Curry, Haskell B},
journal={The Journal of Symbolic Logic},
volume={17},
number={4},
pages={249--265},
year={1952},
publisher={Cambridge University Press}
}

[3]

R. A. Bull, “A modal extension of intuitionist logic.,” Notre Dame Journal of Formal Logic, vol. 6, iss. 2, p. 142–146, 1965.
[Bibtex]

@article{bull:ndjfl65,
author = "Bull, Rowena A.",
title = "A modal extension of intuitionist logic.",
journal = "Notre Dame Journal of Formal Logic",
number = "2",
pages = "142--146",
publisher = "Duke University Press",
doi = "10.1305/ndjfl/1093958154",
url = "https://doi.org/10.1305/ndjfl/1093958154",
volume = "6",
year = "1965",
}

[4] R. A. Bull, “MIPC as the formalisation of an intuitionist concept of modality,” The Journal of Symbolic Logic, vol. 31, iss. 4, p. 609–616, 1966.
[Bibtex]

@article{bull:jsl66,
title={{MIPC} as the formalisation of an intuitionist concept of modality},
author={Bull, Rowena A.},
journal={The Journal of Symbolic Logic},
volume={31},
number={4},
pages={609--616},
year={1966},
publisher={Cambridge University Press}
}

[5] T. W. Satre, “Natural deduction rules for modal logics.,” Notre Dame Journal of Formal Logic, vol. 13, iss. 4, p. 461–475, 1972.
[Bibtex]

@article{satre:72ndjfl,
title={Natural deduction rules for modal logics.},
author={Satre, Thomas W},
journal={Notre Dame Journal of Formal Logic},
volume={13},
number={4},
pages={461--475},
year={1972},
publisher={Duke University Press}
}

[6] H. Ono, “On some intuitionistic modal logics,” Publications of the Research Institute for Mathematical Sciences, vol. 13, iss. 3, p. 687–722, 1977.
[Bibtex]

@article{ono:77prism,
title={On some intuitionistic modal logics},
author={Ono, Hiroakira},
journal={Publications of the Research Institute for Mathematical Sciences},
volume={13},
number={3},
pages={687--722},
year={1977}
}

[7]

D. F. Siemens, “Fitch-style rules for many modal logics.,” Notre Dame Journal of Formal Logic, vol. 18, iss. 4, p. 631–636, 1977.
[Bibtex]

@article{siemens:ndjfl77,
author = "Siemens, David F.",
title = "Fitch-style rules for many modal logics.",
doi = "10.1305/ndjfl/1093888133",
journal = "Notre Dame Journal of Formal Logic",
number = "4",
pages = "631--636",
publisher = "Duke University Press",
url = "https://doi.org/10.1305/ndjfl/1093888133",
volume = "18",
year = "1977",
}

[8] G. Fischer-Servi, “Semantics for a Class of Intuitionistic Modal Calculi,” Italian Studies in the Philosophy of Science. Boston Studies in the Philosophy of Science, vol. 47, 1980.
[Bibtex]

@article{fischer-servi:bsps80,
author = {Gis{\`e}le Fischer-Servi},
title = {Semantics for a Class of Intuitionistic Modal Calculi},
journal = {Italian Studies in the Philosophy of Science. Boston Studies in the Philosophy of Science},
year = {1980},
editor = {Dalla Chiara M.L.},
volume = {47},
publisher = {Springer, Dordrecht}
}

[9] 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
}

[10] M. Božić and K. Došen, “Models for normal intuitionistic modal logics,” Studia Logica, vol. 43, iss. 3, p. 217–245, 1984.
[Bibtex]

@article{bozic:dosen:84sl,
title={Models for normal intuitionistic modal logics},
author={Bo{\v{z}}i{\'c}, Milan and Do{\v{s}}en, Kosta},
journal={Studia Logica},
volume={43},
number={3},
pages={217--245},
year={1984},
publisher={Springer}
}

[11] G. Plotkin and C. Stirling, “A framework for intuitionistic modal logics,” in Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge (TARK), 1986, p. 399–406.
[Bibtex]

@inproceedings{plotkin:stirling:86tark,
title={A framework for intuitionistic modal logics},
author={Plotkin, Gordon and Stirling, Colin},
booktitle={Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge (TARK)},
pages={399--406},
year={1986}
}

[12] W. B. Ewald, “Intuitionistic tense and modal logic,” The Journal of Symbolic Logic, vol. 51, iss. 1, p. 166–179, 1986.
[Bibtex]

@article{ewald:86jsl,
title={Intuitionistic tense and modal logic},
author={Ewald, William Bragg},
journal={The Journal of Symbolic Logic},
volume={51},
number={1},
pages={166--179},
year={1986},
publisher={Cambridge University Press}
}

[13] J. M. Font, “Modality and possibility in some intuitionistic modal logics.,” Notre Dame Journal of Formal Logic, vol. 27, iss. 4, p. 533–546, 1986.
[Bibtex]

@article{font:ndjfl86,
title={Modality and possibility in some intuitionistic modal logics.},
author={Font, Josep M.},
journal={Notre Dame Journal of Formal Logic},
volume={27},
number={4},
pages={533--546},
year={1986},
publisher={University of Notre Dame}
}

[14] H. Ono and N. Suzuki, “Relations between intuitionistic modal logics and intermediate predicate logics,” Reports on Mathematical Logic, vol. 22, p. 65–87, 1988.
[Bibtex]

@article{ono:suzuki:rml88,
title={Relations between intuitionistic modal logics and intermediate predicate logics},
author={Ono, Hiroakira and Suzuki, Nobu-Yuki},
journal={Reports on Mathematical Logic},
volume={22},
pages={65--87},
year={1988}
}

[15] N. Suzuki, “An algebraic approach to intuitionistic modal logics in connection with intermediate predicate logics,” Studia Logica, vol. 48, iss. 2, p. 141–155, 1989.
[Bibtex]

@article{suzuki:sl89,
title={An algebraic approach to intuitionistic modal logics in connection with intermediate predicate logics},
author={Suzuki, Nobu-Yuki},
journal={Studia Logica},
volume={48},
number={2},
pages={141--155},
year={1989},
publisher={Springer},
}

[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] 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",
}

[18] G. A. Kavvos, “The Many Worlds of Modal $\lambda$ -calculi: I. Curry-Howard for Necessity, Possibility and Time,” CoRR, vol. abs/1605.08106, 2016.
[Bibtex]

@article{kavvos:16survey,
author = {G. A. Kavvos},
title = {The Many Worlds of Modal {}-calculi: I. Curry-Howard for
Necessity, Possibility and Time},
journal = {CoRR},
volume = {abs/1605.08106},
year = {2016},
url = {http://arxiv.org/abs/1605.08106},
eprinttype = {arXiv},
eprint = {1605.08106},
timestamp = {Mon, 13 Aug 2018 16:48:19 +0200},
biburl = {https://dblp.org/rec/journals/corr/Kavvos16c.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

[19] G. Bellin, V. De Paiva, and E. Ritter, “Extended Curry-Howard correspondence for a basic constructive modal logic,” in Proceedings of methods for modalities, 2001.
[Bibtex]

@inproceedings{bellin:etal:01,
title={Extended Curry-Howard correspondence for a basic constructive modal logic},
author={Bellin, Gianluigi and De Paiva, Valeria and Ritter, Eike},
booktitle={Proceedings of methods for modalities},
volume={2},
year={2001}
}

[20] F. Pfenning and R. Davies, “A judgmental reconstruction of modal logic,” Mathematical Structures in Computer Science, vol. 11, iss. 4, p. 511–540, 2001.
[Bibtex]

@article{pfenning:davies:mscs01,
author = {Frank Pfenning and Rowan Davies},
title = {A judgmental reconstruction of modal logic},
journal = {Mathematical Structures in Computer Science},
volume = {11},
number = {4},
year = {2001},
pages = {511--540},
note = "Notes to an invited talk at the Workshop on Intuitionistic Modal Logics and Applications (IMLA'99)",
}

[21]

G. A. Kavvos, “Dual-context calculi for modal logic,” in 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, 2017, p. 1–12.
[Bibtex]

@inproceedings{kavvos:lics17,
author = {G. A. Kavvos},
title = {Dual-context calculi for modal logic},
booktitle = {32nd Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS}
2017, Reykjavik, Iceland, June 20-23, 2017},
pages = {1--12},
publisher = {{IEEE} Computer Society},
year = {2017},
url = {https://doi.org/10.1109/LICS.2017.8005089},
doi = {10.1109/LICS.2017.8005089},
timestamp = {Wed, 16 Oct 2019 14:14:54 +0200},
biburl = {https://dblp.org/rec/conf/lics/Kavvos17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

[22] R. Arisaka, A. Das, and L. Straßburger, “On Nested Sequents for Constructive Modal Logic,” Logical Methods in Computer Science, 2015.
[Bibtex]

@article{arisaka:etal:lmcs15,
author = {Ryuta Arisaka and Anupam Das and Lutz Stra{\ss}burger},
title = {On Nested Sequents for Constructive Modal Logic},
journal = {Logical Methods in Computer Science},
year = 2015
}

[23] M. Acclavio, D. Catta, and L. Straßburger, “Game semantics for constructive modal logic,” in International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, 2021, p. 428–445.
[Bibtex]

@inproceedings{acclavio:etal:21tabl,
title={Game semantics for constructive modal logic},
author={Acclavio, Matteo and Catta, Davide and Stra{\ss}burger, Lutz},
booktitle={International Conference on Automated Reasoning with Analytic Tableaux and Related Methods},
pages={428--445},
year={2021},
organization={Springer}
}

[24]

T. Litak, M. Polzer, and U. Rabenstein, “Negative Translations and Normal Modality,” in 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Dagstuhl, Germany, 2017, p. 27:1–27:18.
[Bibtex]

@InProceedings{litak_et_al:LIPIcs:2017:7741,
author =  {Tadeusz Litak and Miriam Polzer and Ulrich Rabenstein},
title =  {{Negative Translations and Normal Modality}},
booktitle =  {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
pages =  {27:1--27:18},
series =  {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN =  {978-3-95977-047-7},
ISSN =  {1868-8969},
year =  {2017},
volume =  {84},
editor =  {Dale Miller},
publisher =  {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address =  {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7741},
URN = {urn:nbn:de:0030-drops-77412},
doi = {10.4230/LIPIcs.FSCD.2017.27},
annote =  {Keywords: negative translations, intuitionistic modal logic, normal modality, double negation}
}

22 thoughts on “Brouwer meets Kripke: constructivising modal logic”

Alex Simpson says:

August 24, 2022 at 6:27 pm

Thanks for this interesting posting. You are right that the statement you quote from my thesis is incorrect. This was first pointed out to me by Carsten Grefe in December 1996, who was I think a PhD student in Berlin at the time. His “simplest” example of a diamond-free formula that is IK but not CK provable was:

$(\neg \Box \bot \rightarrow \Box \bot) \rightarrow \Box \bot$

. I recall that he also told me that the diamond-free fragment of IK is not finitely axiomatisable by diamond-free axioms.

Reply
1. Anupam Das says:
  
  August 25, 2022 at 3:07 pm
  
  Thanks for jumping in and clarifying this Alex! Do you have a reference for Carsten’s claim that $\Diamond$ -free $\mathsf{IK}$ is not finitely $\Diamond$ -free axiomatisable? (I cannot seem to access what DBLP believes is his only paper.)
  
  I reflected on Carsten’s ‘simplest’ example, in particular on its derivation in $\mathsf{IK}$ . I feel like one still requires $k_4$ to derive it (though I am biased by the nested sequent methodology). Namely one should use the instance $(\Diamond \top \to \Box \bot) \to \Box ( \top \to \bot)$ . Using $\bot \equiv \top \to \bot$ thence allows us to assume $\Diamond \top$ among the antecedents to prove $\neg \Box \bot$ , whence the implication becomes derivable in $\mathsf{CK} + k_5$ .
  
  This raises another question: what is the relationship between $\mathsf{CK} + k_3 + k_5$ and $\mathsf{CK}$ over $\Diamond$ -free formulas? I always imagined that the real distinction of $\mathsf{IK}$ is due to $k_4$ , but I hestitate to make any assumption at this point :).
  
  Reply
  1. Alex Simpson says:
    
    August 26, 2022 at 8:07 am
    
    Re: “Do you have a reference for Carsten’s claim that \Diamond-free \mathsf{IK} is not finitely \Diamond-free axiomatisable? ”
    
    No, and I don’t think this appears in his paper (which gives a different proof of the finite model property of IK from my proof). I have a vague recollection that Carsten sent me some of the details by email, but now I can’t find this correspondence. I don’t know if the non-finite-axiomatisability result appears in his PhD thesis, which is presumably available from Berlin University.
    
    Reply
Alex Simpson says:

August 26, 2022 at 8:28 am

I would also like to add one reference that is tangentially relevant to:

“Question. Why is there so much work on computational interpretations of \mathsf{CK} and so little on \mathsf{IK}?”

If one looks at S5 instead of K, then there is a paper that provides a computational interpretation of IS5; namely of the “I” version of S5 rather than of some “C” version of S5:

Tom Murphy VII, Karl Crary, Robert Harper, and Frank Pfenning. A symmetric modal lambda calculus for distributed computing. In H. Ganzinger, editor, Proceedings of the 19th Annual Symposium on Logic in Computer Science (LICS’04), pages 286–295, 2004

Since IK is a sub-logic of IS5, this paper in particular gives a computational interpretation to all axioms of IK.

Reply
Reuben Rowe says:

August 28, 2022 at 10:29 am

Thanks for an interesting post, guys! I have one question, which may be somewhat naive: I couldn’t figure out which formula $¬ ¬ \Box ¬ p \rightarrow \Box ¬ p$ is the GG translation of. Can you help me out?

Reply
Reuben Rowe says:

August 28, 2022 at 10:34 am

Obviously, I meant which formula $\neg \neg \Box \neg p \rightarrow \Box \neg p$ is the GG translation of!

Reply
1. Anupam Das says:
  
  August 30, 2022 at 12:34 pm
  
  Hi Reuben, sorry we could have been clearer here.
  
  First, as we have set it up, $\Box\neg p$ is the GG translation of itself, since GG is defined, in particular, by commuting with $\bot, \neg, \wedge, \to, \Box$ and negated propositional variables (other connectives are written in this basis in a canonical way via De Morgan duality). NB: some versions of GG require an extra two negations immediately in front of the $p$ , for a simpler compositional definition, say GG’. $\mathsf{CK}$ still does not validate this version of GG, e.g. by considering $\Box \neg \neg p$ (which is the GG’-translation of $\Box p$ ) instead of $\Box \neg p$ in this post.
  
  Now, when we say that some intuitionistic system $\mathsf I$ validates the GG translation, we mean that, for any formula $A$ , we have that $\mathsf I \vdash \neg \neg A^{\mathit{GG}} \to A^{\mathit{GG}}$ . In this post we have argued the $\mathsf{CK}$ does not validate the GG translation (e.g. by setting $A = \Box \neg p$ ), and we claim (but omit proof) that $\mathsf{IK}$ does.
  
  By the way, one could ask for the apparently weaker version of validation that, whenever $\mathsf{K}\vdash A$ then $\mathsf I \vdash A^{\mathit{GG}}$ . Note that $\mathsf{CK}$ does not even have this property since the implication $\neg \neg \Box \neg p \to \Box \neg p$ is the GG-translation of itself. Similarly for GG’, by consideration of $\neg \neg \Box p \to \Box p$ and its GG’-translation.
  
  Reply
  1. Reuben Rowe says:
    
    August 30, 2022 at 3:24 pm
    
    Thanks for the clarifications, Anupam. By the way, my research seems to suggest that your GG’ translation is the “standard” one; can you give a reference for the version not requiring $p$ to be translated as $\neg \neg p$ ?
    
    Reply
    1. Anupam Das says:
      
      August 31, 2022 at 2:55 pm
      
      Indeed, I should have said ‘typical’ rather than ‘some’. I don’t have a reference but, logically speaking, one may consider it a minor variant, in the sense that the only difference is that some occurrences of $\neg\neg\neg p$ are replaced by $\neg p$ . Of course, these are intuitionistically equivalent. Similar minor variations of the GG translation present in their action on a disjunction, setting $(A\vee B)^{\mathit{GG}}$ to be either $\neg (\neg A^{\mathit{GG}} \wedge \neg B^{\mathit{GG}})$ or $\neg \neg (A^{\mathit{GG}} \vee B^{\mathit{GG}})$ , or an existential, setting $(\exists x A)^{\mathit{GG}}$ to be either $\neg \forall x \neg A^{\mathit{GG}}$ or $\neg \neg \exists x A^{\mathit{GG}}$ . This indifference is made explicit in, e.g., in the nLab article, while the two conventions are employed respectively, e.g., by the Wikipedia article and by a paper by Ferreira and Oliva.
      
      Might I add, somehow the choice of $\neg p$ as subformula in our ‘counterexample’ is arbitrary. What is interesting is that $\mathsf{IK}$ validates the notion of ‘negative connective’ induced by GG, while $\mathsf{CK}$ does not. To be clear, $\mathsf{IK}$ proves that $\neg\neg$ commutes with negative connectives, namely $\bot,\wedge,\to,\Box$ . Indeed in the modal case, $\neg\neg \Box p \to \Box \neg\neg p$ yields another separation between $\mathsf{IK}$ and $\mathsf{CK}$ that better emphasises this distinguishing feature than the role of propositional variables/literals.
      
      Reply
Nicola Olivetti says:

August 29, 2022 at 8:22 am

Hello,
thanks Anupam, Sonia, and Alex for this very interesting discussion! I have checked the two counterexamples semantically. I was discussing also the issue with Tiziano (Dalmonte). As far as I understand, both frames conditions called F1 and F2 in Alex semantics are needed to validate Anupam & Sonia’s formula, whereas only F1 condtion (the one needed to ensure hereditary property of Diamond formula) is needed to validate the formula proposed by Alex. Now as said condtion F1 is needed in order to ensure that the local definition of Diamond satisfies hereditary property. Thus Alex counterxample seems to give a negative answer to the question by Anupam: even dropping axiom k4, the fragment with only Box of the resulting system would be different from the same fragment of CK (and Wisejekera propositional CCDL). I would also be very intersted to see a proof that the Box-fragment of IK (I mean the diamond-free) is not finitely axiomatisable. I notice that the nested sequent calculus “implicitly” (= in its formula translation) introduces diamond formulas even in the case the sequent to prove contains only formulas without without diamond.
Best
Nicola

Reply
1. Sonia says:
  
  August 31, 2022 at 10:03 am
  
  Hi Nicola, thank you for your comments.
  
  >> As far as I understand, both frames conditions called $F_1$ and $F_2$ in Alex semantics are needed to validate Anupam & Sonia’s formula, whereas only $F_1$ condition (the one needed to ensure hereditary property of $\Diamond$ formula) is needed to validate the formula proposed by Alex.
  
  Indeed, very interesting, I had not noticed this, but it seems to be the case.
  
  >> Thus Alex counter-example seems to give a negative answer to the question by Anupam: even dropping axiom $k_4$ , the fragment with only $\Box$ of the resulting system would be different from the same fragment of $\mathsf{CK}$ (and Wisejekera propositional CCDL).
  
  Do you mean that there is a direct correspondence between the axiom $k_4$ and the $F_2$ frame condition? I do not think I knew this. Do you have the reference for this result?
  
  So can you provide an explicit $k_4$ -free axiomatic derivation of Carsten’s formula? I could not easily construct it. Actually, as Tiziano already observed (and told us at AiML), we do not know of a sequent calculus that is cut-free complete for $\mathsf{CK}$ + $k_3$ + $k_5$ , so this makes it harder for me to figure it out.
  
  >> I notice that the nested sequent calculus “implicitly” (= in its formula translation) introduces diamond formulas even in the case the sequent to prove contains only formulas without diamond.
  
  Indeed “implicit diamonds” in both labelled and nested sequents seem to be the key to unlocking the IK potential 😉
  
  Reply
  1. Tiziano Dalmonte says:
    
    September 1, 2022 at 4:40 pm
    
    Thank you all for the very interesting post and discussion!
    
    Indeed, semantically speaking, it seems that it is F1 that makes all the difference between the Box-fragments of IK and CK. Here a simple argument:
    
    Let me call birelational model any model with <= and R, no matter what conditions among F1, F2, etc, it satisfies (so for instance IPL + Nec + k1, i.e. the Box-fragment of CK and Wijesekera's system, is complete with respect to all birelational models).
    
    If I am not mistaken, we can prove that IPL + Nec + k1 is complete with respect to all birelational models satisfying the condition (F2') if xRy and y <= y', then xRy' (the proof is by simple model transformation, converting any birelational model into an equivalent model satisfying this condition).
    
    Since F2' is a stronger version of F2, it follows that IPL + Nec + k1 is also complete with respect to all birelational models satisfying F2.
    
    By contrast, now we know that IPL + Nec + k1 is NOT complete with respect to the birelational models satisfying F1, since the semantics validates Carsten's formula which is not a theorem.
    
    So of course IPL + Nec + k1 is neither complete with respect to the birelational models satisfying both F1 and F2, as the formulas proposed by Sonia and Anupam show.
    
    Concerning now the logics with both Box and Diamond, and referring to Nicola's and Sonia's comments, what does Carsten's formula tell us about CK + k3 + k5?
    Well, we know that in order to validate k3 we need the local interpretation of Diamond, and that given the local interpretation of Diamond we need F1 to ensure the hereditary property. So Carsten's formula should be valid in any reasonable birelational semantics for CK + k3 + k5.
    
    Note that this does not necessarily mean that CK + k3 + k5 derives Carsten's formula. It can rather be that CK + k3 + k5, if not extended with other axioms (like Carsten's formula or so) does not have any decent birelational semantics.
    
    Reply
    1. Anupam Das says:
      
      September 2, 2022 at 2:20 pm
      
      Tiziano, in your last paragraph you say:
      
      Note that this does not necessarily mean that CK + k3 + k5 derives Carsten’s formula.
      
      But in fact Nicola is claiming precisely that:
      
      Thus [Carsten’s formula] seems to give a negative answer to the question by Anupam: even dropping axiom k4, the fragment with only Box of the resulting system would be different from the same fragment of CK
      
      Is there some misunderstanding here?
      
      Reply
Dale Miller says:

August 31, 2022 at 10:26 am

Thanks, Sonia and Anupam, for this interesting survey of intuitionistic modal logics. Most of this was new to me.

I have a beginner’s question. Goedel showed that one S4 modal operator in classical logic can encode intuitionistic propositional logic. So I imagine one way to encode an intuitionistic modal logic might be to use two modal operators in classical logic. I suspect such encodings are unappealing to most, but still, I’d be interested to know of a reference to such an approach.

Reply
1. Dominik Kirst says:
  
  September 6, 2022 at 7:19 pm
  
  Such an embedding of intuitionistic modal logic into classical bimodal logic has been given by Wolter and Zakharyaschev:
  
  Wolter, Frank, and Michael Zakharyaschev. “Intuitionistic modal logics as fragments of classical bimodal logics.” Logic at work (1997): 168-186.
  
  https://www.researchgate.net/publication/2446198_Intuitionistic_Modal_Logics_as_Fragments_of_Classical_Bimodal_Logics
  
  Reply
  1. Dale Miller says:
    
    September 7, 2022 at 3:50 pm
    
    Thanks, Dominik, for this reference. I’ll add them to the ones offered by Iris.
    
    Reply
Nicola Olivetti says:

September 3, 2022 at 4:25 pm

Hello,
Thanks all for the interesting observations and questions. Concerning the last point raised by Anupam: if I am not wrong (I must type and re-check the proof), I proved that IK-without the axiom K4, that is CK+ K3+K5 is complete with respect to Models with frame condition F1. Since this condition makes valid Carsten’s formula, by completeness it must be derivable by CK+ K3+K5. So that we can conclude that the implicational fragment of CK+ K3+K5 is stronger than the corresponding fragment of CK. This is what I meant writing that “Carsten formula gives a negative answer to Anupam’s question.
However I haven not tried yet to derive Carsten formula from the axioms… I hope to have time in the next days.
By the way, I am not sure I understand the 4th step in the Hilbert derivation given by Sonia and Anupam of their formula, am I missing anything?

Reply
1. Anupam Das says:
  
  September 5, 2022 at 2:35 pm
  
  Please do let us know about the derivation and the completeness result you mention when you can.
  
  For the 4th step, this is a standard trick in $\mathsf{IPL}$ for $\neg\neg$ -elimination when the consequent is $\bot$ (or ’empty’). To expand out the step use the following schematic reasoning,
  
  $\begin{array}{ll} A \to (B\to \bot) & \\ B \to (A \to \bot) & \text{by Currying and commutativity of $\wedge$} \\ B \to \neg A & \text{since $\vdash \neg A \equiv (A\to \bot)$}\\ B \to \neg \neg \neg A & \text{since $\vdash \neg A \to\neg \neg \neg A$ }\\ B \to (\neg \neg A \to \bot) & \text{since $\vdash \neg \neg \neg A \equiv (\neg \neg A \to \bot)$}\\ \neg \neg A \to (B \to \bot) & \text{by Currying and commutativity of $\wedge$} \end{array}$
  
  setting $A:= \Box \neg p$ and $B:= \Diamond p$ .
  
  Reply
2. Anupam Das says:
  
  September 13, 2022 at 5:04 pm
  
  Just to add one point: it is not hard to show that the simplest instance of $\neg\neg$ -elimination for negative formulas, namely $N := \neg \neg \Box \bot \to \Box \bot$ , is already a consequence of Carsten’s formula within $\mathsf{CK}$ . On the other hand $\mathsf{CK}$ does not prove $N$ by the same reasoning as before: there is no cut-free proof. Putting this together, if Carsten’s formula separates $\mathsf{CK}$ from $\mathsf{CK} + k_3 + k_5$ , then there is a simpler such separation by the formula $N$ .
  
  Reply
Iris van der Giessen says:

September 6, 2022 at 5:27 pm

Hi all, thanks for the interesting discussion!

In reply to Dale’s question:
It’s indeed possible to translate intuitionistic modal logics into bimodal logics. Research on this already started in the 70’s. Fischer Servi [1], for instance, provides the connection between $S5-IC$ , also known as $MIPC$ , which is, as I understand it,

$\text{the box-fragment of CK} + S5\text{-axioms} + \Box p \leftrightarrow \neg \Diamond \neg p$

into bimodal logic $(S4,S5)$ . Later Wolter and Zakharyaschev [2,3] wrote papers on similar embeddings for a wide class of intuitionistic modal logics into bimodal logics to obtain general completeness results. If I am correct, he denotes $IK$ as $FS$ (after Fischer Servi) and provides the embedding and bimodal logic in Corollary 36 from [2]. All proof methods are based on semantics.

[1] G. Fischer Servi, “On modal logic with an intuitionistic base,” Studia Logica, vol. 36, 1977.

[2] F. Wolter and M. Zakharyaschev, “On the relation between intuitionistic and classical modal logics,” Algebra and Logic, vol. 36, 1997.

[3] F. Wolter and M. Zakharyaschev, “Intuitionistic modal logics as fragments of classical bimodal logics” Logics at Work, Studies in Fuzziness Soft Computing, vol. 24, 1999.

Reply
1. Dale Miller says:
  
  September 7, 2022 at 3:49 pm
  
  Thanks, Iris, for these references.
  
  Reply
2. Iris van der Giessen says:
  
  October 14, 2022 at 4:05 pm
  
  I have to correct myself. $MIPC$ is NOT the thing that I mentioned in the post above. That is another axiomatization that Fischer Servi discusses in [1] and she does not consider that as the true analogue of classical $S5$ . The duality between box and diamond is usually not taken in the intuitionistic modal setting, but in [3], Wolter and Zakharyaschev actually take $\Diamond$ defined as $\neg \Box \neg$ to study intuitionistic versions of classical modal logics. In [2], they drop this definition and study systems like Fischer Servi. So, as I understand it now, $MIPC$ is $IK$ + $S5$ -axioms.
  
  Reply