 The Future Barcan  Formula[7]  scheme, \(\mathsf{BF}_{G}\), is CD-valid:  \(\models_{\mathrm{CD}} \forall x G \varphi(x) \to G \forall x \varphi(x)\) or, equivalently,   \(\models_{\mathrm{CD}} F \exists x \varphi(x) \to \exists x F \varphi(x)\).