Event Detail

In classical modal logic, necessity []A, possibility <>A, impossibility []~A and non-necessity <>~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 [~] and impossibility <~>, first investigated by Došen, have received less attention and — together with their positive counterparts [] and <> — form a square we call the Došen Square. Unfortunately, the core property of constructive logic, the Disjunction Property (DP), fails when the modalities are combined and, interpreted in birelational Kripke structures à la Došen, the Square partially collapses. We introduce the constructive logic CKD, whose four semantically independent modalities [], <>, [~], <~> prevent the Došen 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[~], HK[], HK<> and HK<~> of Došen and other known theories of intuitionistic modalities are syntactic fragments or axiomatic extensions of CKD.