properties of substitutability
In this entry, we list some basic properties of substitutability in first order logic with respect to commutativity.
Proposition 1.
If $x\mathrm{,}y$ are distinct variables, then
$$t[s/x][r/y]=t[r/y][s[r/y]/x],$$ 
provided that $x$ does not occur in $r$.
Proof.
Suppose $x$ and $y$ are distinct variables, and $r,s,t$ are terms. We do induction^{} on the complexity of $t$.

1.
First, suppose $t$ is a constant symbol. Then LHS and RHS are both $t$.

2.
Next, suppose $t$ is a variable.

–
If $t$ is $x$, then LHS $=s[r/y]$, and since $y$ is not $x$, RHS $=x[s[r/y]/x]=s[r/y]$.

–
If $t$ is $y$, then LHS $=y[r/y]=r$, since $x$ is not $y$, and RHS $=r[s[r/y]/x]=r$, since $x$ does not occur in $r$.

–
If $t$ is neither $x$ nor $y$, then both sides are $t$.
In all three cases, LHS $=$ RHS.

–

3.
Finally, suppose $t$ is of the form $f({t}_{1},\mathrm{\dots},{t}_{n})$. Then LHS $=f({t}_{1}[s/x],\mathrm{\dots},{t}_{n}[s/x])[r/y]=f({t}_{1}[s/x][r/y],\mathrm{\dots},{t}_{n}[s/x][r/y])$, which, by induction, is
$$f({t}_{1}[r/y][s[r/y]/x],\mathrm{\dots},{t}_{n}[r/y][s[r/y]/x])$$ or $f({t}_{1}[r/y],\mathrm{\dots},{t}_{n}[r/y])[s[r/y]/x]=f({t}_{1},\mathrm{\dots},{t}_{n})[r/y][s[r/y]/x]=$RHS.
∎
Now, if $s$ is $y$, then $t[y/x][r/y]=t[r/y][r/x]$, and we record the following corollary:
Corollary 1.
If $x$ is not in $r$ and $y$ not in $t$, then $t\mathit{}\mathrm{[}y\mathrm{/}x\mathrm{]}\mathit{}\mathrm{[}r\mathrm{/}y\mathrm{]}\mathrm{=}t\mathit{}\mathrm{[}r\mathrm{/}x\mathrm{]}$.
The only thing we need to show is the case when $x$ is $y$, but this is also clear, as $t[y/x][r/y]=t[x/x][r/x]=t[r/x]$.
With respect to formulas^{}, we have a similar proposition^{}:
Proposition 2.
If $x\mathrm{,}y$ are distinct variables, then
$$A[t/x][s/y]=A[s/y][t[s/y]/x],$$ 
provided that $x$ does not occur in $s$, and $t$ and $s$ are respectively free for $x$ and $y$ in $A$.
Proof.
Suppose $x$ and $y$ are distinct variables, $s,t$ terms, and $A$ a wff. We do induction on the complexity of $A$.

1.
First, suppose $A$ is atomic.

–
$A$ is of the form ${t}_{1}={t}_{2}$, then LHS is ${t}_{1}[t/x][s/y]={t}_{2}[t/x][s/y]$ and we can apply the previous equation to both ${t}_{1}$ and ${t}_{2}$ to get RHS.

–
If $A$ is of the form $R({t}_{1},\mathrm{\dots},{t}_{n})$, then LHS is $R({t}_{1}[t/x][s/y],\mathrm{\dots},{t}_{n}[t/x][s/y])$, and we again apply the previous equation to each ${t}_{i}$ to get RHS.

–

2.
Next, suppose $A$ is of the form $B\to C$. Then LHS $=B[t/x][s/y]\to C[t/x][s/y]$, and, by induction, is $B[s/y][t[s/y]/x]\to C[s/y][t[s/y]/x]=$ RHS.

3.
Finally, suppose $A$ is of the form $\exists zB$.

–
$x$ is $z$. Then $A[t/x][s/y]=A[s/y]$, and $A[s/y][t[s/y]/x]=A[s/y]$ since $x$ is bound in $A[s/y]$.

–
$x$ is not $z$. Then $A[t/x][s/y]=(\exists zB[t/x])[s/y]$.

*
$y$ is $z$. Then $(\exists zB[t/x])[s/y]=\exists zB[t/x]$. On the other hand, $A[s/y][t[s/y]/x]=A[t[s/y]/x]=\exists zB[t[s/y]/x]$. By induction, $t,s$ are free for $x,y$ in $B$, and $B[t/x]=B[t[s/y]/x]$, the result follows.

*
$y$ is not $z$. Then $(\exists zB[t/x])[s/y]=\exists zB[t/x][s/y]$. On the other hand, $A[s/y][t[s/y]/x]=(\exists zB[s/y])[t[s/y]/x]=\exists zB[s/y][t[s/y]/x]$ since $x$ is not $z$. By induction again, $t,s$ are free for $x,y$ in $B$, and $B[t/x]=B[t[s/y]/x]$, the result follows once more.

*

–
∎
Now, if $t$ is $y$, then $A[y/x][s/y]=A[s/y][s/x]$, and we record the following corollary:
Corollary 2.
If $y$ is not free in $A$, and is free for $x$ in $A$, then $A\mathit{}\mathrm{[}y\mathrm{/}x\mathrm{]}\mathit{}\mathrm{[}s\mathrm{/}y\mathrm{]}\mathrm{=}A\mathit{}\mathrm{[}s\mathrm{/}x\mathrm{]}$.
Title  properties of substitutability 

Canonical name  PropertiesOfSubstitutability 
Date of creation  20130322 19:35:51 
Last modified on  20130322 19:35:51 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  23 
Author  CWoo (3771) 
Entry type  Result 
Classification  msc 03B10 
Classification  msc 03B05 
\@unrecurse 