If I'm not mistaken, Kripke semantics work for the drinker's theorem !So I'm writing this answer to close this question but also in the hope that someone will take a look at it and tell me if I've made any mistakes.
Let me modify them slightly by allowing quantifiers in the following way :
Let $L$ be a relational language, $L=\{R_i, i\in I\}$ ($R_i$ is $n_i$-ary)
Consider $\mathcal{D}$ a set, and $\mathbb{P} = (P,\leq)$ a poset. An interpretation $\mathcal{M}$ for $L$ with individual set $\mathcal{D}$ in $\mathbb{P}$ consists in the data of upwards-closed sets $[| R_i(a_1,...,a_{n_i})|]$ for each $i\in I$ and $(a_1,...,a_{n_i})\in \mathcal{D}^{n_i}$.
For a formula $\varphi(a_1,...,a_n)$ with parameters in $\mathcal{D}$ (one should probably do it with free variables first and use assignments, but since this is not for publication or anything, I'll just skip this step), and $p\in P$ one defines $\mathcal{M}\models_p \varphi(a_1,...,a_n)$ the usual way by induction, the steps where it differs from classical logic are the base case, $\neg$ and $\implies$ : $\mathcal{M}\models_p R_i(a_1,...,a_{n_i})$ is defined as $p\in [|R_i(a_1,...,a_{n_i})|]$; $\mathcal{M}\models_p \neg\varphi(a_1,...,a_n)$ as $\forall q\geq p, \neg (\mathcal{M}\models_q \varphi(a_1,...,a_n))$; and $\implies$ similarly.
One then defines $\mathcal{M}\models \varphi(a_1,...,a_n)$ as "for all $p$, $\mathcal{M}\models_p \varphi(a_1,...,a_n)$".
One can finally define the relation $\Gamma \models_p \phi$, for $\Gamma$ a multiset of formulas, $\phi$ a formula, as "for all interpretations $\mathcal{M}$ of $L$ in $\mathbb{P}$ and all assignments of the free variables to elements of the individual set such that $\mathcal{M}\models_p \Gamma$, $\mathcal{M}\models_p \phi$".
One can then check that for all $p\in P$, $\vdash \subset \models_p$ (where $\vdash$ is the provability relation of intuitionistic logic), and so our models are actual models of intuitionistic logic.
Now take $\mathbb{P}$ to be the natural numbers $\mathbb{N}$, we take only one relation symbol $D$ (representing the drinkers), and $\mathcal{D}= \mathbb{N}$ as well.
Define $[|D(n)|] = \{m, m\geq n\}$ to be our interpretation, this yields a model $\mathcal{M}$. Assume $\mathcal{M} \models \exists x, D(x) \implies (\forall y, D(y))$. Then for all $p$, there is a number $n_p$ such that $\mathcal{M}\models_p D(a_p) \implies \forall y, D(y)$. Unraveling the definitions, this tells us that for all $q\geq p$, if $q\in [|D(a_p)|]$, then $\mathcal{M}\models_q \forall y, D(y)$, hence $q\in \displaystyle\bigcap_{n\in \mathbb{N}} [|D(n)|]$. But this last thing is empty, therefore $[|D(a_p)|]\cap \{j, j\geq p\}$ is as well, a contradiction !
Thus it's not true that $\top \models (\exists x, \top) \implies \exists x, (D(x)\implies \forall y, D(y))$ and hence it's not true that $\vdash (\exists x, \top) \implies \exists x, (D(x)\implies \forall y, D(y))$: the drinker's paradox is not provable intuitionistically.
Of course I haven't done anything new, this is just combining Kripke semantics, topological semantics and the natural interpretation of nonclassicism ("infinite information is not available in finite time") to yield an easy proof of the nonprovability of the drinker's theorem; but if anyone could confirm that this works and that I haven't said anything silly, it would be great !
