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₁ be the largest value in V less than D; let D₂ be the smallest value in V greater than D; let L₁, L₂ be the labels in T corresponding to D₁, D₂; and let L = (L₁ + L₂)/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₁ ... 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₁ ... 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₁ ... 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₁ = a₁. By axiom A.8 there exists an infinite collection of points b₂, b₃ ... 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₁) = D and od( a₁,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₁ < L < L₂ where L₁ and L₂ are labels of consecutive values in T, then let D₁ and D₂ be the orders of magnitude corresponding to L₁, L₂ in T under Z. Let D be chosen so that D₁ << D << D₂. 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 -> 2d, 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 a. If p is true under Z then by lemma 27, there exists an extension T' of T and a instantiation Z' of T' such that a is true under Z'. By the inductive hypothesis, a is true under every instantiation of T'. Now, if d' is an instantiation of T' that satisfies a, and d is the restriction of d'to the variables in T, then clearly d satisfies exists_X a. But by lemma 26, every instantiation d of T can be extended to an instantiation d' of T'. Therefore, every instantiation of T satisfies p.

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.