Understanding The First Axiom Of Gödel's Ontological Proof

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.

• Yes; it is high-order modal logic, because properties : $\varphi, \psi$ are quantified; see e.g. Def.1. – Mauro ALLEGRANZA Jun 7 '18 at 12:48
• The necessity operator is needed in order to derive Th.1 from Ax.1. Th1. says : "Any positive property is possibly instantiated. That is, if $\varphi$ is positive, it is possible that something has property $\varphi$." – Mauro ALLEGRANZA Jun 7 '18 at 12:57
• Maybe useful : Melvin Fitting, Types, Tableaus, and Gödel's God, Kluwer (2002). – Mauro ALLEGRANZA Jun 7 '18 at 12:59
• The difference between $(\forall x) \Theta(x)$ and $\Box (\forall x) \Theta(x)$ is that the former is only an assertion about the current world, while the latter is an assertion about all the worlds that extend the current world. The notation in the question takes a while to digest, but it must be that one of these two is being confused for the other. – Carl Mummert Jun 7 '18 at 13:52
• Thank you for the comments! I started with this thing and there is no word about intensional / extensional properties. Now I read into the book @MauroALLEGRANZA recommended and there it all makes sense. – fweth Jun 8 '18 at 10:29