Testing if real-valued expressions are negative

[CRGreathouse]

In his famous (but unknown to me until recently) 1967 paper,* Richardson showed that the problem of deciding whether a one-variable subelementary expression (an expression involving +, -, *, exp, sin, composition, the constants log 2, pi, and all rational numbers, plus variables x_i) is negative is undecidable. This is a counterpoint to Tarski's decidability result on real closed fields (+, *, =, <).

Many papers have improved on these results in some direction or another. In particular, I was wondering if anyone knew whether this (once?-)unsolved problem mentioned in the paper has been solved:

No method is known for deciding whether a subelementary expression with no variables in it represents a number less than zero. Whether or not such a method exists is an open question.

Also, is there a good survey paper on this sort of work? There is a recent result of Laczkovich that generalizes Richardson (via Wang) by removing constants and substantially reducing composition, but I haven't seen anything remove the variable.

* Daniel Richardson, "Some undecidable problems involving elementary functions of a real variable", Journal of Symbolic Logic 33:4 (1968), pp. 514-520.

 

[CRGreathouse]

Starting to read the Laczkovich paper, I see that he narrows the gap for single-variable expressions substantially: using only x,\sin x^n,\sin(x\sin x^n), addition, and multiplication (composition only on the latter two) and the integers as constants* one obtains an undecidable theory. Replacing \sin(x\sin x^n) with \cos x^n yields a decidable theory.

But I still haven't found anything on the zero-variable case.

* Removing the use of log 2, pi, and noninteger rationals. Actually this can be reduced further to just -1.