Proof of Drinker paradox [duplicate]
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 '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))$.