Variable Capture

Variable capture means a location that had a Free Variable in it becomes bound after the substitution or a location that had a bound variable in it becomes bound to a different quantifier after the substitution.

We have to watch out for “variable capture” in substitution.

Example of Variable Capture

If $P$ is $\forall x•q(y,x)$ and we try to do $P[x/y]$ we would arrive at $\forall x•q(x,x)$, which is NOT correct. This is an example of variable capture.

Related

• Be careful with variable capture whenever you do substitution
• Predicate Logic
• Program Correctness