Natural Deduction $(∀x∃y (P(x) → Q(y))) → (∃y∀x(P(x) → Q(y)))$ I am having trouble with this Natural Deduction question
$$(∀x∃y (P(x) → Q(y))) → (∃y∀x(P(x) → Q(y)))$$
 A: I will use natural deduction rules according to Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007) [see Appendix A, page 217-on, for a summary of the rules]. 
Proof
Assume the antecedent :

$∀x∃y(P(x)→Q(y))$ --- (A)

Then, by $\forall$-elimination :
$∃y(P(a)→Q(y))$
Assume $b$ for $\exists$-elimination :
$P(a)→Q(b)$ --- (B)
By $\forall$-introduction :

$\forall x(P(x)→Q(b))$

and by $\exists$-intorduction :

$\exists y\forall x(P(x)→Q(y))$.

Due to the fact that the "auxiliary" term $b$ is nor longer present in the conclusion, nor in the assumption (A), we can apply $\exists$-elimination and discharge (B), concluding with :

$\exists y\forall x(P(x)→Q(y))$.

Finally, by $\rightarrow$-introduction :


$\vdash (∀x∃y(P(x)→Q(y))) \rightarrow (\exists y\forall x(P(x)→Q(y)))$.



We may check it, showing that the formula is valid using the tableaux method [see Raymond Smullyan, First-Order Logic (1968 - Dover reprint)].
(1) $∀x∃y(P(x)→Q(y))$
(2) $\lnot (\exists y\forall x(P(x)→Q(y))$
(3) $\lnot \forall x(P(x)→Q(a))$ --- rule C on (2) with $a$
(4) $\lnot (P(b)→Q(a))$ --- rule D on (3) with $b$ new
(5) $Pb$ --- from (4)
(6) $\lnot Qa$ --- from (4)
(7) $\exists y(P(b)→Q(y))$ --- rule C on (1) with $b$ 
(8) $P(b)→Q(c)$ --- rule D on (7) with $c$ new
(9a) $\lnot Pb$ --- from (8) : closed with (5)
(9b) $Qc$ --- from (8) : open
(10) $\lnot \forall x(P(x)→Q(c))$ --- rule C on (2) with $c$
(11) $\lnot (P(d)→Q(c))$ --- rule D on (10) with $d$ new
(12) $Pd$ --- from (11)
(13) $\lnot Qc$ --- from (11) : closed witth (9b).
Thus :


$∀x∃y(P(x)→Q(y)) \vDash \exists y\forall x(P(x)→Q(y))$.



Appendix
We can prove it also in "Hilbert-style"; following Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001).
(1) $∀x∃y(P(x)→Q(y))$
(2) $∃y(P(c)→Q(y))$ --- where $c$ is a new constant, by Ax-2 [page 112]
(3) $P(c)→∃yQ(y)$ --- by (Q2B) [page 130], $y$ not free in $P(c)$
(4) $P(c)$ --- assumed
(5) $∃yQ(y)$ --- by modus ponens
(6) $\Gamma, ∃xP(x) \vdash ∃yQ(y)$ --- where $\Gamma = \{ ∀x∃y(P(x)→Q(y)) \}$, 
by Corollary 24H (Rule EI) [page 124 : Assume that the constant symbol $c$ does 
not occur in $\varphi, \psi$, or $\Gamma$, and that $\Gamma, \varphi[x/c] \vdash \psi$. Then $\Gamma, \exists x \varphi \vdash \psi$ and there is a deduction of $\psi$ from $\Gamma, \exists x \varphi$ in which $c$ does not occur.] 
(7) $\Gamma \vdash ∃xP(x) \rightarrow ∃yQ(y)$ --- by Deduction Theorem [page 118]
(8) $\Gamma \vdash \exists y(∃xP(x) \rightarrow Q(y))$ --- by (Q2B) [page 130], $y$ not free in $∃xP(x)$
(9) $\Gamma \vdash \exists y \forall x(P(x) \rightarrow Q(y))$ --- by (Q3A) [page 122], $x$ not free in $Q(y)$, and some tedious passages for replacement. 
Thus :

$∀x∃y(P(x)→Q(y)) \vdash \exists y \forall x(P(x) \rightarrow Q(y))$.

