Dynamic Modalities

A new modal logic containing four dynamic modalities with the following informal reading is introduced: ${square^forall}$ – always necessary, ${square^exists}$ – sometimes necessary, and their duals – ${diamondsuit^forall}$ – always possibly, and ${diamondsuit^exists}$ – sometimes possibly. We present a complete axiomatization with respect to the intended formal semantics and prove decidability via fmp.