I want to explain how the law of excluded middle is necessary for some theorems to some friends that don't have a lot of background in logic (essentially none), but the only things that I can prove are unprovable without the LEM are the dummy theorems "P or not P" and "not not P implies P" which are not necessarily great examples to convince someone ("You need the LEM; look, without it you can't even prove the LEM")
I know that there are other theorems (famously $d^2 = 0 \implies d=0$) but I think the level of the proof is a bit too high for what I'm looking for (if I recall correctly it uses topoi whereas I'm looking for something rather elementary). I thought an easy example could be the drinker's theorem : $(\exists x, x=x) \implies \exists x, (B(x)\implies \forall y, B(y))$. This is an easy theorem, and if I'm not mistaken it's not valid intuitionistically, and since it doesn't require any "construction" ($d^2=0 \implies d=0$ requires having built the reals) I figured that there could be an elementary proof of this fact.
Is there, and if so where could I find it ? If not, are there some "interesting" (for this question, the drinker's theorem will be considered interesting) theorems that are not provable intuitionistically, and such that the proof of this fact is "elementary" ? ("elementary" is left vague here, an example is the proof using Kripke semantics that $P\lor \neg P$ is not provable from intuitionistic logic for a propositional variable $P$)
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 !