Show that the drinking principle is not intuitionistic The drinking principle, namely 
$$ \exists x (p(x) \rightarrow \forall y p(y)) ,$$
aka the drinker paradox, can be infered using the rules of classical logic. 
Is it possible to intuitionistically infer a formula which is not intuitionistically inferrable (such as $\lnot F \lor \lnot\lnot F$ or $\lnot F \lor F$ or $\lnot\lnot F \rightarrow F$ or $\lnot \exists x \lnot F \rightarrow \forall x F$ ...) from the drinking principle?
If  not, how do you prove it can't be inferred with the intuitionistic rules?
 A: The drinker principle is not so strong that assuming it as an axiom will in itself yield classical logic.
One argument for this is that if $\varphi$ does not contain $x$ free, then $\varphi \to (\forall x)\varphi$ is intuitionistically valid. In particular, the drinker principle itself is intuitionistically valid in the special case where $p(x)$ does not mention $x$.
Thus, suppose that intuitionistic first-order logic plus Drinker proves $p\lor \neg p$ where $p$ is a nullary predicate letter. Take the supposed proof and replace every atomic formula other than $p$ by $\top$ everywhere in the proof. This replacement both preserves all inference rules, and all axioms are still provable after the replacement (equality axioms become things like $\top\to\top$ or $\top\to\top\to\top$, which need short proofs of themselves now).  Since there are no terms anywhere anymore, every instance of the Drinker axiom becomes $(\exists x)(\psi\to(\forall x)\psi)$ where $\psi$ does not contain $x$, which is provable without the Drinker axiom. Thus, we can construct a pure intuitionistic proof of $p\lor\neg p$ (which was not affected by the replacement) -- and this is known to be impossible.

To show that Drinker is not itself intuitionisticaly valid, we can show a Kripke model where it is false.
The worlds are $w_0$, $w_1$, $w_2$ with $w_0<w_1$ and $w_0<w_2$, the domain is $\{1,2\}$ everywhere, and
$$ w_1\Vdash p(1) \qquad w_2\Vdash p(2) $$
Then $(\forall x)p(x)$ is false everywhere. So $p(1)\to(\forall x)p(x)$ is false in $w_1$ and $p(2)\to(\forall x)p(x)$ is false in $w_2$, and both of these are false in $w_0$. So there cannot be any witness of $p(x)\to(\forall x)p(x)$ in $w_0$, so the Drinker applied to $p$ is false in $w_0$.
