Decidability of first-order theories of the real numbers
The corresponding first-order theory is the set of sentences that are actually true of the real numbers.As proven by Tarski, this theory is decidable; see Tarski–Seidenberg theorem and Quantifier elimination.Current implementations of decision procedures for the theory of real closed fields are often based on quantifier elimination by cylindrical algebraic decomposition.[2][3] In contrast, the extension of the theory of real closed fields with the sine function is undecidable since this allows encoding of the undecidable theory of integers (see Richardson's theorem).Still, one can handle the undecidable case with functions such as sine by using algorithms that do not necessarily terminate always.