equivalent means that the two formulas are true for exactly the same values of the variables. The Tarski–Seidenberg theorem is an extension of the decidability theorem, as it can be easily checked whether a quantifier-free formula without free variables is true or false. This theorem can be further extended to the following projection theorem. If is a real closed field, a formula with free variables defines a subset of , the set of the points that satisfy the formula. Such a subset is called a semialgebraic set. Given a subset of variables, the projection from to is the function that maps every -tuple to the -tuple of the components corresponding to the subset of variables. The projection theorem asserts that a projection of a semialgebraic set is a semialgebraic set, and that there is an algorithm that, given a quantifier-free formula defining a semialgebraic set, produces a quantifier-free formula for its projection. In fact, the projection theorem is equivalent to quantifier elimination, as the projection of a semialgebraic set defined by the formula is defined by where and represent respectively the set of eliminated variables, and the set of kept variables. The decidability of a first-order theory of the real numbers depends dramatically on the primitive operations and functions that are considered (here addition and multiplication). Adding other functions symbols, for example, the sine or the exponential function, can provide undecidable theories; see Richardson's theorem and Decidability of first-order theories of the real numbers. Complexity of deciding 𝘛rcf Tarski's original algorithm for quantifier elimination has nonelementary computational complexity, meaning that no tower can bound the execution time of the algorithm if is the size of the input formula. The cylindrical algebraic decomposition, introduced by George E. Collins, provides a much more practicable algorithm of complexity where is the total number of variables (free and bound), is the product of the degrees of the polynomials occurring in the formula, and is big O notation. Davenport and Heintz (1988) proved that this worst-case complexity is nearly optimal for quantifier elimination by producing a family of formulas of length , with quantifiers, and involving polynomials of constant degree, such that any quantifier-free formula equivalent to must involve polynomials of degree and length where is big Omega notation. This shows that both the time complexity and the space complexity of quantifier elimination are intrinsically double exponential. For the decision problem, Ben-Or, Kozen, and Reif