Thread: Logic/disjunction proof

Prove ∃x(P(x) → ∀y(P(y))).


Obviously, we have that ∃x(P(x) → ∀y(P(y))) is equivalent to ∃x(¬P(x) ∨ ∀y(P(y))).

This exercise is found in a section on "proofs involving disjunctions." I have tried many different ways to solve this and have a feeling I am not approaching it the right way (why I"m not including any attempts above). Perhaps I am not considering clever enough exhaustive cases? Can anyone direct me in the proper way to begin?

This is the so-called drinker paradox: there is someone in the pub such that, if he is drinking, everyone in the pub is drinking. Its proof essentially uses the law of excluded middle or double-negation elimination.

Do you need a formal proof? If so, which proof system you are using?