  But when does the second-order translation of an axiom reduce to a first-order condition on \(R\) in this way? In the 1970s, van Benthem showed that this happens iff the translation’s holding in a model entails its holding in any bisimular model, where two models are bisimular iff there is a bisimulation between them in the special case where there is a single accessibility relation. That result generalizes easily to the poly-modal case (Blackburn et. al., 2001, p. 103).  This suggests that poly-modal logic lies at exactly the right level of abstraction to describe, and reason about, computation and other processes. (After all, what really matters there is the preservation of truth values of formulas in models rather than the finer details of the frame structures.) Furthermore the implicit translation of those logics into well-understood fragments of predicate logic provides a wealth of information of interest to computer scientists. As a result, a fruitful area of research in computer science has developed with bisimulation as its core idea (Ponse et al. 1995).