Is it legitimate to quantify a variable twice?

Question

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?

Answer 1

Yes, it is okay to reuse the same symbol for a variable in different "scopes". A quantifier binds the variable that it introduces within the subexpression headed by that quantifier.

Note that it's always possible to rewrite an expression into an equivalent one that does not reuse variable symbols, unless there are only finitely many variable symbols.

A variable may appear free in a well-formed formula, meaning that it isn't bound

$$ x \;\;\text{is free in}\;\; P(x) \land Q(x) $$

We can be more precise and use $\text{FV}$ to denote the set of free variables.

$$ \text{FV}(P(x) \land Q(x)) = \{ x \} $$

If a variable is bound by a quantifier then it is no longer free.

$$ \text{FV}\!\left(\forall x \mathop. P(x)\right) = \emptyset $$

We can think about the meaning of $\forall$ as well:

$$ \Gamma \models \forall x \mathop. \varphi \;\;\text{if and only if} \;\; \text{$\Gamma \models \varphi$ for every $x$ in the domain of discourse } $$

So, in the course of determining the truth of a well-formed formula headed by a quantifier, we can remove the quantifier and then consider the result of replacing the newly free variable with all the elements of the domain.

However, instances of $x$ that are hidden behind another quantifier won't actually be free in $\varphi$.

More concretely, the following two statements are equivalent

$$ \forall x \mathop. (P(x) \to \exists x \mathop. Q(x)) \;\;\text{is equivalent to}\;\; \forall x \mathop. (P(x) \to \exists y \mathop. Q(y)) $$

Answer 2

Your formula is a perfectly acceptable and grammatical formula in first-order logic, and it is exactly as you say: the $s$ in $Q(s)$ is quantified by the the $\exists s$, while the $s$ in $R(s)$ is quantified by the $\forall s$.

Note that you can even have something like $\forall s \ \exists s \ P(s)$. In this case, the $s$ in $P(s)$ gets quantified by the $\exists s$, meaning that there are no free variables $s$ to quantify for the $\forall s$. This is why in this formula the $\forall s$ is called a 'null quantifier': while still following the grammatical rules, it effectively serves no purpose. Indeed, the formula is equivalent to simply $\exists s \ P(s)$

But yes, you can use quantifiers with the same variable any number of times. But as you also say, it looks weird, and can certainly invite confusion, so I would recommend never to do this in practice. And if you need a lot of variables, you can always use $x_1, x_2, x_3, ...$

Answer 3

The existing answers are correct, but let me add the following:

In some contexts we find it convenient to restrict attention to formulas which do not do this. For example, it makes some arguments around substitutions easier. This is never truly a big deal as far as I'm aware, but the translation of an arbitrary first-order formula into a "no-redundant-quantification" formula is simple enough that it often (annoyingly!) goes unstated. While elementary logic texts will generally be careful about this, advanced texts and papers often make claims about arbitrary first-order formulas with the implicit assumption that they have no multiply-quantified variables.

It's also worth noting that there are two drawbacks to the translation above. First, it introduces new variables, so if you care about how many variables you're using you lose information. This is actually a meaningful issue - see e.g. chapter $11$ of Libkin's wonderful book Elements of finite model theory. Second, it impacts the complexity of the set of well-formed formulas (e.g. regular, context-free, ...). This isn't a topic I know much about so I don't have much to say here, but I'm sure there are times when this is an issue.