I am trying to understand a modal logic countermodel, illustrating that the QK theorem, $$ \Box (\phi(x) \wedge \forall x \phi (x)) \rightarrow \Box \forall x \phi (x), $$ fails in the alternate semantics for modal logic given by David Lewis's counterpart theory. The countermodel is the following:
It comes from Oliver Kutz's Kripke-Typ Semantiken für die modale Prädikatenlogik , p. 31. I don't understand German, but based on what I could glean from context and Google Translate it doesn't seem like the diagram is explained at all.
Here's what I do understand:
The large circles represent the two worlds, $w_1$ and $w_2$.
The smaller dotted circles, which I would prefer to be loops, indicate that $C (u_1, u_1)$ and $C (u_2, u_2)$ (where $C$ is the "counterpart relation").
At the bottom of each circle is an indication that $\phi/\lnot \phi$ hold of $u_1/u_2$ in their respective worlds.
What I don't get are the dotted arcs. Based on context I believe the quantifiers below the arcs are quantifiers over worlds. This makes sense because the original presentation of counterpart theory utilized a translation procedure to link statements of quantified modal logic to statements in the two-sorted (worlds and individuals) framework of counterpart theory. So, e.g., the formula $\Box \phi (x)$ gets translated as $$\forall v \forall y [W (v) \wedge I (y, v) \wedge C (y, x) \rightarrow \phi^v (y)],$$ which is read as "for every world $v$ if $y$ inhabits $v$ and $y$ is a counterpart of $x$ then $\phi$ is true of $y$ in $v$". Similarly, a statement like $\Diamond \phi (x)$ gets translated as $$\exists v \exists y (W (v) \wedge I (y, v) \wedge C (y, x) \wedge \phi^v (b)).$$
As a result there are various completion I could imagine to the quantification over worlds. It will be true that there is some world where $\exists x \lnot \phi (x)$ is true, namely $w_2$, and so $\Diamond \exists x \lnot \phi (x)$ is true in $w_1$ (and therefore $\lnot \Box \forall x \phi (x)$ is also true in $w_1$, falsifying the consequent of the conditional).
Additionally, both $\phi (x)$ and $\forall x \phi (x)$ are true in $w_1$ since the only counterpart of $u_1$ is itself it also follows that $\Box (\phi (x) \wedge \forall x \phi (x))$ is true in $w_1$. From this and the preceding we have that the conditional QK theorem is false at $w_1$ in this counterpart theory model.
So obviously there is some quantification over worlds in the box and diamond statements, but I can't quite figure out what sort of a relationship the dotted arcs are attempting to indicate.
Any help would be appreciated.