Decidability of checking an antiderivative?

Let's suppose I have two functions $F$ and $G$ and I'm interested in determining whether

$$F(x) = \int G(x)dx.$$

Let's suppose that my functions are composed of elementary functions (polynomials, exponentials, logs, and trigonometric functions), but not, say, Taylor series.

Is this problem decidable? If not, it is it semidecidable?

(I'm asking because I'm teaching a class on computability and a student asked me if a TM could help you integrate a function whose integral was not currently known. I suspect that the functions we don't know how to integrate are more properly functions whose integral can't be expressed as a combination of the above elementary functions rather than functions for which we don't actually know the integral, but that got me thinking about whether the general problem of checking integrals was decidable.)

The short answer to your question is "no". Richardson's theorem and its later extensions basically state that as soon as you include the elementary trigonometric functions, the problem of deciding if $f(x) = 0$ (and hence if $f(x) = g(x)$, since this is the same as $f(x) - g(x) = 0$) is unsolvable.

What's interesting about this is that the first-order theory of real closed fields is decidable. Intuitively, the reason why adding trigonometric functions makes the first-order system undecidable is because you can construct the integers via $\{ x \in R : \sin(\pi x) = 0 \}$, and the theory of the integers is undecidable.

Whether or not the theory of real closed fields with $e^x$ is decidable is a fairly famous open problem.

Even more interesting that this is that if you had an oracle which "solved" the constant problem (i.e. an oracle which can tell you if $f(x) = 0$ or not), then integration of elementary functions in finite terms is decidable, and a practical algorithm is known. So given $G(x)$, we could find $F(x)$ or know that there is no elementary integral of $G$ in finite terms.

StackExchange Computer Science Q#49413, answer score: 9