In intuitionistic FOL, does $\forall x \forall y (P(x) \lor Q(y))$ imply $(\forall x, P(x)) \lor (\forall y, Q(y))$? Of course, in classical logic, if you have $\forall x \forall y (P(x) \lor Q(y))$, then you can conclude $(\forall x, P(x)) \lor (\forall y, Q(y))$: if you didn't have that, then there would be $x$ such that $\lnot P(x)$ and $y$ such that $\lnot Q(y)$, and then that contradicts the assumption.
On the other hand, in intuitionistic logic, I don't think that necessarily holds.  My counterexample is to work in the topos of sheaves on $\mathbb{R}$, let the domain of discourse be $\mathbb{N}^+$, and define $P(n) := (-\infty, \frac{1}{n})$ and $Q(n) := (-\frac{1}{n}, \infty)$.  Then for any $m, n \in \mathbb{N}^+$, $P(m) \cup Q(n) = \mathbb{R}$, so the hypothesis should also be valid for any locally constant functions $m, n : U \to \mathbb{N}^+$, i.e. sections of the constant sheaf $\mathbb{N}^+$.  On the other hand, $\bigcap_m P(m) = (-\infty, 0)$ and $\bigcap_n Q(n) = (0, \infty)$, and the union of those two is $\mathbb{R} \setminus \{ 0 \}$.
So, my question is to verify that this is a correct solution and I didn't miss anything silly.  I would also be interested to see whether a counterexample could be constructed in terms of a Kripke frame, where no example immediately comes to mind for me.
 A: Your logic appears sound.
Another approach is as follows. We work in constructive set theory. Fix a one-element set $1$ and a proposition $P$. Define $P(x) = P$ and $Q(x) = \neg P$.
Consider $S = \{x \in 1 \mid P \lor \neg P\}$. Then $\forall x, y \in S, P(x) \lor Q(y)$. However, if we have $\forall x \in S (P(x))$, then we have $\neg \neg P$. And if we have $\forall y \in S (Q(y))$, then we have $\neg P$. So to assert $(\forall x \in S P(x)) \lor (\forall y \in S Q(y))$ is precisely to assert $\neg P \lor \neg \neg P$. Since $\neg P \lor \neg \neg P$ is not a constructive tautology, we have demonstrated that OP’s implication is not a constructive tautology.
If you want a specific Kripke frame where this fails, you can start with a Kripke frame where $\neg \neg P \lor \neg P$ fails for some $P$, and then trace backwards along my proof. One example involves a 3-element frame with elements $a, b, c$, where the relation is $x \leq y$ precisely when $x = c$. We then define $P$ to hold only at $b$. Then $\neg P$ cannot hold at $c$, since $P$ holds at $b \geq c$. Similarly, $\neg \neg P$ cannot hold at $c$, since $\neg P$ holds at $a \geq c$. Thus, $\neg \neg P \lor \neg P$ doesn’t hold at $c$.
We take $S(a) = 1 = S(b)$ and $S(c) = \emptyset$. We define $P(x)$ to hold at $b$ and fail at $a$, and we define $Q(x)$ to hold at $a$ and fail at $b$. Then we indeed have $\forall x \forall y (P(x) \lor Q(y))$ in our Kripke model, since once we have an $x$ and a $y$, we must be at stage $a$ or $b$. But at stage $c$, we don’t have either $\forall x P(x)$ or $\forall y Q(y)$.
Note that we defined $S, P(x), Q(x)$ in the preceding paragraph by following my constructive set theory construction in the presheaf topos corresponding to the Kripke frame. Kripke models are just models in the internal logic of a topos of presheaves on a poset.
