 Beside nominals and satisfaction operators, in what follows we shall consider the so-called binders \(\mathtt{\forall}\) and \(\mathtt{\downarrow}\) allowing us to build formulas \(\mathtt{\forall a \phi}\) and \(\mathtt{{\downarrow} a \phi}\). The binders bind nominals to points in two different ways: The \(\mathtt{\forall}\) binder quantifies over points analogous to the standard first-order universal quantifier, that is, \(\mathtt{\forall a \phi}\) is true relative to \(w\) if and only if whatever point the nominal \(\mathtt{a}\) refers to, it is the case that \(\mathtt{\phi}\) is true relative to \(w\). The \(\mathtt{\downarrow}\) binder binds a nominal to the point of evaluation, that is, \(\mathtt{{\downarrow} a \phi}\) is true relative to \(w\) if and only if \(\mathtt{\phi}\) is true relative to \(w\) when \(\mathtt{a}\) refers to \(w\). It turns out that the \(\mathtt{\downarrow}\) binder is definable in terms of \(\mathtt{\forall}\) (as shown below).