First-order substitution
= First-order substitution
{title2=$\varphi[\tau/z]$}
Replacing every free occurrence of variable $z$ in a <first-order formula> by a <first-order term> $\tau$. Bound occurrences of $z$ are left alone. The operation requires either that $\tau$ be <free for substitution> at those occurrences or that conflicting <bound variables> first be renamed, as in <capture-avoiding first-order substitution>.