For the life of me, I'm not able to show the following using Gentzen-style ND:
$\neg \forall x \exists y Pxy \vdash \exists x \forall y \neg Pxy$
We may use all the usual rules: $\land$-I, $\land$-E, $\lor$-I, $\lor$-E, $\to$-I, $\to$-E, $\neg$-I,$\neg$-E, CR (classical reductio), $\forall$-I, $\forall$-E, $\exists$-I, $\exists$-E, $=$-I, $=$-E. But we may not use any theorems or metatheorems.
I tried a bunch of stuff, but all my attempts fail at performing the all-introduction at the appropriate time. I'm not sure what to assume such that the constant appearing in the assumption doesn't hinder all-introduction (as the constant is not arbitrary should it appear in an open assumption).
For example, see the following (wrong) attempt:
The all-introduction is wrong because $b$ is not arbitrary.
But how else to proceed? Thanks for the help!
Best Answer
The result is "classic": so your idea of using somewhere LEM or DN is sound.
A possible approach is to assume, in addition to the negation of the formula to be derived, $Pxy$ and $¬∃yPxy$ as well. Using $(\exists \text I)$ we have a first contradiction discharging the first formula and deducing $¬Pxy$.
Now we can generalize wrt $y$ and introduce the existential quantifier for $x$ to have a second contradition with the assumed negation of the formula to be proved. By DN we will discharge the second assumption above to get $∃yPxy$.
Now we can generalize again, because there are no more assumptions with $x$ free, and we get the third and final contradiction.