Quantifier Scope

Logical quantifiers binds a variable within some local scope. This means that whatever meaning we assign to a variable (by its quantifier) is only valid within the scope of said quantifier. More technically, the quantifier scope is the associated sub-formula after a quantifier and its variable.

It can be likened to program scope in coding, since a (programming) variable only makes sense within its function scope, just like a (logical) variable is only bound inside its quantifier scope.

Variable Binding §

A quantifier over some variable $x$ binds $x$ in its scope. Alternatively, $x$ is said to be a bound variable. Any unbound variable is said to be a free variable.

Bad Conventions

Technically speaking, unlike in maths, we can assign the same symbol $x$ to multiple variables. I.e., if we were to have a mathematical equation, it would be something like $x_1+x_2=x_3$, whereas a valid (here meaning obeying the rules) formula can just only use $x$ without any subscripts if each instance is in a different binding scope. That is, if we have a formula where $x$ is bound under different quantifiers (and/or is free) we can give it different meanings. This is similar to variable shadowing in programming, where variables with the same names have different purposes in different program scopes. It’s not good practice, but again, technically it’s possible.

Some examples:

• $\forall x,(P(x)\vee Q(y))$ : $x$ is bound, $y$ is a free variable
• $\forall z(P(y,z)\wedge \exists y(P(y,z)))$ : $z$ is bound throughout the formula, while the first $y$ (on the left) is free. The second $y$ (after the $\exists y$) is bound.
• $\exists x(Q(x))\vee P(x)\vee \exists x(R(x))$ : The first and last instances of $x$ are bound, while the middle one is free.

A formula is closed if it contains no free variables

Shadowing §

Variable shadowing occurs when the same variable is allocated inside two different quantifier scopes, one inside another:

$$\forall x(P(x)\vee \exists x(Q(\underline{x})))$$

• The $\exists x$ has shadowed the more ‘global’ $\forall x$
  • $Q(x)$ refers to the $\exists x$, not the $\forall x$