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

Substitution Inside Scope §

Bound variables can be renamed to other variable symbols (thus binding them instead) provided there is no clashing. To avoid clashing, the renamed variable must not be inside the quantifier scope (it does not matter if it is free or bound!). If these restrictions hold, then substitution does not change the semantics of the formula. That is, it preserves semantic consequences.

This does not hold when renaming free variables. Any renaming of a free variable no longer preserves semantic conseqeunces

For example, take the formula $P(x,y):\forall x(F(x)\wedge G(y))$. We can identify that (in the quantifier scope), $x$ is a bound variable and $y$ is a free variable:

• $P(x,y)[x:=z]=\forall z(F(z)\wedge G(y))$ is a substitution of a bound variable to an out-of-scope variable, $z$. Hence, semantic consequences are preserved i.e. the meaning of the formula is unchanged.
• $P(x,y)[x:=y]=\forall y(F(y)\wedge G(y))$ is a substitution of a bound variable to an in-scope variable. This formula has a very different meaning to the original $P(x,y)$. Hence, semantic consequences are not preserved.
• $P(x,y)[y:=z]=\forall x(F(x)\wedge G(z))$ is a substitution of a free variable. Semantic consequences are not preserved.