Extension of Tarski's result on the decidability of reals

Due to Tarski's result, it is well-known that the first-order theory of reals $(\mathbb{R},+,\cdot,<,=,0,1)$ is decidable. I am working on a paper where I need an extension of this result. More precisely, I would like to consider formulas that involve rational functions, rational coefficients, minima and maxima. Trigonometric functions or exponential functions, instead, are excluded.

While this seems to me to be a straightforward consequence of Tarski's result (essentially, rewrite any formula with the above functions into one with polynomials only; e.g., rewrite $\sqrt[2]{x}$ into $\exists z (z^2 = x)$; for two polynomials $p$ and $q$, rewrite the formula $p / q \leq 1$ into $p \leq q$ and so on).

To my surprise, I could not find any paper that formally establishes this.

Before providing the proof on my own, I wanted to ask around whether someone is aware of a paper that establishes this result.

• The translation of $p/q\leq 1$ is more complex than you give, since you need to assert that $q\neq 0$ and deal with the possibility that one or both of $p$ and $q$ may be negative. May 21, 2015 at 10:10