# 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. 1.

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

2. 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. 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]$.

###### 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. 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. 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. 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]$.

Title properties of substitutability PropertiesOfSubstitutability 2013-03-22 19:35:51 2013-03-22 19:35:51 CWoo (3771) CWoo (3771) 23 CWoo (3771) Result msc 03B10 msc 03B05