Transitivity of Dependence for Free Schemas

Let

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

and

Proof: $\rightarrow$

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

So we are trying to prove that for free schemas ,

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 and variable ,

then there exists an interpretation 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 . This means follows the same path in as in . So the final value of must in must mention or and the final value in 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 such that $i(t) \neq i(t[X\rightarrow X^{'},Y\rightarrow Y^{'}])$ . Pick such that the number of these is minimal and

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

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

s.danicic@gold.ac.uk
Seb's Home Page
Last updated 2007-04-30