[FOM] Re: query about complexity of the theory of [R,+, < ]

[Dave Marker]

Martin:

The theory of nontrivial divisible ordered abelian groups is
complete. So the ordered groups of the reals and the rationals
have the same decidable theory. [This is in section 3.1 of my
Model Theory text.]

Ferrante and Rackoff gave a O(2^{cn}) decision procedure for some c,
while Fischer and Rabin showed that for some constants d there
is no O(2^{dn}) algorithm.

My recollection is that even for stronger theories like the theory
of real closed fields or the theory of the real field with
exponentiation the Fischer-Rabin lower bounds were the best known.
I would be interested if anyone knows of any better results.

Dave Marker