# Is equality of terms for “real” numbers with roots, logarithm, exponential, sin, cos, and other trigonometric operations decidable with a Turing-machine?

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.

-
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

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

-
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