 The second relevant result is the Modal Characterization  Theorem[14]  establishing, for any first-order formula with a free variable, the equivalence between being equivalent to a modal formula and being invariant under bisimulation (see van Benthem 2010: 26–27 for a definition). Bisimulation is a useful result as it can be employed to make a model \(\mathcal{A}\) as small as possible, by bisimulation constraction, as well as to make bigger models.