 Similarly, what is called the bounded fragment of first-order logic can be translated into the hybrid logic but here only the binder \(\mathtt{\downarrow}\) is needed, as pointed out in the paper Areces, Blackburn, and Marx (2001). The bounded fragment is the fragment of first-order logic with the property that quantifiers only occur as in the formula \(\mathtt{\forall c(R(a, c) \rightarrow \phi)}\), where it is required that the variables \(\mathtt{a}\) and \(\mathtt{c}\) are different. A translation from the bounded fragment to the hybrid logic without the \(\mathtt{\forall}\) binder can be obtained by replacing the last clause in the translation HT above by