In the book A=B, the authors point out that while the identity
is provable (by a very simple proof!), it’s not possible to prove the truth or falsity of all such identities. This is because Daniel Richardson proved the following:
Let denote the class of expressions generated by
- The rational numbers, and .
- The variable
- The operations of addition, multiplication, and composition.
- The sine, exponential, and absolute value functions.
Then the problem of deciding whether or not an expression in is identically zero is undecidable. This means as well that the problem of deciding whether or not two expressions are always equal is also undecidable, since this is equivalent to deciding if is identically zero.
A summary of Richardson’s proof (mostly from Richardson’s paper itself) is below.
For all , iff there exist such that .
At the time that Richardson proved his result, the MDRP theorem was not proven. Instead, only the weaker result where is allowed to be an exponential polynomial (i.e., the are allowed to appear as exponents in ) had been proven, and so that’s what he used. I haven’t read Richardson’s proof closely enough to determine if his result can be improved using the full MDRP theorem.
In any case, since there are recursively enumerable sets which are not decidable, we may let be an exponential polynomial such that the problem of deciding, given , whether or not there are such that is undecidable.
Therefore, the problem of deciding, given , whether or not there are non-negative real numbers such that
Now, let be an exponential polynomial which grows very fast (and such that is very large). Then, if is a natural number and there are non-negative reals such that
is less than one, then both and are small. From this last fact, we conclude that each is close to a natural number. Let be the natural number closest to . Then, will be small. But then, because it’s an integer, it will be zero.
Therefore, we have an expression formed from sine and exponential functions (and rational numbers, addition, and multiplication) such that for each , there exist non-negative reals such that iff there exist natural numbers such that (which is an undecidable problem).
By an argument which I won’t reproduce here, we can replace with with the property that for each there exists a real such that iff there exist natural numbers such that . (Notice that now ranges over all reals.) But now, consider the sequence of functions
Each is identically zero iff the corresponding is ever less than zero, which is an undecidable problem.
The reference for Richardson’s paper is: Daniel Richardson, “Some unsolvable problems involving elementary functions of a real variable,” Journal of Symbolic Logic, Volume 33, 1968, pages 514–520
Another reference is: B.F. Caviness, “On canonical forms and simplification,” Journal of the ACM, volume 17, 1970, pages 385–396.