The task is to prove the following (wrong!!): $$ \exists x \forall y P(x,y),\exists a \exists b\neg Q(a,b) \vdash \exists a \exists b(\neg Q(a,b) \land \forall y(P(a,y) \lor P(b,y))) $$ I've actually seen the proof and it is over 30 lines... My main question is how on earth are you supposed to be able to figure that out without proof-solving software?
If someone can describe the method and the thinking strategies they use to solve a problem like the above, I'd be really grateful.
Edit Sorry, I goofed the proof. The real sequent to prove is the following: $$ \exists x \forall y P(x,y),\exists a \exists b(a\neq b) \vdash \exists a \exists b(a \neq b \land \forall y(P(a,y) \lor P(b,y))) $$ When posting on the stack, I usually rename variables and stuff to better understand the problem. But I didn't realize that the equality predicate is special so you can't change it. Sorry. My question is the same though.
The statement isn't true. Let $P(x,y)$ be $xy=0$, and let $Q(a,b)$ be $ab=0$. The hypotheses are satisfied, but the conclusion is $$\exists a\exists b(ab\ne 0\wedge \forall y(ay=0\vee by = 0))$$ which is false.