[FOM] Question on Decidability of Exponentiation and Bounded Sine

[Dmytro Taranovsky]

Is the first order theory of real numbers under addition,
multiplication, exponentiation, and sine, where sine is restricted to
[-1,1] (and returns zero when the argument is out of bounds), decidable?

The region of restriction of sine, as long as it is a finite segment
with rational endpoints, does not affect decidability.  However, the
full theory of real numbers under addition, multiplication, and sine is
undecidable.  The theory of real numbers under addition, multiplication,
and exponentiation is decidable provided that no surprising identity
(like e^e=15) holds.

The question is part of a broader issue, namely how much of mathematics
is part of a decidable theory.  An affirmative answer to the question
above would mean that most of precalculus is decidable.

Sincerely,
Dmytro Taranovsky
http://web.mit.edu/dmytro/www/main.htm