IK

IK is an intuitionistic propositional modal logic.

IK is one of the 'smallest' extensions of intuitionistic propositional logic by both the \Box (necessity) and \lozenge (possibility) modalities. A similar logic which does not include the \lozenge modality is sometimes known as CK.

Formulas

The formulas of IK are given by the following grammar:

A, B \Coloneqq p_i \mid \top \mid \bot \mid A \land B \mid A \lor B \mid A \to B \mid \Box A \mid \lozenge A

Hilbert system

IK can be presented as a Hilbert system in Plotkin and Stirling 1986.

Its two rules are modus ponens and necessitation

\frac{A \quad A  \to B}{B}
\qquad
\frac{A}{\Box A}

as well as instances of the following axioms:

All axioms of intuitionistic propositional logic
k_1: \Box (A \to B) \to (\Box A \to \Box B)
k_2: \Box (A \to B) \to (\lozenge A \to \lozenge B)
k_3: \lozenge (A \lor B) \to \lozenge A \lor \lozenge B
k_4: (\lozenge A \to \Box B) \to \Box (A \to B)
k_5: \lozenge \bot \to \bot

k_1 is the usual K axiom of normal modal logics.

Relationship to FOL

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.

Sequent calculus

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.

References

IK was introduced independently in the following two references.

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},
}

The proof theory of IK, including labelled sequent calculi, is discussed in detail in

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},
}

A recent reference with lots and lots of pointers to the literature is

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},
}