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$.
Title  equivalent formulation of substitutability 

Canonical name  EquivalentFormulationOfSubstitutability 
Date of creation  20130322 19:35:57 
Last modified on  20130322 19:35:57 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  6 
Author  CWoo (3771) 
Entry type  Definition 
Classification  msc 03B05 
Classification  msc 03B10 
\@unrecurse 