Show that $ \forall{x}\exists{y}{(P(x) \to Q(y))} \vdash \exists{y}\forall{x}{(P(x) \to Q(y))} $

Question

I need to show that

$$ \forall{x}\exists{y}{(P(x) \to Q(y))} \vdash \exists{y}\forall{x}{(P(x) \to Q(y))} $$

using the natural deduction rules outlined in Logic in Computer Science: Modelling and Reasoning about Systems by Michael Huth and Mark Ryan.

There is a proof outlined in this answer. However, it seems to violate the scope requirements for $\forall{}$ introduction, as outlined in the book.

Answer 1

Yeah, that one is nasty! Using the Prenex Laws their equivalence is easily demonstrated, but proving those Prenex laws can be a pain. You'll need to use a proof by contradiction. Here is a proof that is quite similar ... and using very similar rules as well.

OK, here's the actual proof:

Answer 2

A proof of the problem given, adapted from @Bram28's answer