(I also asked this 18 hours ago on mathoverflow, but did not yet get any responses there.)
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?
Sun Zhi-Wei in "Reduction of unknowns in Diophantine representations", building on work by Matiyasevich and the MRDP theorem (Matiyasevich, Robinson, Davis, Putnam), has shown that solvability of Diophantine equations can be undecidable with as few as nine variables in $\mathbb{Z}$. Let $0 = D$ be any Diophantine equation with undecidable solvability and a single solution, but where the variables $x_1, x_2, ..., x_k$ of $D$ are taken to be real. Then for $0 = D + \sum_{i=1}^k \sin^2 \pi x_i$ to be satisfied, it is necessary that $(x_1, x_2, \dots, x_k) \in \mathbb{Z}^k$. I.e., this is an encoding of the problem "solve $D=0$ over the integers". By construction, it is undecidable whether this equation has a solution.