The Dosen Square Under Construction: A Tale of Four Modalities

In classical modal logic, necessity square A, possibility lozenge A, impossibility square(sic)A and non-necessity lozenge(sic)A form a Square of Oppositions (SO) whose corners are interdefinable using classical negation. The relationship between these modalities in intuitionistic modal logic is a more delicate matter since negation is weaker. Intuitionistic non-necessity (sic) and impossibility (sic), first investigated by Dosen, have received less attention and-together with their positive counterparts square and lozenge-form a square we call the Dosen Square. Unfortunately, the core property of constructive logic, the Disjunction Property (DP), fails when the modalities are combined and, interpreted in birelational Kripke structures a la Dosen, the Square partially collapses. We introduce the constructive logic CKD, whose four semantically independent modalities. square, lozenge, (sic) prevent the Do.sen Square from collapsing under the effect of intuitionistic negation while preserving DP. The model theory of CKD involves a constructive Kripke frame interpretation of the modalities. A Hilbert deduction system and an equivalent cut-free sequent calculus are presented. Soundness, completeness and finite model property are proven, implying that CKD is decidable. The logics HK(sic), HK square, HK lozenge and HK(sic) of Dosen and other known theories of intuitionistic modalities are syntactic fragments or axiomatic extensions of CKD.