= Solution
A term $t$ is <free for substitution> for $x_i$ in $\alpha$ when none of its variables becomes bound at a free occurrence of $x_i$ being replaced. Equivalently, no <quantifier> surrounding such an occurrence binds a variable of $t$. Bound occurrences of $x_i$ are not replaced. This occurrence-sensitive condition prevents variable capture.
For example take $\alpha(x)=\exists y\,\neg(x=y)$ and $t=y$. On a two-element domain, $\forall x\exists y\,\neg(x=y)$ is true. Naive textual substitution produces $\exists y\,\neg(y=y)$, which is false on every nonempty domain. Thus the corresponding unrestricted A4 implication would be invalid. The problem is that the inserted free $y$ was captured by the existing <existential quantifier>. Renaming that binder first instead gives the correct instance $\exists z\,\neg(y=z)$, with $z$ fresh.
Back to article page
