FOM: computable ordered nonabelian group

[Matthew Frank]

In response to my request for a computable ordered nonabelian group, Chris
Miller suggested "the group of infinitely increasing (i.e., $\uparrow
+\infty$) germs at $+\infty$ of (absolutely) semialgebraic functions",
where the group operation is composition and the order is the natural
order.  This indeed fits the bill; my unpacking of the suggestion is
below.  --Matt


f(x) is semi-algebraic if f(x)=y is equivalent to
 exists z1, ... zn such that phi(x,y,z1,...,zn),
 where phi is quantifier-free and in the language of fields
So we can represent these functions by formulas in order to discuss
computability.


Our group is the set of semi-algebraic functions such that
 f(x) -> infinity when x->+infinity, i.e.
 for every N, there exists c, for all x>c, f(x)>N

under the equivalence operation of f(x)~g(x) iff
 there is some c such that f(x)=g(x) for all x>c

with the group operation being composition,

and the order being f(x)>g(x) iff
 there is some c such that f(x)>g(x) for all x>c.


We have inverses because all these functions are eventually monotone,
  and inverses are computable by switching x and y in phi.
Group composition is (well-defined and) computable:
  if f(x)=y is equivalent to alpha 
  and g(y)=z is equivalent to beta
  then g(f(x))=z is equivalent to (exists y)(alpha and beta),
    which can be rewritten in the desired form.

The order relation is computable by the decidability of RCF.
Trichotomy holds because distinct semi-algebraic functions can be equal
at only finitely many points.

If f>g then hf>hg by the eventual monotonicity of h
If f>g then fh>gh trivially.