I am wondering if it is legitimate in first-order logic to quantify one variable twice in a single formula, for instance, as in the following proposition: \begin{equation} \left(\forall s\right) \left(\exists t\right) \left[P\left(t\right) \wedge R\left(s\right) \wedge \left(\exists s\right) Q\left(s\right)\right]. \end{equation} It seems to me that there is no problem in $s$ appearing twice as quantifiers. But it looks a little weird.
P.S. I am having this question as I read the following statement in set theory about variable substitution:
If $\Psi$ is $\left(\forall v_{k}\right)\Theta$ for some formula $\Theta$, and if $k \neq i$, then $\Psi^{*}$, which is achieved from substitution of $v_{j}$ for $v_{i}$ in $\Psi$, is just $\left(\forall v_{k}\right)\Theta^{*}$, where $\Theta^{*}$ is achieved from substitution of $v_{j}$ for $v_{i}$ in $\Theta$. If $k = i$, then $\Psi^{*}$ is $\left(\forall v_{j}\right)\Gamma$, where $\Gamma$ is achieved from substitution of $v_{j}$ for $v_{i}$ in $\Theta$.
It seems that in set theory, variables are quantified only once. Otherwise, $\Gamma$ should be achieved from substitution of $v_{j}$ for FREE occurrences of $v_{i}$ in $\Theta$, which means that the substition should only take place the first time $v_{i}$ is met as a quantifier, and not for others included inside. Is it that in set theory, laws from first-order logic are relaxed so that each variable is assumed to be quantified only once?