View source for Richardson's theorem

{{Short description|Undecidability of equality of real numbers}}
In [[mathematics]], '''Richardson's theorem''' establishes the [[undecidable problem|undecidability]] of the equality of [[real number]]s defined by [[expression (mathematics)|expression]]s involving [[integers]], {{pi}}, <math>\ln 2,</math> and [[exponential function|exponential]] and [[sine]] functions. It was proved in 1968 by the mathematician and computer scientist Daniel Richardson of the [[University of Bath]].

Specifically, the class of expressions for which the theorem holds is that generated by rational numbers, the number [[Pi|π]], the number [[natural logarithm|ln 2]], the variable ''x'', the operations of addition, subtraction, multiplication, [[function composition|composition]], and the [[sine|sin]], [[exponential function|exp]], and [[absolute value|abs]] functions.

For some classes of expressions generated by other primitives than in Richardson's theorem, there exist algorithms that can determine whether an expression is zero.<ref>Dan Richardson and John Fitch, 1994, "[http://portal.acm.org/citation.cfm?id=190429 The identity problem for elementary functions and constants] {{Webarchive|url=https://web.archive.org/web/20240504073813/https://consent.cookiebot.com/uc.js |date=2024-05-04 }}", Proceedings of the international symposium on Symbolic and algebraic computation, pp. 85&ndash;290.</ref>

==Statement of the theorem==
Richardson's theorem can be stated as follows:<ref>{{cite journal |zbl=0175.27404 |title=Some Undecidable Problems Involving Elementary Functions of a Real Variable |first=Daniel |last=Richardson |journal=Journal of Symbolic Logic |volume=33 |issue=4 |year=1968 |pages=514–520 |jstor=2271358 }}</ref>  
Let ''E'' be a set of expressions that represent <math>\R\to\R</math> functions. Suppose that ''E'' includes these expressions:
* ''x'' (representing the identity function)
* ''e<sup>x</sup>'' (representing the exponential functions)
* sin ''x'' (representing the sin function)
* all rational numbers, ln&nbsp;2, and π (representing constant functions that ignore their input and produce the given number as output)
Suppose ''E'' is also closed under a few standard operations. Specifically, suppose that if ''A'' and ''B'' are in ''E'', then all of the following are also in ''E'':
* ''A'' + ''B'' (representing the pointwise addition of the functions that ''A'' and ''B'' represent)
* ''A'' − ''B'' (representing pointwise subtraction)
* ''AB'' (representing pointwise multiplication)
* ''A''∘''B'' (representing the composition of the functions represented by ''A'' and ''B'')
Then the following [[decision problem]]s are unsolvable:
* Deciding whether an expression ''A'' in ''E'' represents a function that is nonnegative everywhere
* If ''E'' includes also the expression |''x''| (representing the absolute value function), deciding whether an expression ''A'' in ''E'' represents a function that is zero everywhere
* If ''E'' includes an expression ''B'' representing a function whose [[antiderivative]] has no representative in ''E'', deciding whether an expression ''A'' in ''E'' represents a function whose antiderivative can be represented in ''E''. (Example: <math>e^{ax^2}</math> has an antiderivative in the [[elementary function]]s if and only if {{math|1=''a'' = 0}}.)

==Extensions==
After [[Hilbert's tenth problem]] was solved in 1970, B. F. Caviness observed that the use of ''e<sup>x</sup>'' and ln 2 could be removed.<ref>{{cite journal |title=On Canonical Forms and Simplification |first=B. F. |last=Caviness |journal=Journal of the ACM |volume=17 |issue=2 |year=1970 |pages=385–396 |doi=10.1145/321574.321591 |doi-access=free }}</ref>
Wang later noted that under the same assumptions under which the question of whether there was ''x'' with ''A''(''x'') < 0 was insolvable, the question of whether there was ''x'' with ''A''(''x'') = 0 was also insolvable.<ref>{{cite journal |first=P. S. |last=Wang |title=The undecidability of the existence of zeros of real elementary functions |journal=Journal of the Association for Computing Machinery |volume=21 |issue=4 |year=1974 |pages=586–589 |doi=10.1145/321850.321856 |doi-access=free }}</ref>

[[Miklós Laczkovich]] removed also the need for π and reduced the use of composition.<ref>{{cite journal |first=Miklós |last=Laczkovich |title=The removal of π from some undecidable problems involving elementary functions |journal=Proc. Amer. Math. Soc. |volume=131 |issue=7 |year=2003 |pages=2235–2240 |doi=10.1090/S0002-9939-02-06753-9 |doi-access=free }}</ref>  In particular, given an expression ''A''(''x'') in the ring generated by the integers, ''x'', sin ''x<sup>n</sup>'', and sin(''x'' sin ''x<sup>n</sup>'') (for ''n'' ranging over positive integers), both the question of whether ''A''(''x'') > 0 for some ''x'' and whether ''A''(''x'') = 0 for some ''x'' are unsolvable.

By contrast, the [[Tarski–Seidenberg theorem]] says that the first-order theory of the real field is decidable, so it is not possible to remove the sine function entirely.

==See also==

* {{annotated link|Constant problem}}
* {{annotated link|Elementary function}}
* {{annotated link|Tarski's high school algebra problem}}

==References==

{{reflist}}

==Further reading==

* {{cite book |last1=Petkovšek |first1=Marko |author-link1=Marko Petkovšek |last2=Wilf |first2=Herbert S. |author-link2=Herbert S. Wilf |last3=Zeilberger |first3=Doron |author-link3=Doron Zeilberger |title=A&nbsp;=&nbsp;B |publisher=[[A. K. Peters]] |url=http://www.cis.upenn.edu/~wilf/AeqB.html |year=1996 |isbn=1-56881-063-6 |pages=212 |url-status=dead|archive-url=https://web.archive.org/web/20060129095451/http://www.cis.upenn.edu/~wilf/AeqB.html |archive-date=2006-01-29 }}

==External links==

* {{MathWorld|urlname=RichardsonsTheorem|title=Richardson's theorem}}

{{Mathematical logic}}

[[Category:Undecidable problems]]
[[Category:Functions and mappings]]
[[Category:Theorems in the foundations of mathematics]]