# The existential theory of the reals

Some definitions of the existential theory of the reals (ETR) allow a real closed field and some definitions allow only rational numbers as coefficients of polynomials. Which one is correct? Will the answer to the question have an effect on the PSPACE proof by J. Canny? For example, ETR is not in PSPACE, if numbers in real closed field are allowed as coefficients?

-

## 1 Answer

In order for this to be a computational problem in the first place, you have to fix a representation of the coefficients by finite strings (which in particular implies that the field is countable). The answer will in general depend on the representation.

For the most obvious case, if the coefficients are taken from the field of real algebraic numbers, and are represented in a common way (minimal polynomial + an isolating interval or a BKR sign condition), then the problem is equivalent to the one with rational coefficients, because we can just plug the definitions of the coefficients into the formula.

-
Thanks for your answer. Is it correct that we then have to introduce one equation and one new fresh variable for each coefficient, if we choose, for example, the minimal polynomial representation for the coefficients? Won't it blow up the complexity? –  dschaehi Mar 8 '13 at 15:27
For each coefficient, you introduce one variable, an equation stating the variable is a root of the respective polynomial, and something to uniquely pick up the particular root: for example, if the coefficient is specified as the unique root of $f(x)$ in the interval $[a,b]$, you would include the inequalities $x-a\ge0$ and $b-x\ge0$ (which can be combined to $(x-a)(b-x)\ge0$). This is a polynomial-time reduction, the description of the new system has length polynomial in the length of the original input (in effect, it is the same input organized in a different way). ... –  Emil Jeřábek Mar 8 '13 at 17:06
... In particular, a PSPACE-algorithm for the problem with rational coefficients will give a PSPACE-algorithm for the more general problem. I have no practical experience with such problems, so I have no idea how much would it affect practical performance of the algorithm, or whether a different reduction might be more suitable, but for theoretical purposes, this preserves the computational complexity of the problem. –  Emil Jeřábek Mar 8 '13 at 17:11
in practice, exact symbolic algorithms for ETR are quite slow; in particular, the running time is exponential in the number of variables, with a largish constant. Algorithms based on sums of squares relaxations are faster, although the computations they perform are only approximate, implying all sorts of theoretical nastiness. –  Dima Pasechnik Mar 9 '13 at 7:27
Thanks for the answers and comments! –  dschaehi Mar 11 '13 at 10:48