[FOM] re: question on decidability of exponentiation and bounded sine
marker at math.uic.edu
Thu Dec 18 12:36:42 EST 2003
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
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.
More information about the FOM