 But the expressivity comes with a cost. As usual in multi-modal systems, the crucial question is the interaction between the involved modalities, and in this case, the discussion typically centers on the following two: the Barcan formula, \(\forall x \oBox Px \rightarrow \oBox\forall x Px\), and its converse, \(\oBox\forall x Px \rightarrow \forall x \oBox Px\) (see Barcan 1946). The reason for the controversy becomes clear when the generic predicate P is replaced by, say, the formula \(\exists x (x=y)\), which can be read as “x exists”. Then, the first formula becomes