Scope of quantifiers in first-order logic

In many situations, it is important to know which variables have free occurrences within the scope of a quantification.

Example Although quantified variables can, in principle, be renamed while keeping equivalence, this is not true in general. For instance, $\forall x_0 \exists x_1 R(x_0, x_1)$ is not equivalent to $\forall x_1 \exists x_1 R(x_1, x_1)$, because the substituent $x_1$ gets into the scope of a quantification.

This leads to the following definition.

Definition [scope] The set of variables which occur free within the scope of quantifications of a variable $x_i$ in a first-order formula $\varphi$ is denoted $\text{scope}(x_i, \varphi)$ and defined by induction as follows.

Base mapping

• $\text{scope}(x_i, \bot) = \emptyset$ and $\text{scope}(x_i, \top) = \emptyset$.
• $\text{scope}(x_i, R(t_0, \dots, t_{n-1})) = \emptyset$ for every $n$-ary relation symbol $R$ and terms $t_0, \dots, t_{n-1}$.
• $\text{scope}(x_i, t_0 \doteq t_1) = \emptyset$ for all terms $t_0$ and $t_1$.

Another way to say this is: $\text{scope}(x_i, \varphi) = \emptyset$ for every atomic formula $\varphi$.

Inductive step

• $\text{scope}(x_i, C(\varphi_0, \dots, \varphi_{n-1})) = \bigcup_{i<n} \text{scope}(x_i, \varphi_j)$ for every $n$-ary connective $C$ and all formulas $\varphi_0, \dots, \varphi_{n-1}$.
• $\text{scope}(x_i, Q x_j \varphi) = \begin{cases}\text{fvars}(\varphi) \setminus \{x_i\} & \text{if $i = j$}\\ \text{scope}(x_i, \varphi) \setminus \{x_j\} & \text{otherwise}\end{cases}$ for $Q \in \{\exists, \forall\}$ and formula $\varphi$.

The scope for some formula can be different for any variable because each variable might occur with different quantifiers or unbounded.

Example \begin{align*} \operatorname{scope}(x_0, \forall x_0\;\exists x_1\; (E(x_0,x_1) \wedge E(x_1,x_2))) &= \operatorname{fvars}(\exists x_1\; (E(x_0,x_1) \wedge E(x_1,x_2))\setminus\{x_0\} & \text{Def. $\text{scope}$ (inductive step)}\\ &= \{x_0, x_2\}\setminus\{x_0\} & \text{Def. $\text{fvars}$}\\ &= \{x_2\} & \text{Def. $\setminus$}\\ \operatorname{scope}(x_1, \forall x_0\;\exists x_1\; (E(x_0,x_1) \wedge E(x_1,x_2))) &= \operatorname{scope}(x_1, \exists x_1\; (E(x_0,x_1) \wedge E(x_1,x_2)))\setminus\{x_0\} & \text{Def. $\text{scope}$ (inductive step)}\\ &= \operatorname{fvars}(E(x_0,x_1) \wedge E(x_1,x_2))\setminus\{x_1\}\setminus\{x_0\} & \text{Def. $\text{scope}$ (inductive step)}\\ &= \{x_0, x_1, x_2\}\setminus\{x_1\}\setminus\{x_0\} & \text{Def. $\text{fvars}$}\\ &= \{x_2\} & \text{Def. $\setminus$}\\ \operatorname{scope}(x_2, \forall x_0\;\exists x_1\; (E(x_0,x_1) \wedge E(x_1,x_2))) &= \operatorname{scope}(x_2, \exists x_1\; (E(x_0,x_1) \wedge E(x_1,x_2)))\setminus\{x_0\} & \text{Def. $\text{scope}$ (inductive step)}\\ &= \operatorname{scope}(x_2, E(x_0,x_1) \wedge E(x_1,x_2))\setminus\{x_1\}\setminus\{x_0\} & \text{Def. $\text{scope}$ (inductive step)}\\ &= \bigl(\operatorname{scope}(x_2, E(x_0,x_1)) \cup \operatorname{scope}(x_2, E(x_1,x_2))\bigr)\setminus\{x_1\}\setminus\{x_0\} & \text{Def. $\text{scope}$ (inductive step)}\\ &= \bigl(\emptyset \cup \emptyset\bigr)\setminus\{x_1\}\setminus\{x_0\} & \text{Def. $\text{scope}$ (base mapping)}\\ &= \emptyset & \text{}\\ \end{align*}

If in some formula $\varphi$ a variable $x_i$ is not quantified, then $\operatorname{scope}(x_i, \varphi)=\emptyset$.

Exercises

Exercise Show that for any first-order formula $\varphi$ and any variable $x_i\in\text{FOVars}$ it holds that \[\operatorname{scope}(x_i,\varphi) \subseteq \operatorname{fvars}(\varphi).\]