Is there a natural deduction for ∀x∃y(P(x)→Q(y)) ⊢ ∀x(P(x)→∃y Q(y))?

Question

I have been trying to find a counter model to:

∀x∃y(P(x)→Q(y)) ⊢ ∀x(P(x)→∃yQ(y))

But I can't really find one. So, is there a natural deduction for this? If so, any hints on where to start?

Or am I missing something obvious? I have been at it for a while so I could be missing something really simple at this point.

Answer 1

1) $∀x∃y(P(x)→Q(y))$ --- premise

2) $∃y(P(x)→Q(y))$ --- $∀$-elim

3) $P(x)→Q(y)$ --- assumed [a] for $∃$-elim

4) $P(x)$ --- assumed [b]

5) $Q(y)$

6) $∃yQ(y)$ --- $∃$-intro

7) $P(x) \to ∃yQ(y)$ --- discharging [b]

8) $P(x) \to ∃yQ(y)$ --- from 3)-7) and 2) by $∃$-elim, discharging [a]

9) $∀x(P(x) \to ∃yQ(y))$ --- $∀$-intro.

---

Note. We have :

$\vdash (α → ∃y \ β) ↔ ∃y \ (α → β)$, if $y$ is not free in $α$.