The Došen Square under construction: A tale of four modalities

In classical modal logic, necessity $\Box A$, possibility $\Diamond A$, impossibility $\Box \neg A$ and non-necessity $\Diamond \neg 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 $\overline{\Box}$ and impossibility $\overline{\Diamond}$, first investigated by Došen, have received less attention and—together with their positive counterparts $\Box$ and $\Diamond$—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 $\mathsf{CKD}$, whose four semantically independent modalities $\Box$, $\Diamond$, $\overline{\Box}$, $\overline{\Diamond}$ prevent the Došen Square from collapsing under the effect of intuitionistic negation while preserving DP. The model theory of $\mathsf{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 $\mathsf{CKD}$ is decidable. The logics $\mathsf{HK} \overline{\Box}$, $\mathsf{HK} \Box$, $\mathsf{HK} \Diamond$ and $\mathsf{HK} \overline{\Diamond}$ of Došen and other known theories of intuitionistic modalities are syntactic fragments or axiomatic extensions of $\mathsf{CKD}$.

This is joint work with Luke Burke and Stephan Scheele.