# Is there a theorem that can easily be proved to be non intuitionistic?

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$)

• See Intuitionistic Mathematics about weak counterexamples. – Mauro ALLEGRANZA Mar 4 '18 at 17:08
• Erm.... "essentially none" is my background in logic. According to your rendition of the Drinker Paradox, yours is different. – Professor Vector Mar 4 '18 at 17:15
• @ProfessorVector : I'm not talking about my background, I'm talking about my friends' ;) – Max Mar 4 '18 at 17:25
• The rendition of the Drinker Paradox you quote is theirs? – Professor Vector Mar 4 '18 at 17:26
• @ProfessorVector : well it's mine but it's essentially the same for everyone, isn't it ? – Max Mar 4 '18 at 17:31

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 !

• Your example is more complicated than necessary. Any preorder that isn't an equivalence relation will do. You can also use a temporal reading which is probably more accessible. So we can choose $\mathbb P=\{\mathsf{now},\mathsf{later}\}$ with $\mathsf{now}<\mathsf{later}$. Propositions are only allowed to move from false to true with "time", never the other way. Similarly, the domain can only increase with time. $P\implies Q$ means $P$ implies $Q$ at the current and all future times. Similarly, $\forall x.P(x)$ means $P$ holds for every element of the current domain and all future ones. ... – Derek Elkins Mar 16 '18 at 23:55
• ... $P\lor\neg P$ means $P$ is always false or always true and is invalidated by a $P$ which is false $\mathsf{now}$ but true $\mathsf{later}$. The Drinker's statement is then: "At any time there is a person who whenever they start drinking, everybody drinks from then on." To reiterate, once someone starts drinking they can't stop. One counter-model is then $\mathcal D_{\mathsf{now}}=\{a\}$ and $\mathcal D_{\mathsf{later}}=\{a,b\}$ with $D(a)$ and $\neg D(b)$. That is, someone drinking alone in a bar who is joined later by someone who doesn't drink. – Derek Elkins Mar 16 '18 at 23:55
• @DerekElkins : indeed, I was really complicating things, thanks a lot !! – Max Mar 17 '18 at 11:18
• Here's another example if you don't want to allow the domain to change. This uses a branching time model. Consider a poset that's a diamond which starts with two people who aren't drinking and ends with both people drinking, and the two intermediate worlds have one or the other drinking. The notion of truth is "things that are true regardless of the order of when the two people start drinking". The Drinker's statement again fails in the initial world, since it only holds of a person if they start drinking last. – Derek Elkins Apr 2 '18 at 1:47