Suppose my premise is "for all x: P(x)" and I am trying to prove "exists y: Q(y)". Which quantifier proof rule could I use in the first step of my proof, and which in the last?
My answer to this would be rule of specification, then existence. However, I am stuck on the difference between instantiation proof and existence. Can anyone help me with that?
You cannot prove it because it is not valid.
Consider the interpretation with domain the set $\mathbb N$ of natural numbers and interpret $P(x)$ as $x \ge 0$ and $Q(y)$ as $y < 0$.
Under this interpretation, the formula means :
In $\mathbb N$ the antecedent is true while the consequent is false: thus, the formula is false.