Proof of theorem 4

**Lemma 24:** Let *T* be a cluster tree and let *Z* be a valuation
over om-space *O* satisfying *T*. Let *x* be a symbol not in *T*,
let *a* be a point in *O*, and let *Z*' be the valuation
*Z* *union* {*x* -> *a*}. Then there exists an extension
*T*' of *T* by *x* such that *Z*' satisfies *T*'.

**Proof:** If *T* is the empty tree, the statement is trivial. If
*T* contains the single symbol *y*, then if *a* = *Z*(*y*) then
operation (2) applies with *M*.label=0; if *a* <> *Z*(*y*) then
operation (2) applies with *M*.label=1.

Otherwise, let *y* be the symbol in *T* such that od(*Z*(*y*),*a*) is
minimal. (We will deal with the case of ties in step (D) below.)
Let *F* be the father of *y in T*.

Let *D*=od(*Z*(*y*),*a*).
Let *V* be the set of all orders of magnitude od(
*Z*(*p*), *Z*(*q*)),
where *p* and *q* range over symbols in *T*. We define *L* to be the
*suitable label for **D* as follows: If *D in V*, then *L* is the
label in *T* corresponding to *D*. If *D* is larger than any value
in *V* then *L* is the label of the root of *T* plus 1. If *D* *not in* *V*,
but some value in *V* is larger than *D*, then
let *D*_{1} be the largest value in *V* less than *D*;
let *D*_{2} be the smallest value in *V* greater than *D*;
let *L*_{1}, *L*_{2} be the labels in *T* corresponding to *D*_{1}, *D*_{2};
and let
*L* = (*L*_{1} + *L*_{2})/2.

One of the following must hold:

- A.
*Z*(*y*) =*a*, and*F*.label=0. Then apply operation (3) with*N*=*F*.- B.
*Z*(*y*) =*a*and*F*.label <> 0. Then apply operation (4) with*M*.label = 0.- C.
*Z*(*y*) <>*a*, but od(*Z*(*y*),*a*) is less than od(*Z*(*z*),*a*) for any other symbol*z*<>*y in T*. Apply operation (4) with*M*.label set to the suitable value for*D in T*.- D.
- There is more than one value
*y*_{1}...*y*_{k}for which od(*Z*(*y*_{i}),*a*) =*D*. It is easily shown that in this case there is an internal node*Q*such that*y*_{1}...*y*_{k}is just the set of symbols in the subtree of*Q*. There are three cases to consider:- D.i
*D*=odiam(*Z*(*Q*.symbols)). Then apply operation (3) with*N*=*Q*.- D.ii
*D*> odiam(*Z*(*Q*.symbols)), and*Q*is not the root. Then apply operation (5) with*C*=*Q*. Set*M*.label to be the suitable value for*D*. (It is easily shown that*D*< odiam(*Z*(*N*.symbols)), where*N*is the father of*Q*.)- D.iii
*D*> odiam(*Z*(*Q*.symbols)), and*Q*is the root. Apply operation (6).

**Lemma 25:** Let *A* ={
*a*_{1} ... *a*_{k}} be a finite set of
points whose diameter has order-of-magnitude *D*. Then there exists
a point *u* such that, for
*i* = 1 ... *k*, od(*u*,*a*_{i}) = *D*.

**Proof:** Let
*b*_{1} = *a*_{1}. By axiom A.8 there exists an
infinite collection of points
*b*_{2}, *b*_{3} ... such that od(
*b*_{i},*b*_{j}) = *D* for *i* <> *j*. Now,
for any value *a*_{i} there can be at most one value *b*_{j} such
that od(
*a*_{i}, *b*_{j}) << *D*; if there were two such values
*b*_{j1} and *b*_{j2},
then by the om-triangle inequality, od(
*b*_{j1},*b*_{j2})
<< *D*. Hence, all but *k* different values of *b*_{j}
are at least *D* from any of the *a*_{i}. Let *u* be any of these
values of *b*_{j}. Then since od(*u*,*a*_{1}) = *D* and od(
*a*_{1},*a*_{i})
<<= *D* for all *i*, it follows that od(*u*,*a*_{i}) <<= *D* for all *a*_{i}. Thus, since od(*u*,*a*_{i}) <<= *D* but
not od(*u*,*a*_{i}) << *D*, it follows that od(*u*,*a*_{i}) = *D*.

**Lemma 26:** Let *T* be a cluster tree; let *Z* be a valuation
over om-space *O* satisfying *T*; and let *T*' be an
extension of *T* by *x*. If *O* is dense and unbounded above,
then there is a value *a* such that the valuation *Z* *union*
{*x* -> *a*} satisfies *T*'.

**Proof:** For operations (1) and (2) the statement is trivial.

Otherwise, let *L* be an extending label of *T*. If *L* = 0, then set *D* = 0.
If *L* is in *T*, then let *D* be the order of magnitude corresponding to *L*
in *T* under *Z*.
If
*L*_{1} < *L* < *L*_{2} where *L*_{1} and *L*_{2} are labels of consecutive
values in *T*, then let *D*_{1} and *D*_{2} be the orders of magnitude
corresponding to *L*_{1}, *L*_{2} *in T* under *Z*. Let *D* be
chosen so that
*D*_{1} << *D* << *D*_{2}. If *L* is greater than any
label in the tree, then choose *D* to be greater than the diameter of the
tree under *Z*.

