Normal Companions of Intuitionistic Modal Logics

Previously, Dosen and Bozic introduced four independent intuitionistic modal logics, one for each of four types of modal operators-necessity N, possibility P, impossibility Im, and unnecessity Un. These logics are denoted HKM, where M is an element of {N, P, Un, Im}. Interest in treating the four types of modal operators separately is associated with just the fact that these cannot be reduced to each other over intuitionistic logic. Here we study extensions of logics HKM that have normal companions. It turns out that all extensions of the logics HKN and HKUn possess normal companions. For the extensions of HKP and HKIm, we obtain a criterion for the existence of normal companions, which is postulated as the presence of some modal law of double negation. Also we show how adding of this law influences expressive capacities of a logic. Of particular interest is the result saying that extensions of HKP and HKIm have normal companions only if they are definitionally equivalent to those of HKN and HKUn respectively. This result is one more example of the differences in behavior of the four types of modal operators over intuitionistic logic.

Automated summary

This article studies the extensions of four independent intuitionistic modal logics, finding that the extensions of HKN and HKUn have normal companions, while the extensions of HKP and HKIm have normal companions only if they satisfy a certain law of double negation, and the addition of this law affects the expressive capacities of the logic. It is noteworthy that the extensions of HKP and HKIm have normal companions only if they are definitionally equivalent to the extensions of HKN and HKUn, respectively.