How to prove the tautology $ \neg \forall{x} \exists{y} (Py \wedge \neg Px) $? I've been beating my head trying to prove the following tautology for some time:
$$ \therefore \neg \forall{x} \exists{y} (Py \wedge \neg Px)$$
I think there's some tricky intermediate step that I'm missing. Any help would be appreciated.
 A: Let's start from the equivalent form
$$
\exists x \big( \forall y (\lnot Py \vee Px) \big),
$$
where I've added a set of brackets for clarity. The inner statement contains a disjunction where one of the sentences is independent of $y$; therefore we can move that sentence out of the scope of the quantifier:
$$
\exists x \big( Px \vee \forall y (\lnot Py) \big).
$$
Now we again have a disjunction where the second sentence is independent of $x$, so we separate it in a similar way:
$$
\exists x (Px) \vee \forall y (\lnot Py).
$$
This is clearly a tautology, after changing the second half to the equivalent $\lnot\exists x(Px)$.
A: Let's rewrite it explicitely so the tautological character of the sentence can be easily seen. $$\exists_x \forall_y \, \neg P(y) \vee P(x)$$
It simply says that either ($\exists_x P(x)$) or ($\forall_y \,\neg P(y)$) holds for each formula P.
A: I'll consider Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001)).
The proof system [see page 112] is based on modus ponens as only rule of inference and :

The logical axioms are all generalizations of wffs of the following forms, where $x$ and $y$ are variables and $\alpha$ and $\beta$ are wffs:
1. Tautologies;
2. $\forall x \alpha \rightarrow \alpha^x_t$, where $t$ is substitutable for $x$ in $\alpha$;
3. $\forall x(\alpha \rightarrow \beta) \rightarrow (\forall x\alpha \rightarrow  \forall x \beta)$;
4. $\alpha \rightarrow \forall x \alpha$, where $x$ does not occur free in $\alpha$.

We need also some provable equivalences; see Enderton, page 121 and page 130 :

(Q2A) -- $\vdash (\alpha \rightarrow \forall x \beta) \leftrightarrow \forall x (\alpha \rightarrow \beta)$, if $x$ does not occur free in $\alpha$
(Q2B) -- $\vdash (\alpha \rightarrow \exists x \beta) \leftrightarrow \exists x (\alpha \rightarrow \beta)$, if $x$ does not occur free in $\alpha$
(Q3A) -- $\vdash (\forall x \beta \rightarrow \alpha) \leftrightarrow \exists x (\beta \rightarrow \alpha)$, if $x$ does not occur free in $\alpha$
(Q3B) -- $\vdash (\exists x \beta \rightarrow \alpha) \leftrightarrow \forall x (\beta \rightarrow \alpha)$, if $x$ does not occur free in $\alpha$.


Proof
All the following steps are equivalences.

(1) $\exists y Py \rightarrow \exists y Py$ --- axiom 1 : it is an instance of the tautology : $\alpha \rightarrow \alpha$ [please, note that it is also : $\lnot \exists y Py \lor \exists y Py$, from which its "tautologuous" nature is still more evident]

(2) $\exists y Py \rightarrow \exists x Px$ --- renaming bound variables [see Theorem 241 (Existence of Alphabetic Variants), page 126]
(3) $\exists x(\exists y Py \rightarrow Px)$ --- by (Q2B), because $x$ is not free in $\exists y Py$
(4) $\exists x \forall y(Py \rightarrow Px)$ --- by (Q3B), because $y$ is not free in $Px$
(5) $\exists x \forall y \lnot (Py \land \lnot Px)$ --- by the tautological equivalence : $(p \rightarrow q) \leftrightarrow \lnot (p \land \lnot q)$


(6) $\lnot \forall x \exists y (Py \land \lnot Px)$ --- by the properties of quantifiers.


