IK is an intuitionistic propositional modal logic.
IK is one of the 'smallest' extensions of intuitionistic propositional logic by both the (necessity) and (possibility) modalities. A similar logic which does not include the modality is sometimes known as CK.
The formulas of IK are given by the following grammar:
IK can be presented as a Hilbert system in [Plotkin and Stirling 1986].
Its two rules are modus ponens and necessitation
as well as instances of the following axioms:
is the usual K axiom of normal modal logics.
Modal logics are known to correspond to fragments of first-order logics.
[Simpson 1994, pg 54] argues that IK is somewhat 'canonical,' as it corresponds to intuitionistic first-order logic along the same translation that lifts K to classical first-order logic.
There is no known Gentzen-style, cut-free sequent calculus that is complete for IK [Simpson 1994, Das and Marin 2023].
However, [Simpson 1994] presents a number of labelled sequent calculi for a number of logics, including IK.
Plotkin, Gordon D., and Colin Stirling. ‘A Framework for Intuitionistic Modal Logics’. In Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge, Monterey, CA, USA, March 1986, edited by Joseph Y. Halpern. Morgan Kaufmann, 1986. [pdf]
@inproceedings{plotkin_1986,
title = {A Framework for Intuitionistic Modal Logics},
booktitle = {Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge, Monterey, {CA}, {USA}, March 1986},
publisher = {Morgan Kaufmann},
author = {Plotkin, Gordon D. and Stirling, Colin},
editor = {Halpern, Joseph Y.},
date = {1986}
}
Fischer Servi, Gisèle. ‘Semantics for a Class of Intuitionistic Modal Calculi’. In Italian Studies in the Philosophy of Science, edited by Maria Luisa Dalla Chiara, 47:59–72. Boston Studies in the Philosophy of Science. Dordrecht: Springer Netherlands, 1980. https://doi.org/10.1007/978-94-009-8937-5_5.
@inproceedings{cohen_semantics_1980,
location = {Dordrecht},
title = {Semantics for a Class of Intuitionistic Modal Calculi},
volume = {47},
doi = {10.1007/978-94-009-8937-5_5},
series = {Boston Studies in the Philosophy of Science},
pages = {59--72},
booktitle = {Italian Studies in the Philosophy of Science},
publisher = {Springer Netherlands},
author = {Fischer Servi, Gisèle},
editor = {Dalla Chiara, Maria Luisa},
editorb = {Cohen, Robert S. and Wartofsky, Marx W.},
editorbtype = {redactor},
date = {1980},
}
Simpson, Alex K. ‘The Proof Theory and Semantics of Intuitionistic Modal Logic’. PhD Thesis, The University of Edinburgh, 1994. http://hdl.handle.net/1842/407.
@thesis{simpson_1994,
title = {The Proof Theory and Semantics of Intuitionistic Modal Logic},
url = {http://hdl.handle.net/1842/407},
institution = {The University of Edinburgh},
type = {phdthesis},
author = {Simpson, Alex K.},
date = {1994},
}
Das, Anupam, and Sonia Marin. ‘On Intuitionistic Diamonds (and Lack Thereof)’. In Automated Reasoning with Analytic Tableaux and Related Methods, edited by Revantha Ramanayake and Josef Urban, 14278:283–301. Lecture Notes in Computer Science. Cham: Springer Nature Switzerland, 2023. https://doi.org/10.1007/978-3-031-43513-3_16.
@inproceedings{das_2023,
location = {Cham},
title = {On Intuitionistic Diamonds (and Lack Thereof)},
volume = {14278},
doi = {10.1007/978-3-031-43513-3_16},
series = {Lecture Notes in Computer Science},
pages = {283--301},
booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods},
publisher = {Springer Nature Switzerland},
author = {Das, Anupam and Marin, Sonia},
editor = {Ramanayake, Revantha and Urban, Josef},
date = {2023},
}