# LP, the Larch Prover -- Capturing variables

It is generally the case that, for any formula `P(x)` involving a variable
`x` and any term `t`, the formula `P(t)` (i.e., the result of
substituting `t` for each free occurrence of `x` in `P`) is a logical
consequence of `P(x)`. However, this may not be the case if the substitution
*captures* some free variable in `t`, that is, if `t` contains a free
variable that becomes bound by some quantifier in `P`. For example, if
`P(x)` is `\E y (x ~= y)`, then `P(y)` and `P(s(y))` are not logical
consequences of `P(x)` because the free variable `y` in the terms `y`
and `s(y)` is captured by the quantifier in `P`.
For this reason, LP automatically changes bound variables to avoid captures
during rewriting, in response to the fix and instantiate
commands, and in response to the
generalization and
specialization proof methods.