Intuitionistic modal logic

An intuitionistic modal logic should be a logic that is both intuitionistic at its core, but is also equipped with modalities, usually denoted \lozenge, \Box, \ldots.

It is not so easy to tell what such a logic should look like, and many different variants have been studied.

Simpson's criteria

In his PhD thesis Simpson 1994, Alex Simpson proposed six criteria that an intuitionistic modal logic should satisfy:

1. It should be conservative over intuitionistic logic.
2. It should prove all intuitionistic theorems (even with modalities, e.g. \Box \varphi \to (\psi \to \Box \varphi)).
3. Adding the law of the excluded middle \varphi \lor \lnot \varphi should yield a classical modal logic.
4. It should satisfy the disjunction property.
5. \Box and \lozenge should be independent.
6. The semantics of modalities should be ‘intuitionistically comprehensible.'

The last condition is not formal. In Simpson's thesis it is interpreted as follows. Suppose we have a Kripke semantics given by a satisfaction relation w \vDash \varphi. We can express the definition of that clause in a first-order logic, obtaining a sentence \textsf{ksat}(w, \varphi). Then, \varphi should be a theorem iff \forall w. \textsf{ksat}(w, \varphi) is a theorem of intuitionistic first-order logic.

References

@phdthesis{simpson_1994,
	type = {{PhD} {Thesis}},
	title = {The {Proof} {Theory} and {Semantics} of {Intuitionistic} {Modal} {Logic}},
	url = {http://hdl.handle.net/1842/407},
	school = {The University of Edinburgh},
	author = {Simpson, Alex K.},
	year = {1994},
}