Proof of Drinker paradox

Question

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 ?

Answer 1

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

Answer 2

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

Answer 3

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