Past exam of the logic and set theory course of the University of Oxford / 2011 / A / 3 / b

The first-order term $t$ is free for substitution for $x_i$ in $\varphi$ if, at every free occurrence of $x_i$ to be replaced, no enclosing quantifier binds a variable occurring in $t$. Equivalently, the substitution introduces no variable capture. Only free occurrences of $x_i$ are replaced.

Take $\varphi =\forall x_1(x_0=x_1)$. The term $x_2$ is free for substitution for $x_0$: its variable is not bound by the enclosing quantifier. The term $x_1$ is not free for substitution for $x_0$, because insertion under $\forall x_1$ captures that occurrence.

Thus the first substitution gives $\forall x_1(x_2=x_1)$; the second, illegitimate substitution would give $\forall x_1(x_1=x_1)$.

In a two-element first-order structure, $\varphi =\forall x_1(x_0=x_1)$ is false for every first-order variable assignment. Blind substitution of $x_1$ for $x_0$ yields $\forall x_1(x_1=x_1)$, which is true. This does not express the original property evaluated at the value of the inserted term: it has changed a free parameter into a bound variable.

For a direct failure of the substitution axiom, use $\theta (x_0)=\exists x_1(x_0\ne x_1)$. On a two-element domain, $\forall x_0\theta (x_0)$ is true, whereas the captured instance $\exists x_1(x_1\ne x_1)$ is false. Consequently an unrestricted A4 would prove a false implication. The free for substitution condition is necessary for soundness.