How can I prove the following with natural deduction rules? ¬∀x∃yP(x,y) ⊢ ∃x∀y¬P(x,y) I have been stuck with this problem for a long time, I tried reductio ad absurdum and I got the hypothesys [¬∃x∀y¬P(x,y)], then I try to eliminate the negation of the premise, but I have to prove ∀x∃yP(x,y), and after using the introduction of universal quantifier rule, I go again with reductio ad absurdum, gaining a second hypothesis [¬∃yP(x,y)]. But at this point I have two hypothesis that contain negations of existencial quantifier, and I don't know how to use them constructively. I found some other similar questions, but all the answers given do not say which rules must be applied, and since I'm a beginner I didn't understand them.

You are doing this exactly right! You just have to derive $\forall y \
eg P(x,y)$ from $\
eg \exists y P(x,y)$

Now, I am not sure how your proof system defines the rule for $\forall$ Introduction ... in the system that I use you designate a 'fresh' constant to take the role of the arbitrary object from the domain. So this is what it looks like in my preferred system, called Fitch:

![enter image description here](