 and the \(\Box\) gets resolved as described above. The above choice of \(\Pi'\) realizes a possibilist notion of quantification. By introducing a binary “existence” predicate in the meta-logic and by utilizing this predicate as an additional guard in the definition of \(\Pi'\) an actualist notion of quantification can be obtained. Expressing that an embedded modal formula \(\varphi_{{o}\imath}\) is globally valid is then captured by the formula \(\forall x_{\imath} [\varphi_{{o}\imath} x_{\imath}]\). Local validity (and also actuality) can be modeled as \(\varphi_{{o}\imath} n_{\imath}\), where \(n_{\imath}\) is a nominal (constant symbol in the meta-logic) denoting a particular possible world.