mathematical logic Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of forma ...

, a first-order language of the

real numbers In mathematics, a real number is a number that can be used to measure a ''continuous'' one-dimensional quantity such as a distance, duration or temperature. Here, ''continuous'' means that values can have arbitrarily small variations. Every re ...

is the set of all well-formed sentences of

first-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...

that involve

universal Universal is the adjective for universe. Universal may also refer to: Companies * NBCUniversal, a media and entertainment company ** Universal Animation Studios, an American Animation studio, and a subsidiary of NBCUniversal ** Universal TV, a t ...

and

existential quantifier In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some". It is usually denoted by the logical operator symbol ∃, which, w ...

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

theory A theory is a rational type of abstract thinking about a phenomenon, or the results of such thinking. The process of contemplative and rational thinking is often associated with such processes as observational study or research. Theories may ...

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, is there an

algorithm In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing ...

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 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 An algebraic number is a number that is a root of a non-zero polynomial in one variable with integer (or, equivalently, rational) coefficients. For example, the golden ratio, (1 + \sqrt)/2, is an algebraic number, because it is a root of th ...

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 defi ...

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 \ldots" can be viewed as a question "When is there an x such t ...

. 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, and an algorithm to compute it, that are fundamental for computer algebra and real algebraic geometry. Given a set ''S'' of polynomials in R''n'', a cylindrical algebraic decom ...

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 exponent ...

concerns the extension of this theory to another primitive operation, the

exponential function The exponential function is a mathematical function denoted by f(x)=\exp(x) or e^x (where the argument is written as an exponent). Unless otherwise specified, the term generally refers to the positive-valued function of a real variable, ...

. It is an open problem whether this theory is decidable, but if

Schanuel's conjecture In mathematics, specifically transcendental number theory, Schanuel's conjecture is a conjecture made by Stephen Schanuel in the 1960s concerning the transcendence degree of certain field extensions of the rational numbers. Statement The con ...

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 that is opp ...

is undecidable since this allows encoding of the undecidable theory of integers (see

Richardson's theorem In mathematics, Richardson's theorem establishes the undecidability of the equality of real numbers defined by expressions involving integers, , \ln 2, and exponential and sine functions. It was proved in 1968 by mathematician and computer scient ...

). 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 Robustness is the property of being strong and healthy in constitution. When it is transposed into a system, it refers to the ability of tolerating perturbations that might affect the system’s functional body. In the same line ''robustness'' ca ...

, 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