Tarski's Exponential Function Problem

Tarski's Exponential Function Problem

Definitions and mathematical statement

A first-order sentence in the real exponential field is built from real variables, the constants $0,1$, addition, multiplication, order, equality, and the usual real function $\exp$, using Boolean operations and quantifiers over ${\mathbb{R}}$. Let \[ \operatorname{Th}({\mathbb{R}}_{\exp})=\{\ulcorner\varphi\urcorner:({\mathbb{R}};0,1,+,\cdot,\exp,<)\models\varphi\}. \] The question is whether this set of finite encodings is decidable by an algorithm halting on every input. It concerns arbitrary quantifier alternation, not only an existential fragment, and imposes no complexity bound.

Formulation and concept references: [S1].

Short English statement

Can a terminating algorithm decide every first-order statement about real arithmetic with the exponential function?

Research attempt

Current frontier.

The supplied STACS 2025 paper distinguishes Tarski's full exponential field problem from its own existential extension by integer powers. Its introductory root-barrier conjecture gives a useful formulation of the effective zero-testing obstacle. [S1], Section 1, Conjecture 2. Berarducci--Gallinaro's June 2026 revision gives a new axiomatization and decidability argument assuming the real form of Schanuel's conjecture; an unconditional restricted model-completeness theorem in that paper is not an unconditional solution of the full decision problem. [E1], introduction and Theorems 12.4 and 14.4. The following attempt separates effective transformations actually available from transcendence hypotheses not proved here.

Attack routes.

One may algebraize exponential terms by changing variables, use certified numerical root isolation, or enumerate consequences of an effective complete axiomatization. The first route must cope with variables appearing both outside and inside exponentials. The second needs an effective gap between zero and a small nonzero value, including singular roots. The third needs completeness, not just a recursively enumerable sound list of axioms. We develop an exact algebraizable fragment and then examine the missing zero test.

Attempt I: an all-quantifier decidable fragment.

Consider sentences whose atomic expressions are rational polynomials in terms \[ \exp(r_1x_1+\cdots+r_sx_s),\qquad r_i\in{\mathbb{Q}}, \] with arbitrary Boolean combinations and quantifier alternation. Require that the variables occur only in these homogeneous rational linear exponents. There are no bare $x_i$, no nested exponentials, and no nonzero constant terms inside the exponent. These restrictions define a fragment of the target language, not a replacement for it.

Take a positive integer $D$ divisible by all coefficient denominators and substitute $y_i=\exp(x_i/D)$. This is a bijection from ${\mathbb{R}}$ to ${\mathbb{R}}_{>0}$ in each coordinate. If $r_i=a_i/D$, then \[ \exp\!\left(\sum_i r_i x_i\right)=\prod_i y_i^{a_i}. \] Every atom becomes a comparison of rational Laurent polynomials. Multiplying both sides of an atomic equality or inequality by a sufficiently large positive monomial clears all negative exponents without changing its truth value. Replace quantifiers by \[ \exists x_i\,\varphi\ \rightsquigarrow\ \exists y_i\,(y_i>0\wedge\varphi^*),\qquad \forall x_i\,\varphi\ \rightsquigarrow\ \forall y_i\,(y_i>0\Rightarrow\varphi^*). \] By structural induction on the formula, this transformation preserves truth, including every quantifier alternation. It terminates after finite rational arithmetic. The resulting sentence lies in the theory of real closed fields, whose decision procedure is the classical Tarski result recalled in [E1], Section 1.

For example, the sentence $\forall x\,\exists z\,[e^{x/2}e^z=1]$ becomes $\forall y>0\,\exists w>0\,[yw^2=1]$ with $D=2$ and is true. The equally elementary-looking equation $e^x=x+2$ lies outside the fragment: after the substitution, the right side contains $D\log y+2$. Introducing a symbol for $\log$ merely restores the original transcendental relation. Adding arbitrary exponential constants also requires deciding their exact algebraic relations, which the transformation did not do.

Attempt II: what numerical certification can decide.

Let $f_1,\ldots,f_r$ be specified exponential-polynomial expressions on a compact rational box $B$. Bounds on their derivatives can be computed recursively from rational arithmetic and upper bounds on the exponential function on bounded intervals. Consequently $F(x)=\min_i f_i(x)$ has a computable Lipschitz constant $L$. For a supplied rational $\delta>0$, the following promise problem is decidable: \[ \max_{x\in B}F(x)\geq\delta \quad\hbox{versus}\quad \max_{x\in B}F(x)\leq-\delta. \] Choose a finite rational grid with covering radius at most $\delta/(4\max(1,L))$ and evaluate each $F$ to error at most $\delta/4$. The grid maximum differs from the true maximum by at most $\delta/2$. Its sign distinguishes the two cases. Every operation terminates; the number of grid points can be large but the original task imposes no complexity bound.

