 The translations given above are truth-preserving. To state this formally, one makes use of the well-known observation that models and assignments for hybrid logic can be considered as models and assignments for first-order logic and vice versa. These truth-preservation results are straightforward to formulate and we leave the details to the reader. Thus, the hybrid logic with the binder \(\mathtt{\forall}\) has the same expressive power as first-order logic with equality and the hybrid logic without the binder \(\mathtt{\forall}\) (but with the binder \(\mathtt{\downarrow}\)) has the same expressive power as the bounded fragment of first-order logic (note that the translation \(\mathrm{ST}_\mathtt{a} (\mathtt{\phi})\) of any formula \(\mathtt{\phi}\) without the binder \(\mathtt{\forall}\) is in the bounded fragment).