If *T*' is formed from *T* by operation (3), then using
lemma 25
let *a* be a point such that od(*a*,*Z*(*y*)) = odiam(*N*) for all
*y in N*.symbols.

If *T*' is formed from *T* by operation (4), then let *a* be a
point such that od(*a*,*Z*(*y*)) = *D*.

If *T*' is formed from *T* by operation (5), then let *a* be a
point such that od(*a*,*Z*(*y*)) = *D* for all *y in C*.symbols.
(Note that, since *M*.label < *N*.label, *D* < odiam(*N*.symbols).)

If *T*' is formed from *T* by operation (6), then let *a* be a
point such that od(*a*,*Z*(*y*)) = *D* for all *y in R*.symbols.

In each of these cases, it is straightforward to verify that
*Z* *union* {*x* -> *a*} satisfies *T*'.

As we observed in section 8 regarding
lemma 28, the conditions on *O* in
lemma 26
are necessary, and the statement is false otherwise. For example,
let *O* be the om-space described in example I, section 3, of
polynomials over an infinitesimal *d*. Then *O* is not
unbounded above; there is a maximum order-of-magnitude *O*(1).
Let *T* be the starting tree of Figure 3 (upper-left corner),
and let *T*' be the result of applying operation 6 (middle bottom).
Let *Z* be the valuation {
*u* -> *d*, *v* -> 2*d*,
*w* -> 1}. Then *Z* satisfies *T*, but it cannot be extended
to a valuation that satisfies *T*', as that would require *x* to
be given a value such that od(*v*,*w*) << od(*x*,*w*), and no such value
exists within *O*. The point of the lemma
is that, if *O* is required to be both dense and unbounded above,
then we cannot get ``stuck'' in this way.

**Lemma 27:** Let *T* be a cluster tree. Let *X* be a variable not among
the symbols of *T*. Let *a* be an open formula
in *L*, whose free variables are the symbols of *T* and the variable
*X*. Let *p* be the formula exists_*X* *a*. Let *O* be an om-space
that is dense and unbounded above. Then
there exists an instantiation *Z* of *T in O* that satisfies
*p* if and only if there exists an extension *T*' of *T* and an instantiation *Z*' of *T*' that extends *Z*
and satisfies *a*.

**Proof:** Suppose that there exists an instantiation *Z* of *T* that satisfies exists_*X* *a*. Then, by definition, there is a point
*a in O* such that *Z* satisfies *a*(*X*/*a*). That is,
the instantiation *Z* *union* {*X* -> *a*} satisfies *a*.
Let *Z*' = *Z* *union* {*X* -> *a*}. By
lemma 24, the cluster tree *T*'
corresponding to *Z*'is an extension of *T*.

Conversely, suppose that there exists an extension *T*' of
*T* and an instantiation *Z*' of *T*' satisfying
*a*. Let *Z* be the restriction of *Z*' to the
symbols of *T*. Then clearly *Z* satisfies the formula
exists_*X* *a*.

**Lemma 28:** Let *T* be a cluster tree. Let *p* be an open formula
in *L*, whose free variables are the symbols of *T*.
Let *O* be an om-space
that is dense and unbounded above.
If one instantiation *Z* of *T in O* satisfies *p* then every
instantiation of *T in O* satisfies *p*.

**Proof:** We can assume without loss of generality that
the only logical symbols in *p* are *not*, *and*,
*exists*, = (equals) and variables names, and that the only non-logical
symbol is the predicate ``much_closer''. We now proceed using structural
induction on the form of *p*. Note that
an equivalent statement of the inductive hypothesis is, ``For any
formula *q*, either *q* is true under every instantiation of *T*,
or *q* is false under every instantiation of *T*.''

Base case: If *p* is an atomic formula ``*X* = *Y*'' or
``much_closer(*W*,*X*,*Y*,*Z*)'' then this follows immediately from corollary 4.

Let *p* have the form *not* *q*. If *p* is true under
*Z*, then *q* is false under *Z*. By the inductive hypothesis,
*q* is false under every instantiation of *T*. Hence *p* is
true under every instantiation of *T*.

Let *p* have the form *q* *and* *r*. If *p* is true under
*Z* then both *q* and *r* are true under *Z*. By
the inductive hypothesis, both *q* and *r* are true under
every instantiation of *T*. Hence *p* is true under every instantiation
of *T*.

Let *p* have the form *exists _{X}*

**Theorem 4:** Let *T* be a cluster tree. Let *p* be an open formula
in *L*, whose free variables are the symbols of *T*.
Let *O* be an om-space
that is dense and unbounded above. Algorithm decide(*T*,*p*) returns
**true** if *T* satisfies *p* and **false** otherwise.

**Proof:** Immediate from the proof of lemma 28.