[FOM] re: question on decidability of exponentiation and bounded sine

[Dave Marker]

Dmytro Taranovsky asks:

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

I believe this interesting question is still open.

Macintyre and Wilkie showed that the theory of the reals with
exponentiation is decidably assuming Schanuel's Conjecture
(if x_1,...,x_n are complex numbers linearly independent over the
rationals then the field generated by x_1,..x_n,exp(x_1),...,exp(x_n)
has transcendence degree at least n over the rationals.)

It's hard to imagine a proof along these lines once we have
restricted sine.

There are other interesting open questions here. We know
that the theory of the reals with exponentiation is model complete
and hence is axiomatized by Pi_2-sentences, but we have no real
clue what this axiomatization would be. The Macintyre-Wilkie
axiomatization has sentences of arbitrary complexity.

Dave Marker