I'm trying to prove the claim ∀x¬∀y(Pxy→Qxy)⊢∀x∃yPxy in a Gentzen-style system. I know that I will have to use universal elimination to derive ¬∀y(Pay→Qay)from ∀x¬∀y(Pxy→Qxy). I would then use ¬∀y(Pay→Qay) to derive a contradiction, from some assumption ∀y(Pay→Qay). But I don't quite see how to go on from there-does anyone have an idea? My hunch is that the conclusion derives from a contradiction with no undischarged premises, but nothing I have tried quite works out.
Thanks for your help, it is much appreciated!
1) $∀x¬∀y(Pxy → Qxy)$ --- premise
2) $¬∀y(Pxy → Qxy)$ --- from 1) by $∀$-elim
3) $¬∃yPxy$ --- assumed [a]
4) $Pxy$ --- assumed [b]
5) $∃yxy$ --- from 4) by $∃$-intro
6) $\bot$ --- from 3) and 5)
7) $Qxy$ --- from 6) by $\bot$-elim: $\bot \vdash \varphi$
8) $Pxy → Qxy$ --- from 4) and 6) by $\to$-intro, discharging [b]
9) $∀y(Pxy → Qxy)$ --- from 8) by $∀$-intro: $y$ not free in 1) and 3)
10) $\bot$ --- from 2) and 9)
11) $∃yPxy$ --- from 3) by Double Negation, discharging [a]