Let be a linear free schema. Then such that and .

Proof:

We can define to be "almost" the natural state, . Where is an "unused" variable.

if state is such that

for some interpretation and variable ,

then there exists an interpretation such that

or .

Case 1: 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 or .

So or .

Case 2. There are some such that . Pick such that the number of these is minimal and

It none of these mention then we are done. If none of these mention then we are done. Otherwise contstruct interpretation which

s.danicic@gold.ac.uk