This procedure is not a solution of the unrestricted existential problem. If the maximum is zero, no fixed positive promise gap applies. Nor does it decide unbounded searches by checking successively larger boxes: an empty set provides no automatic stopping certificate. For $f(x)=e^x-x-1$, the exact zero at $x=0$ is singular since $f'(0)=0$. Interval errors getting smaller around that value do not alone certify whether a perturbed expression is exactly zero.

The root-barrier assertion in the formulation source is more targeted. Given integer exponential polynomials $f_1,\ldots,f_n,g$, it asks for an effective positive integer $t$ such that at every nonsingular real zero $\alpha$ of the $f_i$ one has either $g(\alpha)=0$ or $|g(\alpha)|>1/t$. [S1], Conjecture 2. If this $t$ and certified arbitrarily accurate approximations to an isolated such $\alpha$ were available, evaluating $g(\alpha)$ within $1/(4t)$ would distinguish the two alternatives by the threshold $1/(2t)$. This implication is elementary and exact. The unproved part is an algorithm producing the uniform $t$ with the source's quantifiers, not the final comparison. The presence of only finitely many values in some isolated calculation would not supply such an effective bound uniformly across inputs.

Attempt III: testing the proof-enumeration route.

Suppose $T$ were a recursively enumerable, sound, complete axiomatization of $\operatorname{Th}({\mathbb{R}}_{\exp})$. Dovetail proof searches for $\varphi$ and $\neg\varphi$. Soundness prevents both from appearing, and completeness guarantees that one appears, yielding a decision procedure. If completeness is omitted, neither search need halt. Thus writing down plausible differential axioms for an ordered exponential field does not establish decidability.

The recent paper proves the required completeness for its indicated axioms only under $\mathrm{SC}_{{\mathbb{R}}}$, the real Schanuel assertion about transcendence degree of linearly independent real tuples and their exponentials. That hypothesis has not been proved in this notebook. The paper's unconditional model completeness in a restricted setting cannot be substituted for the full completeness statement. [E1], Theorems 12.4, 14.2 and 14.4.

Stress test.

The algebraic change of variables is globally bijective on each quantified coordinate; it is not just a local analytic substitution. Cleared denominators are positive, so inequality directions are preserved. The fragment excludes exactly the mixed ordinary/exponential occurrences that would reintroduce logarithms. The finite-grid algorithm states its promise and compact domain explicitly, rather than mistaking a semidecision procedure for a halting algorithm on every sentence. The root-barrier discussion includes nonsingularity and an effective bound; qualitative isolation alone is not enough.

The companion symbolic checks verify Laurent identities and positive monomial clearing on examples. They are not an implementation of a full real-exponential decision procedure or a test of Schanuel's conjecture. No finite precision convention is allowed to identify a small value with zero in the mathematical argument.

Outcome.

Outcome: Exploratory approach with unresolved gap.

An explicit all-quantifier fragment has been reduced effectively to real closed fields, and a robust compact-domain promise problem has a proved grid algorithm. Neither includes arbitrary mixed exponential sentences. The precise missing zero-barrier/completeness inputs have been isolated, with their dependence on an unresolved transcendence hypothesis retained. The original decidability question is not resolved, and no novelty claim is made for these fragment arguments.

Sources

• S1 Jorge Gallego-Hernandez, Alessio Mansutti, "On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number," 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025), LIPIcs vol. 327, Article 37, pp. 37:1-37:18. https://drops.dagstuhl.de/storage/00lipics/lipics-vol327-stacs2025/LIPIcs.STACS.2025.37/LIPIcs.STACS.2025.37.pdf. Catalogue formulation source.
• E1 Alessandro Berarducci and Francesco Gallinaro. On the elementary theory of the real exponential field, arXiv:2603.08365v2, 23 June 2026. Theorems 12.4, 14.2 and 14.4. Restricted model completeness is unconditional; the full completeness and decidability conclusions retain the real Schanuel hypothesis. https://arxiv.org/html/2603.08365v2. Consulted 27 September 2026 for the indicated result or scope.