Can we apply $2$ different quantifiers to the same variable

first-order-logiclogicpredicate-logicquantifiers

So I'm very new to FOL and I've been trying to wrap my head around quantifiers and the scope of them however I got a bit confused on this example

$\forall x\in D [p(x) \implies \exists x d(x)]$

Does this mean verbally for all $x \in D$ if p(x) is true then there exsists an $x \in D$ such that property $d(x)$ is true since the $\forall x$ scopes everything in the implication then everything in the implication must be an element of $D$ .
however I know that $2$ different quantifiers cannot quantify the same variable so is it just then for all $x \in D$ if $p(x)$ is true then there exsists some x possibly not in $D$ such that $d(x)$ is true?.

Thanks in advance.

Best Answer

The quantifiers $\forall x\in D~$ and $\exists x$ each bind all free occurrences of $x$ inside their scope. However, any such occurrence can be bound to only one quantifier, and its immediate container has precedence.

Since such occurrences of $x$ inside the scope of $\exists x$ are bound to that quantifier, therefore they are not considered free inside the scope of $\forall x\in D$.

$\forall x\in D~.(p(x)\to\exists x~d(x))$ is equivalent to $\forall x\in D~.(p(x)\to\exists y~d(y))$ (with the caveat that $y$ does not occur free in $d(x)$ and is thus substitutable).


"For anything in $D$, should it satisfy $p(~)$ it will imply that something$^\dagger$ will satisfy $d(~)$."

$\dagger$ not necessarily the same thing, nor does it even need be in $D$.