On Wikipedia, the first Axiom of Gödel's ontological proof is $$(P(\phi)\land\square\forall x(\phi(x)\Rightarrow\psi(x)))\Rightarrow P(\psi),$$ I assume there are implicit quantifiers present for $\phi$ and $\psi$. Also I assume Gödel used the possible worlds semantics of higher order modal logic since his proof dates back to 1941 and Kripke semantics appeared in the late 1950s, according to Wikipedia.
I don't get how the box here actually adds some meaning. As far as I found out, the two prevailing interpretations of higher order modal logic are constant domain models and varying domain models. Since varying domain models incorporate constant domain models, I'll just argue about the latter here.
So let's say we start in world $\Gamma\in\mathcal{G}$ of a particular model $\mathcal{M}=(\mathcal{G},\mathcal{D},\mathcal{I})$ under valuation $v$. The implicit quantifiers fix $\phi$ and $\psi$ as relations in the domain of $\Gamma$, i.e. $v(\phi),v(\psi)\subseteq\mathcal{D}(\Gamma)$. Now $\forall x(\phi(x)\Rightarrow\psi(x))$ evaluates to true if and only if $\forall u\in\mathcal{D}(\Gamma)(v(\phi)(u)\Rightarrow v(\psi)(u))$ or, in other words, $v(\phi)\subseteq v(\psi)$. But $\square\forall x(\phi(x)\Rightarrow\psi(x))$ would just possibly throw in some new elements $u$ from the domains of other worlds, which are not contained in $\mathcal{D}(\Gamma)$, hence also not contained in $v(\phi)$ or $v(\psi)$, so the new formula wouldn't evaluate to something different as the old, 'local' one, it seems to me.