 Note that the binder \(\mathtt{\downarrow}\) is definable in terms of \(\mathtt{\forall}\) as the formula \(\mathtt{{\downarrow} a\phi \leftrightarrow \forall a(a \rightarrow \phi)}\) is valid in any frame.