Help with modal logic countermodel 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.  
 A: You are correct about your assumptions so far and that the paragraph doesn't contain any explicit explanation of the dotted arrows. I'm not familiar with counterpart theory in particular so am not entirely certain about it either, but I think the explanation lies in the last paragraph of the subchapter, which translates as follows:

Note that in the last case [(ii) following from the assumption $\mathcal{M} \vDash \neg \phi^{w_2}$], no conditions on the existence of counterparts are imposed, since the formula $\neg \Box \forall x \phi(x)$ contains no free variables. Indeed, this is the source of of the failure of box distribution. For note that due to the double quantification $\forall v \forall y \ldots$ over worlds and objects, subformulas of a formula $\psi$ of the form $\Diamond \chi(\overline{z})$, depending on which free variables $\overline{z}$ they contain, are evaluated in multiple possible worlds. In particular, a sentence of the form $\Box \phi$ is evaluated in all possible worlds, without restrictions in terms of an accessibility relation on the set of possible worlds taking effect. [...]

I therefore believe that $\forall v \ldots$ is the translation of the formula (i), and $\exists v \ldots$ is a translation of the formula (ii), and the dotted arcs indicate that the formulas are evaluated in all possible worlds $w_1, w_2$ disregarding constraints on accessibility, since they contain no free variables.
Does this explanation make sense?
