equivalent formulation of substitutability

Proposition 1.

Suppose a variable $x$ occurs free in a wff $A$. A term $t$ is free for $x$ in $A$ iff no variables in $t$ are bound by a quantifier in $A\mathit{}\mathrm{[}t\mathrm{/}x\mathrm{]}$.

Proof.

We do induction on the complexity of $A$.

• If $A$ is atomic, then any $t$ is free for $x$ in $A$, and clearly $A[t/x]$ is just $A$, which has no bound variables.

• If $A$ is of the form $B\to C$, then $t$ is free for $x$ in $A$ iff $t$ is free for $x$ in both $B$ and $C$ iff no variables in $t$ are bound in either $B$ or $C$ iff no variables in $t$ are bound in $A$.

• Finally, suppose $A$ is of the form $\exists yB$. Since $x$ is free in $A$, $x$ is not $y$, and $t$ is free for $x$ in $A$ iff $y$ is not in $t$ and $t$ is free for $x$ in $B$ iff, by induction, $y$ is not in $t$ and no variables of $t$ are bound in $B[t/x]$ iff no variables of $t$ are bound in $\exists yB[t/x]$, which is just $A[t/x]$ (since $x\ne y$).

∎

If $x$ does not occur free in $A$ (either $x$ occurs bound in $A$ or not at all in $A$), then $t$ is obviously free for $x$ in $A$, but $A[t/x]$ is just $A$, and there is no guarantee that variables in $t$ are bound in $A$ or not.

In the special case where $t$ is a variable $y$, we see that $y$ is free for $x$ in $A$ iff $y$ is not bound in $A[y/x]$, provided that $x$ occurs free in $A$. In other words, $y$ is free for $x$ in $A$ iff no free occurrences of $x$ in $A$ are in the scope of $Qy$, where $Q$ is either $\exists$ or $\forall$. So if $y$ is not bound in $A$, $y$ is free for $x$ in $A$, regardless of whether $x$ is free or bound in $A$. Also, $x$ is always free for $x$ in $A$.