# Logic of a Mixed Quantifier Conditional Proof

Given a true statement of the form $$\forall x\, \exists y\, (P(y) \implies S(x))$$ How would I go about instantiating this statement? I know that I can use a universal instantiation to yield $$\, \exists y\, (P(y) \implies S(m))$$ for some arbitrary $m$ in the universe, but is the existential instantiation just as simple as usual, i.e, do I just pick a $n$ for which $P$ holds? This would yield $$P(n) \implies S(m)$$ Is this correct?

Also, is an existential instantiation of this form "linked" to the variable $m$ that I introduced with the universal instantiation? That is, do I think of $m$ as being fixed?

As you correctly surmise, you can of course not just pick any constant to instantiate an existential with. Indeed, after having instantiated the universal with $m$, we can of course not guarantee that the 'something' that has property $P$ is that very $m$. And indeed in general we cannot instantiate the existential with any constant (or any variable-free term) that we are already using elsewhere.

This is why we have to pick a constant that we are not using elsewhere when instantiating an existential: it is our way of saying: "well, we know something has such-and-such a property, but we don't know who or what it is, so let's just give it a name, so we can at least refer to it by a name".

Finally, note that just because we use a new constant does not mean that it has to be different from any of the other constants already in use. That is, later on we may realize that $n=m$. But to be safe, and keep all possibilities open, we have to use a new constant.