Tarski's exponential function problem

Last updated

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 exponential function) is decidable. [1]

Contents

The problem

The ordered real field R is a structure over the language of ordered rings Lor = (+,·,−,<,0,1), with the usual interpretation given to each symbol. It was proved by Tarski that the theory of the real field, Th(R), is decidable. That is, given any Lor-sentence φ there is an effective procedure for determining whether

He then asked whether this was still the case if one added a unary function exp to the language that was interpreted as the exponential function on R, to get the structure Rexp.

Conditional and equivalent results

The problem can be reduced to finding an effective procedure for determining whether any given exponential polynomial in n variables and with coefficients in Z has a solution in Rn. Macintyre & Wilkie (1995) showed that Schanuel's conjecture implies such a procedure exists, and hence gave a conditional solution to Tarski's problem. [2] Schanuel's conjecture deals with all complex numbers so would be expected to be a stronger result than the decidability of Rexp, and indeed, Macintyre and Wilkie proved that only a real version of Schanuel's conjecture is required to imply the decidability of this theory.

Even the real version of Schanuel's conjecture is not a necessary condition for the decidability of the theory. In their paper, Macintyre and Wilkie showed that an equivalent result to the decidability of Th(Rexp) is what they dubbed the Weak Schanuel's Conjecture. This conjecture states that there is an effective procedure that, given n ≥ 1 and exponential polynomials in n variables with integer coefficients f1,..., fn, g, produces an integer η ≥ 1 that depends on n, f1,..., fn, g, and such that if α ∈ Rn is a non-singular solution of the system

then either g(α) = 0 or |g(α)| > η−1.

Related Research Articles

In mathematical logic, model theory is the study of the relationship between formal theories, and their models. The aspects investigated include the number and size of models of a theory, the relationship of different models to each other, and their interaction with the formal language itself. In particular, model theorists also investigate the sets that can be defined in a model of a theory, and the relationship of such definable sets to each other. As a separate discipline, model theory goes back to Alfred Tarski, who first used the term "Theory of Models" in publication in 1954. Since the 1970s, the subject has been shaped decisively by Saharon Shelah's stability theory.

Hilbert's tenth problem is the tenth on the list of mathematical problems that the German mathematician David Hilbert posed in 1900. It is the challenge to provide a general algorithm that, for any given Diophantine equation, can decide whether the equation has a solution with all unknowns taking integer values.

<span class="mw-page-title-main">Diophantine approximation</span> Rational-number approximation of a real number

In number theory, the study of Diophantine approximation deals with the approximation of real numbers by rational numbers. It is named after Diophantus of Alexandria.

In mathematics, a Pisot–Vijayaraghavan number, also called simply a Pisot number or a PV number, is a real algebraic integer greater than 1, all of whose Galois conjugates are less than 1 in absolute value. These numbers were discovered by Axel Thue in 1912 and rediscovered by G. H. Hardy in 1919 within the context of Diophantine approximation. They became widely known after the publication of Charles Pisot's dissertation in 1938. They also occur in the uniqueness problem for Fourier series. Tirukkannapuram Vijayaraghavan and Raphael Salem continued their study in the 1940s. Salem numbers are a closely related set of numbers.

In mathematics, an expression or equation is in closed form if it is formed with constants, variables and a finite set of basic functions connected by arithmetic operations and function composition. Commonly, the allowed functions are nth root, exponential function, logarithm, and trigonometric functions. However, the set of basic functions depends on the context.

In mathematics, a homogeneous function is a function of several variables such that the following holds: If each of the function's arguments is multiplied by the same scalar, then the function's value is multiplied by some power of this scalar; the power is called the degree of homogeneity, or simply the degree. That is, if k is an integer, a function f of n variables is homogeneous of degree k if

In computational complexity theory, a function problem is a computational problem where a single output is expected for every input, but the output is more complex than that of a decision problem. For function problems, the output is not simply 'yes' or 'no'.

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.

Transcendental number theory is a branch of number theory that investigates transcendental numbers, in both qualitative and quantitative ways.

<span class="mw-page-title-main">Schanuel's conjecture</span> Conjecture on the transcendence degree of field extensions to the rational numbers

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.

In mathematics, the resultant of two polynomials is a polynomial expression of their coefficients that is equal to zero if and only if the polynomials have a common root, or, equivalently, a common factor. In some older texts, the resultant is also called the eliminant.

In mathematical logic, a definable set is an n-ary relation on the domain of a structure whose elements satisfy some formula in the first-order language of that structure. A set can be defined with or without parameters, which are elements of the domain that can be referenced in the formula defining the relation.

<span class="mw-page-title-main">Angus Macintyre</span> British mathematician and logician

Angus John Macintyre FRS, FRSE is a British mathematician and logician who is a leading figure in model theory, logic, and their applications in algebra, algebraic geometry, and number theory. He is Emeritus Professor of Mathematics, at Queen Mary University of London.

In mathematics, an exponential field is a field with a further unary operation that is a homomorphism from the field's additive group to its multiplicative group. This generalizes the usual idea of exponentiation on the real numbers, where the base is a chosen positive real number.

In mathematical logic, Tarski's high school algebra problem was a question posed by Alfred Tarski. It asks whether there are identities involving addition, multiplication, and exponentiation over the positive integers that cannot be proved using eleven axioms about these operations that are taught in high-school-level mathematics. The question was solved in 1980 by Alex Wilkie, who showed that such unprovable identities do exist.

In mathematics, Wilkie's theorem is a result by Alex Wilkie about the theory of ordered fields with an exponential function, or equivalently about the geometric nature of exponential varieties.

In transcendental number theory, a mathematical discipline, Baker's theorem gives a lower bound for the absolute value of linear combinations of logarithms of algebraic numbers. Nearly fifteen years earlier, Alexander Gelfond had considered the problem with only integer coefficients to be of "extraordinarily great significance". The result, proved by Alan Baker, subsumed many earlier results in transcendental number theory. Baker used this to prove the transcendence of many numbers, to derive effective bounds for the solutions of some Diophantine equations, and to solve the class number problem of finding all imaginary quadratic fields with class number 1.

In mathematical logic, a first-order language of the real numbers is the set of all well-formed sentences of first-order logic that involve universal and existential quantifiers and logical combinations of equalities and inequalities of expressions over real variables. The corresponding first-order theory 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 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.

<span class="mw-page-title-main">Constant-recursive sequence</span> Infinite sequence of numbers satisfying a linear equation

In mathematics, an infinite sequence of numbers is called constant-recursive if it satisfies an equation of the form

In mathematics, an ordered exponential field is an ordered field together with a function which generalises the idea of exponential functions on the ordered field of real numbers.

References

  1. ↑ Kuhlmann, S. "Model theory of the real exponential function". Encyclopedia of Mathematics. Heidelberg: Springer-Verlag. Retrieved 2024-08-07.
  2. ↑ Macintyre, Angus; Wilkie, Alex (1996). Oddifreddi, Piergiorgio (ed.). On the Decidability of the Real Exponential Field, in: Kreiseliana: about and around Georg Kreisel. Wellesley, MA: A K Peters. pp. 441–467. ISBN   9781568810614. MR   1435773. Zbl   0896.03012.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.