# Proof of Drinker paradox [duplicate]

I searched all over the internet but didn't find a formal proof for this paradox, so here is my attempt:

$\exists x[P(x)\implies \forall yP(y)]$

Let $x=x_0$. Thus $P(x_0)$ is given.

Let $y$ be arbitrary. So we have to prove $P(y)$.

$y$ being arbitarary means that either $y=x_0$ or $y\ne x_0$.

So now we prove $P(x_0) \lor P(z)$ where $z$ is arbitrary and $z\ne x_0$.

$P(x_0)$ is given. So the paradox is true. $\square$

Is this correct ? If not what is wrong ?

## marked as duplicate by bof, Hakim, Namaste logic StackExchange.ready(function() { if (StackExchange.options.isMobile) return; $('.dupe-hammer-message-hover:not(.hover-bound)').each(function() { var$hover = $(this).addClass('hover-bound'),$msg = $hover.siblings('.dupe-hammer-message');$hover.hover( function() { $hover.showInfoMessage('', { messageElement:$msg.clone().show(), transient: false, position: { my: 'bottom left', at: 'top center', offsetTop: -7 }, dismissable: false, relativeToBody: true }); }, function() { StackExchange.helpers.removeMessages(); } ); }); }); May 24 '14 at 12:01

• @gitgud So I cant really separate the conclusion to cases ? – Nameless May 23 '14 at 20:21
• @gitgud Doesn't separating the $y$ into 2 cases give me all the possible $y$ values ? – Nameless May 23 '14 at 20:24
• But you'd need to conclude $P(y)$ is both cases. This isn't what you've done. – Git Gud May 23 '14 at 20:25
• You can find several proofs here. I like this one. – bof May 24 '14 at 10:53
• Note that $\exists x: P(x) \implies \forall x:P(x)$ is not true in general. – Dan Christensen Mar 6 '15 at 4:25

Your proof is bad. You don't have $P(x_0)$ is given. You have to show that such $x_0$ exists.

The point is that if there $x_0$ such that $\lnot P(x_0)$, then $P(x_0)\rightarrow\forall yP(y)$ is vacuously true; otherwise for all $x$ it is true that $P(x)$ and therefore $\forall yP(y)$ is true, and the implication is again true, in which case any choice of $x$ will prove the statement.

One key point is that the proof doesn't constructively show which of the option holds, is it the case that $\forall yP(y)$ is true, or perhaps there exists some $x$ such that $\lnot P(x)$?

• I used existential instantination to get $P(x_0)$. – Nameless May 23 '14 at 20:25
• But the instantiation doesn't give you $P(x_0)$. It gives you $P(x_0)\rightarrow\forall yP(y)$. – Asaf Karagila May 23 '14 at 20:27
• @Nameless Presumably $\exists x[P(x)\implies \forall yP(y)]$ is your thesis and not a premise. You can't instantitiate (is this a word?) from your goal. – Git Gud May 23 '14 at 20:27
• This isn't a formal proof, but I think it is what you really want: \begin{align}\exists x\left[P(x)\to \forall yP(y)\right]&\iff \exists x\left[\neg P(x)\lor \forall yP(y)\right]\\ &\iff \exists x\neg P(x)\lor \exists x\forall yP(y)\\ &\iff \exists x\neg P(x)\lor \forall yP(y)\\ &\iff \neg \forall x P(x)\lor \forall xP(x).\end{align} – Git Gud May 23 '14 at 20:49
• Semantically, assuming the universe isn't empty (otherwise neither the initial statement, nor that equivalence are true), assume $\forall xP(x)$ is true. Since $x$ is a bounded variable, you can change it, thus getting $\forall yP(y)$. Since the universe isn't empty there exists $x$. Therefore there exists $x$ such that $\forall yP(y)$. The other direction uses similar tricks. We've flooded Asaf's ping box enough. – Git Gud May 23 '14 at 21:04

I 'll just copy my proof from http://forums.philosophyforums.com/threads/lpl-exercise-and-60616.html

2  | |__________ ~Ex(Px -> VyPy)   New Subproof for ~ Introduction
3  | | |________ Pa                New Subproof for -> Introduction
4  | | | |_____b                   variable for Universal Introduction
5  | | | | |____ ~Pb               New Subproof for ~ Introduction
6  | | | | | |__ Pb                New Subproof for -> Introduction
7  | | | | | |   _|_               5,6 _|_ Introduction
8  | | | | | |   VyPy              7 _|_ Elimination
.  | | | | | <-------------------- end subpproof
9  | | | | |     Pb -> VyPy        6-8 -> Introduction
10 | | | | |     Ex(Px -> VyPy)    9 Existentional Introduction
11 | | | | |     _|_               2,10 _|_ Introduction
.. | | | | <---------------------- end subpproof
12 | | | |       ~~Pb              5-11 ~ Introduction
13 | | | |       Pb                12 ~~ Elimination
.. | | | <------------------------ end subpproof
14 | | |         VyPy              4-13 Universal Introduction
.. | | <-------------------------- end subpproof
15 | |           Pa -> VyPy        3-14 -> Introduction
16 | |           Ex(Px -> VyPy)    15 Existentional Introduction
17 | |          _|_                2,16 _|_ Introduction
.. | <---------------------------- end subpproof
18 |            ~~Ex(Px -> VyPy)   2-17 ~ Introduction
19 |            Ex(Px -> VyPy)     18 ~~ Elimination


This is the shortest I managed, I don't think a shorter proof using the standard introduction and elimination rules exist

Here we can find a discussion of the Drinker paradox.

We can prove it in Hilbert-style using the axiom system of Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001)).

In this post you can find a proof of theorem (Q3A) [see Example 8, page 130] :

$\vdash(∀x \beta \rightarrow \alpha) \leftrightarrow ∃x(\beta \rightarrow \alpha)$, if $x$ does not occur free in $\alpha$.

From axiom 2 : $\forall x \alpha \rightarrow \alpha[x/t]$, where $t$ is substitutable for $x$ in $\alpha$, with $P(x)$ as $\alpha$ and $y$ as $t$, we have :

$\vdash \forall x P(x) \rightarrow P(y)$.

Thus we have :

$\forall x P(x) \vdash P(y)$

and applying the Generalization Theorem [page 117] :

$\forall x P(x) \vdash \forall y P(y)$.

Finally, by Deduction Theorem [page 118], we conclude :

$\vdash (\forall x P(x) \rightarrow \forall y P(y))$.

Now we can apply the above theorem (Q3A), with $\forall y P(y)$ as $\alpha$ and $P(x)$ as $\beta$, where clearly, $x$ is not free in $\alpha$, to conclude :

$\vdash \exists x (P(x) \rightarrow \forall y P(y))$.