MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

If yes, how? Also, I know you can't do it for arbitrary statements about real numbers, but that's not what I'm asking, and by "real" numbers, I mean the numbers constructible from 1, -, /, and the operations mentioned in the title.

Also, I don't care about numbers that can't be constructed from said operations and constant.

share|cite|improve this question
Note: I added the "lo.logic" and "algorithms" tags to the question. – Gro-Tsen Jan 15 '13 at 18:55
If the answer is yes, then the next question is if it is NPC. – Lucas K. Jan 19 '13 at 23:46
up vote 11 down vote accepted

Assuming Schanuel's conjecture, the answer seems to be yes, according to Daniel Richardson, "How to recognize zero" J. Symbolic Comput 24 (1997), 627–645 (doi:10.1006/jsco.1997.0157, available here online), in which the author defines a set of numbers he calls "elementary", which is algebraically closed and closed under exponential, logarithm and trigonometric functions, and for which equality is decidable (again, assuming Schanuel's conjecture).

share|cite|improve this answer
The OP also asked, "If yes, how?" Even assuming that Schanuel's conjecture is true, I assume that no practical, general algorithm will never be found. Even in the much simpler case of the real field, Tarski only proved that the theory was decidable; he didn't explicitly construct a practical algorithm. – Ben Crowell Jan 15 '13 at 19:36
Well, Tarski did explicitly construct an algorithm (and even implemented it at some point), but it’s prohibitively slow. Better results are known, in particular, the theory of the reals is decidable in exponential space (and doubly exponential time). Its existential fragment is decidable in polynomial space, and it’s an open problem whether it’s possible to get it down to the polynomial hierarchy. – Emil Jeřábek Jan 15 '13 at 20:09
@Ben Crowell: The cited article by Richardon does give an explicit algorithm, and claims that it was implemented and is actually usable. – Gro-Tsen Jan 15 '13 at 22:34

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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