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