Transitivity of Dependence for Free Schemas

Let $S;T$ be a linear free schema. Then $x S;T z \iff \exists y$ such that $x S y$ and $y T z$.

Proof: $\rightarrow$

We can define $I[X \rightarrow X^{'}]$ to be "almost" the natural state, $I$. Where $X'$ is an "unused" variable.

So we are trying to prove that for free schemas $S$,

if state $J=I[X \rightarrow X^{'},Y\rightarrow Y^{'}]$ is such that

${\mathcal M}[\![{S}]\!] Ji(z) \neq {\mathcal M}[\![{S}]\!] Ii(z)$ for some interpretation $i$ and variable $z$,

then there exists an interpretation $j$ such that

${\mathcal M}[\![{S}]\!] I[X\rightarrow X^{'}]jz \neq {\mathcal M}[\![{S}]\!] Ijz$ or ${\mathcal M}[\![{S}]\!] I[Y\rightarrow Y^{'}]jz \neq {\mathcal M}[\![{S}]\!] Ijz$.

Case 1: $i(t) = i(t[X\rightarrow X^{'},Y\rightarrow Y^{'}])$ for all predicate terms $t$. This means $i$ follows the same path in $I$ as in $J$. So the final value of $z$ must in $I$ must mention $X$ or $Y$ and the final value in $J$ must mention $X^{'}$ or $Y^{'}$.

So ${\mathcal M}[\![{S}]\!] I[X\rightarrow X^{'}]iz \neq {\mathcal M}[\![{S}]\!] Iiz$ or ${\mathcal M}[\![{S}]\!] I[Y\rightarrow Y^{'}]iz \neq {\mathcal M}[\![{S}]\!] Iiz$.

Case 2. There are some $t$ such that $i(t) \neq i(t[X\rightarrow X^{'},Y\rightarrow Y^{'}])$. Pick $i$ such that the number of these is minimal and

$${\mathcal M}[\![{S}]\!] Ji(z) \neq {\mathcal M}[\![{S}]\!] Ii(z)$$

It none of these mention $X$ then we are done. If none of these mention $Y$ then we are done. Otherwise contstruct interpretation $i^{'}$ which $i^{'}(t) = i(t)[X\rightarrow X^{'}]$