mathematical logic Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...

, a first-order language of the

real numbers In mathematics, a real number is a number that can be used to measurement, measure a continuous variable, continuous one-dimensional quantity such as a time, duration or temperature. Here, ''continuous'' means that pairs of values can have arbi ...

is the set of all well-formed sentences of

first-order logic First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...

that involve universal and

existential quantifier Existentialism is a family of philosophy, philosophical views and inquiry that explore the human individual's struggle to lead an Authenticity (philosophy), authentic life despite the apparent Absurdity#The Absurd, absurdity or incomprehensibili ...

s and logical combinations of equalities and inequalities of expressions over real variables. The corresponding first-order

theory A theory is a systematic and rational form of abstract thinking about a phenomenon, or the conclusions derived from such thinking. It involves contemplative and logical reasoning, often supported by processes such as observation, experimentation, ...

is the set of sentences that are actually true of the real numbers. There are several different such theories, with different expressive power, depending on the primitive operations that are allowed to be used in the expression. A fundamental question in the study of these theories is whether they are decidable: that is, whether there is an

algorithm In mathematics and computer science, an algorithm () is a finite sequence of Rigour#Mathematics, mathematically rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algo ...

that can take a sentence as input and produce as output an answer "yes" or "no" to the question of whether the sentence is true in the theory. The theory of

real closed fields In mathematics, a real closed field is a field F that has the same first-order properties as the field of real numbers. Some examples are the field of real numbers, the field of real algebraic numbers, and the field of hyperreal numbers. Defin ...

is the theory in which the primitive operations are multiplication and addition; this implies that, in this theory, the only numbers that can be defined are the real

algebraic number In mathematics, an algebraic number is a number that is a root of a function, root of a non-zero polynomial in one variable with integer (or, equivalently, Rational number, rational) coefficients. For example, the golden ratio (1 + \sqrt)/2 is ...

s. As proven by Tarski, this theory is decidable; see

Tarski–Seidenberg theorem In mathematics, the Tarski–Seidenberg theorem states that a set in (''n'' + 1)-dimensional space defined by polynomial equations and inequalities can be projected down onto ''n''-dimensional space, and the resulting set is still defin ...

and

Quantifier elimination Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. Informally, a quantified statement "\exists x such that ..." can be viewed as a question "When is there an x such ...

. Current implementations of decision procedures for the theory of real closed fields are often based on quantifier elimination by

cylindrical algebraic decomposition In mathematics, cylindrical algebraic decomposition (CAD) is a notion, along with an algorithm to compute it, that is fundamental for computer algebra and real algebraic geometry. Given a set ''S'' of polynomials in R''n'', a cylindrical algebraic ...

. Tarski's decidable algorithm was implemented on electronic computers in the 1950s. Its runtime is too slow for it to reach any interesting results.

Tarski's exponential function problem In model theory, Tarski's exponential function problem asks whether the theory of the real numbers together with the exponential function is decidable. Alfred Tarski had previously shown that the theory of the real numbers (without the exponentia ...

concerns the extension of this theory to another primitive operation, the exponential function. It is an open problem whether this theory is decidable, but if Schanuel's conjecture holds then the decidability of this theory would follow. In contrast, the extension of the theory of real closed fields with the

sine function In mathematics, sine and cosine are trigonometric functions of an angle. The sine and cosine of an acute angle are defined in the context of a right triangle: for the specified angle, its sine is the ratio of the length of the side opposite that ...

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. In particular, one can design algorithms that are only required to terminate for input formulas that are robust, that is, formulas whose satisfiability does not change if the formula is slightly perturbed. Alternatively, it is also possible to use purely heuristic approaches.

References

{{algebraic-geometry-stub Formal theories of arithmetic Real numbers Real algebraic geometry

See also

References