  In the 1970s, a version of bisimulation had already been developed by modal logicians to help better understand the relationship between modal logic axioms and their corresponding conditions on Kripke frames. Kripke’s semantics provides a basis for translating modal axioms into sentences of a second-order language where quantification is allowed over one-place predicate letters \(P\). Replace metavariables \(A\) with open sentences \(Px\), translate \(\Box Px\) to \(\forall y(Rxy \rightarrow Py)\), and close free variables \(x\) and predicate letters \(P\) with universal quantifiers. For example, the predicate logic translation of the axiom schema \(\Box A\rightarrow A\) comes to \(\forall P \forall x[\forall y(Rxy\rightarrow Py) \rightarrow Px\)]. Given this translation, one may instantiate the variable \(P\) to an arbitrary one-place predicate, for example to the predicate \(Rx\) whose extension is the set of all worlds w such that \(Rxw\) for a given value of \(x\). Then one obtains \(\forall x[\forall y(Rxy\rightarrow Rxy) \rightarrow Rxx\)], which reduces to \(\forall xRxx\), since \(\forall y(Rxy\rightarrow Rxy)\) is a tautology. This illuminates the correspondence between \(\Box A\rightarrow A\) and reflexivity of frames \((\forall xRxx)\). Similar results hold for many other axioms and frame conditions. The “collapse” of second-order axiom conditions to first order frame conditions is very helpful in obtaining completeness results for modal logics. For example, this is the core idea behind the elegant results of Sahlqvist (1975).