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{]}$.