Natural Deduction $(∀x∃y (P(x) → Q(y))) → (∃y∀x(P(x) → Q(y)))$

Question

I am having trouble with this Natural Deduction question

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

Answer 1

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))$.