(I asked this a little over 3 months ago on math.SE, and when I initially re-asked here, no one had responded there. $\:$ After I re-asked here, Eric Towers responded there, since I had forgotten to give a link to here. $\:$ However, his response uses a construction whose expressions are not constants.)
Richardson's theorem is given in this wikipedia article. $\:$ In this answer, Eric Towers states that
- An algebraic expression is decidable. This is also the Tarski-Seidenberg theorem.
- Algebraic expressions plus $\exp$ are decidable if Schanuel's conjecture holds.
Otherwise, this is unknown. See Tarski's exponential function problem.- Throw in sine and determining whether the constant expression vanishes is undecidable. (This can be linked to the undecidability of models of the integers (a la
Godel's Incompleteness Theorems) via the zeroes of $\sin (\pi k)$ for any integer $k$.
See Hilbert's Tenth Problem and Matiyasevich's Theorem.)
Sine isn't critical; any (real-)periodic function would do.
.
How can the last bullet point of that quote be proven?