= Solution
In a two-element <first-order structure>, $\phi=\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. \b[The <free for substitution> condition is necessary for soundness.]
Back to article page
