
## 8. The First-Order Theory

Our final result asserts that if the om-space is rich enough then the full first-order language of order-of-magnitude distance comparisons is decidable. Specifically, if the collection of orders of magnitude is dense and unbounded above, then there is a decision algorithm for first-order sentences over the formula, "od(W, X) ≪ od(Y, Z)" that runs in time O(4 n (n!) 2 s)
where n is the number of variables in the sentence and s is the length of the sentence.

The basic reason for this is the following: As we have observed in corollary 4, a cluster tree T determines the truth value of all constraints of the form "od( a, b ) ≪ od( c, d )" where a, b, c, d are symbols in the tree. That is, any two instantiations of T in any two omspaces agree on any such constraint. If we further require that the om-spaces are dense and unbounded, then a much stronger statement holds: Any two instantiations of T over such om-spaces agree on any first-order formula free in the symbols of T over the relation
"od( W, X ) ≪ od( Y, Z )". Hence, it suffices to check the truth of a sentence over all possible cluster trees on the variables in the sentence. Since there are only finitely many cluster trees over a fixed set of variables (taking into account only the relative order of the labels and not their numeric values), this is a decidable procedure.

Let L be the first-order language with equality with no constant or function symbols, and the single predicate symbol "much closer(a, b, c, d)".  It is easily shown that L is as expressive as the language with the function symbol "od" and the relation symbol «.

Definition 7: An om-space Ω with orders of magnitude D is dense if it satisfies the following axiom:
A.9 For all orders of magnitude δ 1 ≪ δ 3 in D , there exists a order of magnitude δ 2 in D
such that 61 << 62 << 63.

Ω is unbounded a bove if it satisfies the following:
A.10 For every order of magnitude δ 1 in D there exists δ 2 in D such that δ 1 ≪ δ 2 .

If D is the collection of orders of magnitude in the hyperreal line, then both of these are satisfied. In axiom [A.9], if 0 If 0 = δ 1 ≪ δ 3 , choose δ 2 = δ 3 δ where δ ≪ 1. In axiom [A.10] oose δ 2 = δ 1 /δ where 0 < δ < 1.

Definition 8: Let T be a cluster tree. Let lo = 0, l 1, l 2 . . . l k be the distinct labels in T
in ascending order. An extending label for T is either (a) li for some i; (b) lk + 1 (note that l k is the label of the root); (c) ( li –1 + li )/2 for some i between 1 and k .

Note that if T has k distinct non-zero labels, then there are 2 k + 2 different extending labels for T .

Definition 9: Let T be a cluster tree. Let x be a symbol not in T . The cluster tree T t extends T with x if T t is formed from T by applying one of the following operations (a single application of a single operation).

1. T is the null tree and T t is the tree containing the single node x .