 The language we consider is the language of ordinary modal logic built over ordinary propositional symbols \(\mathtt{p}, \mathtt{q}, \mathtt{r}, …\) as well as nominals \(\mathtt{a}, \mathtt{b}, \mathtt{c}, …\) and extended with satisfaction operators and binders. We take the propositional connectives \(\mathtt{\wedge}\) and \(\mathtt{\neg}\) to be primitive; other propositional connectives are defined as usual. Similarly, we take the modal operator \(\mathtt{\Box}\) to be primitive and define the modal operator \(\mathtt{\Diamond}\) as \(\mathtt{\neg \Box \neg}\). As the name suggests, binders bind nominals and the notions of free and bound occurrences of nominals are defined analogously to first-order logic. Satisfaction operators do not bind nominals, that is, the free nominal occurrences in a formula \(\mathtt{@_a \phi}\) are the free nominal occurrences in \(\mathtt{\phi}\) together with the occurrence of \(\mathtt{a}\). We let \(\mathtt{\phi[c/a]}\) be the formula \(\mathtt{\phi}\) where the nominal \(\mathtt{c}\) has been substituted for all free occurrences of the nominal \(\mathtt{a}\). If the nominal \(\mathtt{a}\) occurs free in \(\mathtt{\phi}\) within the scope of \(\mathtt{\forall c}\) or \(\mathtt{{\downarrow} c}\), then the bound nominal \(\mathtt{c}\) in \(\mathtt{\phi}\) is renamed as appropriate.