Universal instantiation with universal quantifiers within scope If I have a formula in FOL of this kind
$\forall x, [[\forall y, \neg P(x) \vee \neg S(x, y)] \vee [\forall z, A(z) \wedge G(x,z)]]$
I want to remove the universal quantifiers.
What's the intuition behind removing the universal quantifiers for each variables?
I know that for a formula like $\forall x, P(x)$ you can do $P(x/u)$ where u is the substitution of x by a constant. But i don't know if the process is different if we have more universal quantifiers within the formula or if a predicate involves something more than x.
Help would be appreciated! 
 A: Consider the statement $\forall x P(x) \rightarrow 
Q$. This statement has a universal inside the statement in the sense that the statement is a conditional, the antecedent of which is a universal. As such, the statement is saying that $Q$ is true if all objects have property $P$. Now, can we instantiate the universal quantifier with some constant to get $P(c) \rightarrow Q$?  Clearly not, because the result would be a much stronger statement, as it says that  $Q$ is true once the single object c has property P.
So, we see that we cannot just instantiate any universal with a constant if it is inside a larger statement. Thus, we can do one of two things:


*

*We can come up with some way to figure out in which cases we can instantiate the universal when it is part of a larger statement. One could do this by counting how many negations the universal is 'in', and how many times it is in the antecedent of a conditional, and when that total number is even, one can instantiate the universal ... except when the universal is inside the scope of a biconditional (or an $xor$, or ...)

*We only allow the instantiation of a universal when the whole statement is a universal.
Typically, proof systems use the latter approach, as it is a good bit easier!  
