Particularization rules of premises with multiple quantifiers

Question

I have this reasoning with multiple quantifiers and I need to prove it's validity

$\exists x : [F(x) \wedge S(x)] \rightarrow \forall y : [M(y) \rightarrow W(y)]$

$\exists y : [M(y) \wedge \neg W(y)]$

∴ $\forall x : [F(x) \rightarrow \neg S(x)] $

My question is if I can particularize the quantifiers of the first premise separately, since the variables are different for each one. If not, then what's the best approach in this case?

Answer 1

Long comment

Details depend on the proof system used... but to "can I particularize the quantifiers of the first premise separately?" the answer is NO.

What we can do is to use Prenex Normal Form and re-write the 1st premise in the equivalent form:

$∀x[(F(x)∧S(x)) → ∀y (M(y)→W(y))].$

Having said that, a proof strategy can be:

Assume $Fa$ and assume $Sa$ and thus derive $Fa \land Sa$ and then $\exists x (Fx \land Sx)$.

With it, form 1st premise, derive $\forall y (My \to Wy)$ and using Existential Elimination on the 2nd premise derive a contradiction, from which you can close the sub-proof of EE and derive $\lnot Sa$ and finally $Fa \to \lnot Sa$, without open assumptions left and thus you can generalize it.