Richardson's theorem

In mathematics, Richardson's theorem establishes the undecidability of the equality of real numbers defined by expressions involving integers, π,

It was proved in 1968 by the mathematician and computer scientist Daniel Richardson of the University of Bath.

[1] Richardson's theorem can be stated as follows:[2] Let E be a set of expressions that represent

[4] Miklós Laczkovich removed also the need for π and reduced the use of composition.

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.