Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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|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

1 Answer 1

up vote 10 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|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
1  
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
2  
@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

 
discard

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.