# Events

September 25, 2024, 6-7:30 PM **(note special time)** in
234 Philosophy

*Michael Mendler and Luke Burke (Otto-Friedrich University of
Bamberg)*

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

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.