Proof of Drinker paradox [duplicate]

$\begingroup$

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 ?

$\endgroup$ 5

3 Answers

$\begingroup$

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

$\endgroup$ 10 $\begingroup$

I 'll just copy my proof from

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

$\endgroup$ $\begingroup$

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 :