Welcome to MathOverflow

Question

5

1

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.

edited Jan 15 at 18:55

Gro-Tsen
928●3●13

asked Jan 15 at 13:59

tailcalled
53●3

	Note: I added the "lo.logic" and "algorithms" tags to the question. – Gro-Tsen Jan 15 at 18:55
	If the answer is yes, then the next question is if it is NPC. – Lucas K. Jan 19 at 23:46

Gro-Tsen · Accepted Answer · 2013-01-15 18:50:33Z UTC

9

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

answered Jan 15 at 18:50

Gro-Tsen
928●3●13

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 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 at 20:09

1

@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 at 22:34

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

Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

1 Answer

You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.