Does $\forall x (\phi(x) \vee \neg \phi(x))$ imply (2) $\forall x \phi (x) \vee \neg \forall x \phi(x)$ in intuitionistic logic? Does (1) $\forall x (\phi(x) \vee \neg \phi(x))$ imply (2) $\forall x \phi (x) \vee \neg \forall x \phi(x)$ in intuitionistic logic?
It seems to me that it does not, and my heuristic is this: (1) "says" that we have an algorithm that shows, for every object, that it is $\phi$ or not $\phi$. (2) "says" that either we have an algorithm that shows that every object is $\phi$, or we don't have it. (1) doesn't give us such an algorithm, nor does it show that there is no such thing, so it does not entail (2).
But, unless am I simply mistaken, the question is: how to show this more formally?
 A: Usually, the way to show that an implication does not hold is to give a countermodel.
This requires some notion of semantics. There are a few ways to give semantics to intuitionistic first-order logic, but the simplest is probably Kripke semantics.
It will suffice to find a countermodel to $\forall x\,(P(x)\lor \lnot P(x))\models \forall x\,P(x)\lor \lnot \forall x\, P(x)$, where $P$ is a unary relation symbol. That is, we want to find a Kripke model $M$ and a world $w$ in $M$ such that $w\models \forall x\,(P(x)\lor \lnot P(x))$ but $w\not\models \forall x\,P(x)\lor \lnot \forall x\, P(x)$.
The meaning of the first sentence is: for all worlds $w'\geq w$ and elements $x\in D(w')$, we have that $P$ holds of $x$, or for all worlds $w''\geq w'$, $P$ does not hold of $x$. Part of the definition of Kripke model is that if $P$ holds of $x$ in $w'$, then for all worlds $w''\geq w'$, $P$ holds of $x$. So $P$ cannot switch from "on" to "off", and this sentence says additionally that $P$ cannot switch from "off" to "on".  So intuitively, this says that the truth value of $P$ never switches.
The meaning of the second sentence is: Either it's true that for all $w'\geq w$ and  elements $x\in D(w')$, $P$ holds of $x$, or it's true that for all $w'\geq w$, there exists $w''\geq w'$ and an element $x\in D(w'')$ such that $P$ does not hold of $x$. Intuitively, either $P$ holds of everything in sight, or counterexamples to $P$ are "dense".
To get the second sentence to fail, we need:
(1) There exists $w'\geq w$ and $x\in D(w')$ such that $P$ does not hold of $x$, and  (2) there exists $w'\geq w$ such that for all $w''\geq w$ and all $x\in D(w'')$, $P$ holds of $x$.
Ok, now we can construct our countermodel. Let $W = \{w,w_1,w_2\}$ with $w\leq w_1$, $w\leq w_2$, and $w_1,w_2$ incomparable. Let $D(w) = D(w_2) = \{a\}$ and $D(w_1) = \{a,b\}$, with $P = \{a\}$ in all three worlds.
The truth value of $P$ never switches on an element, so $w\models \forall x\,(P(x)\lor \lnot P(x))$. The world $w_1\geq w$ witnesses condition (1), since $P$ does not hold of $b\in D(w_1)$, and the world $w_2\geq w$ witnesses condition (2), since $P$ holds of all elements of all worlds $\geq w_2$. So $w\not\models \forall x\,P(x)\lor \lnot \forall x\, P(x)$.
