De re/dicto knowledge Define $\mathcal{K}$ as a knowledge operator characterized by a S4 modal system. There is a distinction between de re and de dicto expressions of knowledge:

*

*$\exists x\mathcal{K}A(x)$ is a de re expression of knowledge: there exists $x$ such that the agent knows $A(x)$.

*$\mathcal{K}\exists xA(x)$ is a de dicto expression of knowledge: the agent knows that there exists $x$ such that $A(x)$.

As is usually assumed in the literature, de re knowledge entails de dicto knowledge (but usually not the other way around):
$$\exists x\mathcal{K}A(x)\rightarrow\mathcal{K}\exists xA(x)\tag{$*$}$$
My question is the following: given the above definitions and $(*)$, can we prove $(**)$?
$$\mathcal{K}(\exists xA(x)\rightarrow\exists yB(y))\rightarrow(\exists x\mathcal{K}A(x)\rightarrow\exists y\mathcal{K}B(y))\tag{$**$}$$
I tried to use the distribution axiom for $\mathcal{K}$ which is available from the S4 system, but I cannot see how to proceed. Can anyone help? Is $(**)$ provable or not?
 A: 
given the above... can we prove $(**)$?

No, nor can we prove its negation.
Here are the countermodels, generated using this tool, courtesy of one Wolfgang Schwarz:
Let $W$ be the set of worlds, $D$ the set of individuals, $R$ the accessibility relation on $W$, and $A'$ and $B'$ the interpretations of the relation symbols $A$ and $B$, respectively.
Then, for
$$\begin{array}
\ W=\{w_0,w_1\}\\
D = \{0,1\}\\
A'=\{(0,w_0),(0,w_1)\}\\
B'=\{(1,w_0),(0,w_1)\}\\
R = W\times W
\end{array}$$
we have $w_0\Vdash\neg(**)$, and for
$$\begin{array}
\ W=\{w_0\}\\
D = \{0\}\\
A'=\{(0,w_0)\}\\
B'=\{(0,w_0)\}\\
R = W\times W
\end{array}$$
we have $w_1\Vdash(**)$.
However, $(**)$ is provable with the addition of the Buridan formula ($\mathsf{BuF}$) to the axioms. Here is the proof:
$$\def\knows{\mathcal K}
\begin{array}
\ 1. & \knows\exists xAx\to\exists x\knows Ax &\mathsf{BuF}\\
2. & \knows\exists yBy\to\exists y\knows By & \mathsf{BuF}\\
3. & \knows(\exists xAx\to\exists yBy)\to(\knows\exists xAx\to\knows\exists yBy) & \mathsf{K}\\
4. & \quad \knows(\exists xAx\to\exists yBy) & \text{assumption}\\
5. & \quad \knows\exists xAx\to\knows\exists yBy &\mathsf{MP}\ 3,4\\
6. & \quad \quad \knows\exists x Ax &\text{assumption}\\
7. & \quad \quad \knows\exists yBy &\mathsf{MP}\ 5,6\\
8. & \quad \quad\exists y\knows By &\mathsf{MP}\ 2,7\\
9. & \quad \knows \exists x Ax\to\exists y\knows By & \mathsf{DT}\ 6-8\\
10. & \quad \exists x\knows Ax\to\knows\exists xAx & (*)\\
11. & \quad \quad \exists x\knows Ax & \text{assumption}\\
12. & \quad \quad \knows\exists x Ax & \mathsf{MP}\ 10,11\\
13. & \quad \quad\exists y\knows By & \mathsf{MP}\ 9,13\\
14. & \quad\exists x\knows Ax\to\exists y\knows By & \mathsf{DT}\ 11-13\\
15. & \knows(\exists xAx\to\knows\exists yBy)\to(\exists x\knows Ax\to\exists y\knows By) & \mathsf{DT}\ 4-14
\end{array}$$
A: 
I tried to use the distribution axiom for K which is available from the S4 system, but I cannot see how to proceed.

No.  It does not seem doable.
$$\def\fitch#1#2{~~~\begin{array}{|l}#1\\\hline#2\end{array}}\def\knows{\mathcal K}\fitch{\exists x~\knows Ax\to\knows\exists x~Ax}{\fitch{\knows(\exists x~Ax\to\exists y~ By)}{\knows\exists x~Ax\to\knows\exists y~By\qquad\textsf{K distibution}\\\fitch{\exists x~\knows Ax}{\knows\exists x~Ax\qquad\to\mathsf E\\\knows\exists y~By\qquad\to\mathsf E\\~~~\vdots\\\exists y~\knows By\qquad\textsf{.... how?}}\\(\exists x~\knows Ax)\to(\exists y~\knows By)}\\(\knows(\exists x~Ax\to\exists y~By ))\to((\exists x~\knows Ax)\to(\exists y~\knows By))}$$
Using Krippke semantics for S4 (reflexive and transitive many worlds), it does not seem that each accessible world having something satisfying $B$ would entail the existence of a single thing that does so in every accessible world.
