You are here
Homeproperties of substitutability
Primary tabs
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,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$.
In all three cases, LHS $=$ RHS.

3. Finally, suppose $t$ is of the form $f(t_{1},\ldots,t_{n})$. Then LHS $=f(t_{1}[s/x],\ldots,t_{n}[s/x])[r/y]=f(t_{1}[s/x][r/y],\ldots,t_{n}[s/x][r/y])$, which, by induction, is
$f(t_{1}[r/y][s[r/y]/x],\ldots,t_{n}[r/y][s[r/y]/x])$ or $f(t_{1}[r/y],\ldots,t_{n}[r/y])[s[r/y]/x]=f(t_{1},\ldots,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[y/x][r/y]=t[r/x]$.
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,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},\ldots,t_{n})$, then LHS is $R(t_{1}[t/x][s/y],\ldots,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[y/x][s/y]=A[s/x]$.
Mathematics Subject Classification
03B10 no label found03B05 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
 Corrections