[#P3134] Decidability of the real exponential field
Problem. Is the first-order theory of the ordered exponential field \(\mathbb R_{\exp}=(\mathbb R;0,1,+,\cdot,<,\exp)\) decidable?
1Context
Known frontier: R_exp is o-minimal, and a Schanuel-type conjecture yields decidability. Open boundary: An unconditional decision procedure or undecidability proof remains unknown.
2Problem setup
Definition 1 (first-order theory). All sentences in the displayed language true in the real exponential field.
Definition 2 (decidable). Membership in that set of true sentences is algorithmically decidable.
Remark 1. Tarski proved decidability for real closed fields without exp. Adding the total exponential function preserves o-minimality, yet no unconditional decision procedure is known.
3What counts as a solution
- Give a terminating algorithm deciding every sentence of R_exp.
- Or prove undecidability by an effective reduction.
1Status
Current status (Current status and exact unresolved remainder). OPEN as checked on 2026-08-01. Strongest checked neighboring result: R_exp is o-minimal, and a Schanuel-type conjecture yields decidability. Exact unresolved remainder: An unconditional decision procedure or undecidability proof remains unknown.[1][2]
1Records
Notes and companion material
Original intake status. OPEN as checked on 2026-08-01. Strongest checked neighboring result: R_exp is o-minimal, and a Schanuel-type conjecture yields decidability. Exact unresolved remainder: An unconditional decision procedure or undecidability proof remains unknown.
- Equivalent-formulation queries: decidability real exponential field open 2026; Tarski exponential function problem current status Schanuel
- Strongest checked neighboring result: R_exp is o-minimal, and a Schanuel-type conjecture yields decidability.
- Exact unresolved remainder: An unconditional decision procedure or undecidability proof remains unknown.
How the 4 records connect
ProblemDecidability of the real exponential field
2See also
How to cite
TheoremDB contributors, “Decidability of the real exponential field,” TheoremDB research memory, snapshot of August 1, 2026. https://theoremdb.org/statements/real-exponential-field-decidabilityThis page as plain text: real-exponential-field-decidability.md
This problem includes 4 records joined by 3 typed links, sourced from ris.uni-paderborn.de[1], current as of August 1, 2026.
1References
- Packet source. A. Macintyre and A. Wilkie, On the decidability of the real exponential field, Kreiseliana (1996). bibliographic record for pages 441-467. bibliographic record for pages 441-467. ↗journal article · primary source · checked 2026-08-01Source use: original summary.Proves decidability assuming a form of Schanuel's conjecture.Also cited at A. Macintyre and A. Wilkie, On the decidability of the real exponential field, Kreiseliana (1996). bibliographic record for pages 441-467.Source used to assess the problem's recorded status.For Decidability of the real exponential field: This is the dated publication status for the canonical target Decidability of the real exponential field.Source named by the research packet.
- L. van den Dries, Some results about exponential fields, survey (2024). Tarski exponential problem discussion. ↗journal article · secondary source · checked 2026-08-01Source use: original summary.Describes the decision problem as open and reviews current model theory.Source used to assess the problem's recorded status.For Decidability of the real exponential field: Describes the decision problem as open and reviews current model theory.
Original TheoremDB editorial statement and source synthesis; external works are used for citation only.