Is $\forall x \square \varphi \leftrightarrow \square \forall x \varphi$ a valid formula for all formulas $\varphi$? I haven't yet studied formal semantics of a modal logic with quantifiers, so forgive me if I make any rookie mistakes.
My thinking goes like this. The modal quantifier $\square$ ranges over the set of all possible worlds $\mathbf{W}$. $(\to)$ Let $\forall x \square \varphi$. This means that in the actual world $w_A$, $\varphi$ holds necessarily for all $x$, which means that $\varphi$ holds for all $x$ in every other world. But this just means $\square \forall x \varphi$. $(\leftarrow)$ Let $\square \forall x \varphi$. This means that $\forall x \varphi$ holds in every world, which means that $\varphi$ holds for all $x$ in every world, including the actual world $w_A$, which means that $\varphi$ holds necessarily (i.e., in every other world as well) in the actual world for all $x$. This means $\forall x \square \varphi$.
This also seems to hold if $\mathbf{W}$ is empty, if we define $\emptyset \models \square \psi$ for all formulas $\psi$, which seems similar to how $\forall$ works on empty domains in FOL.
Is my thinking correct? Let me know. :)
 A: The formula you mention is equivalent to the conjunction of the Barcan and the converse Barcan formula. The Barcan formula defines the class of variable domain frames which are anti-monotonic, in the sense that in accessible worlds no new things can come into existence . The converse Barcan formula defines the class of frames which are monotonic in the sense that in accessible worlds things cannot pass out of existence. Taken together these formulas define the class of frames, where worlds related by accessibility relations have the same domain. I'll illustrate these claims by showing that the Barcan formula defines the anti-monotonic frames.
Let a variable domain frame on a set $D$ be a tuple $F=(W, R, d)$, where $(W, R)$ is a relational structure as in propositional modal logic and $d$ is a function from $W$ to subsets of $D$. A variable domain model on a frame is a pair consisting of the frame and an interpretation function. The satisfaction clauses treat first-order quantifiers so that, at a point $w$ of the model, they only range over $d(w)$. Validity $\varphi$ in a frame $F$ ($F \models \varphi$) is defined as usual.
Let a variable domain frame be anti-monotonic, if for every $w, v \in W$ it holds that

*

*$wRv \Rightarrow d(v) \subseteq d(w)$
It is straightforward to show that for any variable domain frame $F$:

*

*$F$ is anti-monotonic iff $F \models \forall x \Box \varphi \rightarrow \Box \forall x \varphi$
To see that let $F$ be anti-monotonic, $M =(F, I), w, g \models \forall x \Box \varphi wRv$ and $a \in d(v)$. So, $a \in d(w)$ and thus $M, v, g\frac{a}{x} \models \varphi$ and we are done.
For the other direction assume that there are $w, v \in W$ with $wRv$ and  $ u \in d(v) \setminus d(w)$, for some $u \in D$. Let $I$ be defined on a 1-place predicate $P$ such that $I(P)(z) = d(w)$, for any $z \in W$. Then it is trivial that $(F, I), w, g \models \forall x \Box Px$. But since $u \not \in d(w) = I(P)(v)$ we have that $(F,I), v ,g \not \models \forall x Px$ and so $(F,I), w, g \not \models \Box \forall x Px$.
