Multimodal logic

A multimodal logic is a modal logic that has more than one primitive modal operator. They find substantial applications in theoretical computer science.

A modal logic with n primitive unary modal operators ${\displaystyle \Box _{i},i\in \{1,\ldots ,n\}}$ is called an n-modal logic. Given these operators and negation, one can always add ${\displaystyle \Diamond _{i}}$ modal operators defined as ${\displaystyle \Diamond _{i}P}$ if and only if ${\displaystyle \lnot \Box _{i}\lnot P}$.

...
Wikipedia