Proof of a statement involving quantifiers I've been trying to solve the following exercise of Velleman's "How To Prove It":
Prove $\exists x(P(x)\to \forall yP(y))$.
Could anybody give a hint on this? I guessed some transformations could be made to the problem, but I'm not quite sure...
Thanks!
 A: Depending on what are exactly the logical axioms of your first order logic, the proof would be a bit different. 

Intuitively, consider whether $(\forall y)P(y)$ holds. If it does then any $x$ would make $P(x) \Rightarrow (\forall y)P(y)$ hold. Hence $(\exists x)(P(x) \Rightarrow (\forall y)P(y))$. 
The other case is that $\neg(\forall y)P(y)$. Let $x$ be such that $\neg P(x)$. Then for this particular $x$, $P(x) \Rightarrow (\forall y)P(y)$ since the conditional is not satisfied. Thus $(\exists x)(P(x) \Rightarrow (\forall y)P(y))$. 
A: Alternatively (to add to @William's answer) proceed by Reductio: so suppose
$$\neg\exists x(Px \to \forall yPy)$$which is equivalent to $$\forall x\neg(Px \to \forall yPy).$$ The only thing we can do is pick some object from the domain [here we do have to assume a non-empty domain] and instantiate to get $$\neg(Pa \to \forall yPy)$$A negated conditional is only true if the antecedent is true and consequent is false, hence $$Pa$$ $$\neg\forall yPy$$ From the latter we have $$\exists y\neg Py$$ An existential is only true if witnessed by some object, name it $b$, so $$\neg Pb$$ What else do we know about $b$? We have to appeal to the universal quantified claim (our only option here) so $$\neg(Pb \to \forall yPy)$$ Another negated conditional, so for it to be true its antecedent has to be true, i.e. $$Pb$$ And we have hit a contradiction. Our original supposition is ruled out, and we are done.
Of course, what we've got here is a (commented version of a) proof in a standard tree system of logic. And what it illustrates is how, in simple cases like this, the production of a proof in such a system is often more or less automatic (you don't need to think strategically, but just grind out doing the only sensible thing at each stage). It isn't for nothing that books such Richard Jeffrey's and Wifrid Hodges texts on logic-by-trees (and many later ones) have proved so popular for intro courses, as beginners find tree systems particularly easy to use.
