3
$\begingroup$

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.

| cite | improve this question | |
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – David Richerby May 21 '15 at 10:10
3
$\begingroup$

I doubt there's a proof you can cite, since the result is obvious. The "features" you're adding are first-order definable, and first-order logic is closed under substitution.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.