= Capture-avoiding first-order substitution
{title2=$\varphi[\tau/z]$}
= Capture-avoiding substitution in first-order logic
{synonym}
To perform a <first-order substitution>, first rename each conflicting <bound variable> to a fresh name, then replace the designated free occurrences. The fresh names must avoid the formula's relevant free names and all names in the inserted <first-order term>. For instance, substituting $f(u,t)$ for $z$ in $\exists t\,Q(z,t)$ requires renaming the binder, producing $\exists s\,Q(f(u,t),s)$ rather than $\exists t\,Q(f(u,t),t)$. The latter would change the intended meaning by capturing $t$.
Back to article page
