Math Conjectures

Decidability of the Real Exponential Field

OPENLandmarkOpen problemProposed c. 1950 · Full conjecture

Canonical statement

There exists an algorithm which, given any first-order sentence φ\varphi in the language {0,1,+,⋅,<,exp⁡}\{0,1,+,\cdot,<,\exp\}, halts and correctly decides whether
(R;0,1,+,⋅,<,x↦ex)⊨φ. (\mathbb R;0,1,+,\cdot,<,x\mapsto e^x)\models\varphi .
View source LaTeX
There exists an algorithm which, given any first-order sentence \(\varphi\) in the language \(\{0,1,+,\cdot,<,\exp\}\), halts and correctly decides whether
\[
  (\mathbb R;0,1,+,\cdot,<,x\mapsto e^x)\models\varphi .
\]
LOG-DEC-005:[Tarski1951Decision][Wilkie1996ModelComplete][MacintyreWilkie1996][BerarducciGallinaro2026Rexp]
Logic and foundationsNumber theory

Notes

Tarski showed that the first-order theory of the ordered field of real numbers is decidable, and around 1950 his decision program raised the question of whether the same holds when the exponential function is added to the structure [Tarski1951Decision]. The problem asks for an algorithm that decides every first-order sentence of (R;0,1,+,⋅,<,x↦ex)(\mathbb R;0,1,+,\cdot,<,x\mapsto e^x).

Wilkie proved that the real exponential field is model complete and o-minimal, so its definable sets are geometrically tame [Wilkie1996ModelComplete]. Building on this, Macintyre and Wilkie showed that the theory is decidable provided an appropriate real form of Schanuel's conjecture from transcendental number theory holds [MacintyreWilkie1996]. Recent work continues to analyze the elementary theory of the real exponential field and the reach of these methods [BerarducciGallinaro2026Rexp].

Decidability is therefore known conditionally, and the obstruction is number-theoretic rather than model-theoretic: an unconditional algorithm appears to require progress on transcendence questions of Schanuel type. The problem remains open.

References (4)

The boxed statement is the canonical open formulation — not a stronger variant or a related research program. The status reflects the catalog's last review; do your own literature search before investing serious effort.