It's well known that sentences about the real closed field can be decided by algorithm and the complexity of this is about $d^{2^{O(n)}}$ where $d$ is the product of the degrees of polynomials in the sentence. See [here](https://en.wikipedia.org/wiki/Real_closed_field#Complexity_of_deciding_%F0%9D%98%9Brcf)


Now adding an operation such as the $\sin$ function to the field structure leads to the ability to define natural numbers (and so now its undecidable).


Other operations such as adding an $\exp$ appear to be open problems (we can't prove if it is decidable or not, let alone having an algorithm which provably runs in finite time).


So I was curious, do we know ANY other *relations* which can be added to the underlying structure such that we still end up with a decidable theory AND we are able to prove new sentences which were not expressible before.


I would expect it should be possible to construct an ordinal-indexed hierarchy of such decidable theories, each of whose runtime for deciding expressions is naturally related to the ordinal it is indexed by and whose limit approaches the theory of the natural numbers.


But that is just wishful thinking for now ^


I guess I'm just curious if anyone knows how to make a "bigger" theory than the real closed field which is still decidable.



What theories are larger than the real closed field but still decidable?
Thanks to a 1958 paper by Abraham Robinson (whose impetus was a question of Alfred Tarski), an example of such a theory that properly extends RCF is the theory of the structure $(\mathbb{R},~+,~\cdot,~A)$, where $A$ is the collection of algebraic real numbers.


More generally, Robinson's proof shows that the theory of structures of the form $(\mathbb{R},~+,~\cdot,~F)$ is decidable for any *real closed* subfield $F$ of the field or reals.


A free copy of Robinson's paper can be found [here](http://matwbn.icm.edu.pl/ksiazki/fm/fm47/fm47111.pdf).


