Unconditional decidability of the real exponential field and the Igusa–Knight–Schweber General Theorem over the dyadic-interval structure $\mathcal{R}_{int}$

This problem collects two independent unresolved issues concerning the decidability and generic computing strength of structures on the real numbers. Part A is Tarski's long-standing question whether the complete first-order theory of the real exponential field, $T_{\exp}=\mathrm{Th}(\mathbb{R};+,\cdot,<,0,1,\exp)$, is decidable without unproved hypotheses. Macintyre and Wilkie proved decidability assuming the real form of Schanuel's Conjecture and showed decidability to be equivalent to a weak first-order form of it; Berarducci and Gallinaro (2026) re-derived the conditional decidability from a new axiomatization; but no unconditional resolution is known. Part B arises from the study of Igusa, Knight and Schweber on the generic computing strength of structures on the real numbers (J. Symb. Log. 82(1), 2017) and asks for a complete proof of the interval-structure analogue of their General Theorem: every o-minimal expansion, in a countable language with definable Skolem functions, of the structure $\mathcal{R}_{int}$ (the reals with the order and predicates for the half-open dyadic intervals) is generically Muchnik reducible to $\mathcal{R}_{int}$. The source paper proved only the degree equivalences $\mathcal{B}\equiv^*_w\mathcal{R}_{int}\equiv^*_w\mathcal{R}_{\mathbb{Q}}$ and outlined, without proof, the modification of its argument. Both parts are open as of September 2026.

Background

The real exponential field is the structure $\mathcal{R}_{\exp}=(\mathbb{R};+,\cdot,<,0,1,\exp)$, and $T_{\exp}$ denotes its complete first-order theory: the set of all sentences of the language $\{+,\cdot,<,0,1,\exp\}$ true in the reals with exponentiation. Tarski's 1951 decision method for elementary algebra and geometry established that the theory of the real closed field $(\mathbb{R};+,\cdot,<)$ is decidable, and asked whether decidability persists when exponentiation is added to the language. Wilkie (1996) proved that $T_{\exp}$ is model complete — every definable set is a projection of a set defined by an equation $p(x_1,\dots,x_n,e^{x_1},\dots,e^{x_n})=0$ with $p$ a polynomial — which makes $\mathcal{R}_{\exp}$ o-minimal: every definable subset of the real line is a finite union of points and intervals. Model completeness, however, is non-effective and yields no decision procedure.

The obstacle is arithmetic. Schanuel's Conjecture in its real form (SCR) asserts that whenever $x_1,\dots,x_n$ are $\mathbb{Q}$-linearly independent reals, the $2n$-tuple $x_1,\dots,x_n,e^{x_1},\dots,e^{x_n}$ has transcendence degree at least $n$ over $\mathbb{Q}$. Macintyre and Wilkie (1996) proved that SCR implies decidability of $T_{\exp}$: under SCR there is an algorithm deciding whether an exponential polynomial over $\mathbb{Q}$ has a real zero, and this suffices for the full theory; Wilkie (1997) described the resulting conditional algorithm. They also showed that decidability of $T_{\exp}$ is equivalent to a weak first-order axiom-scheme form of the conjecture (the Weak Schanuel scheme), as recalled in Berarducci–Gallinaro (2026). Recent work sharpens only the conditional picture: Krapp (2024) proved under Schanuel's Conjecture that the prime model of real exponentiation (the unique smallest model of the theory) embeds into every o-minimal exponential field; Berarducci–Gallinaro (2026) proved under SCR that $T_{\exp}$ is axiomatized by the axioms of definably complete exponential fields — definably complete meaning that every bounded definable subset of the domain has a least upper bound — satisfying $\exp'=\exp$, re-deriving the Macintyre–Wilkie decidability, and proved unconditionally only the model completeness of the analogous theory with the exponential restricted to $(-1,1)$; Chonev–Ouaknine–Worrell (2023) proved unconditionally that the Infinite Zeros Problem for exponential polynomials is decidable, but their decidability of the Zero Problem is Schanuel-conditional and limited to differential order at most 8. Schanuel's Conjecture itself remains open, so the unconditional status of $T_{\exp}$ is unresolved.

The second ingredient is computable structure theory. A copy (computable presentation) of a countable structure is an isomorphic structure with domain the natural numbers, and a countable structure $\mathcal{A}$ is Muchnik reducible to a countable structure $\mathcal{B}$, written $\mathcal{A}\le_w\mathcal{B}$, if from every copy of $\mathcal{B}$ one can compute a copy of $\mathcal{A}$. Knight–Montalbán–Schweber extended this to structures of arbitrary cardinality: $\mathcal{A}\le^*_w\mathcal{B}$ (generic Muchnik reducibility) holds iff in every generic extension $V[G]$ of the set-theoretic universe $V$ in which both structures are countable, $V[G]$ satisfies $\mathcal{A}\le_w\mathcal{B}$. In this ordering, Cantor space $2^{\omega}$ (the set of infinite binary sequences), its representation $\mathcal{W}$, and an $\omega$-saturated (countably saturated) elementary extension $\mathcal{R}^*$ of the ordered field all occupy the generic Muchnik degree strictly below the ordered field $\mathcal{R}$ and Baire space $\mathcal{B}=\omega^{\omega}$ (the set of infinite sequences of natural numbers), which are equivalent to each other. Igusa–Knight–Schweber (2017) asked where expansions of $\mathcal{R}$ land. Their main results: $(\mathbb{R},\exp)\equiv^*_w\mathcal{R}$, and more generally $(\mathbb{R},f)\equiv^*_w\mathcal{R}$ for every analytic $f$; the proof of the former codes the theory $T_{\exp}$ as a real parameter, which is why the intrinsic decidability of that parameter bears directly on the construction. Their General Theorem states that if $\mathcal{M}$ is an o-minimal expansion, in a countable language, of $\mathcal{R}_{\mathbb{Q}}=(\mathbb{R},<,(q)_{q\in\mathbb{Q}})$ — the reals with the ordering and constants naming each rational — and $\mathcal{M}$ has definable Skolem functions (a definable function selecting a witness for every existential formula), then $\mathcal{M}\leq^*_w\mathcal{R}_{\mathbb{Q}}$. In Section 5 they introduced the leaner interval structure $\mathcal{R}_{int}$: the reals with the ordering and a unary predicate for each half-open dyadic interval $[q,q')$ with dyadic rational endpoints $q<q'$. They proved $\mathcal{B}\equiv^*_w\mathcal{R}_{int}$ (via preferred binary expansions) and $\mathcal{R}_{\mathbb{Q}}\equiv^*_w\mathcal{R}_{int}$, and indicated that the General Theorem should hold with $\mathcal{R}_{int}$ in place of $\mathcal{R}_{\mathbb{Q}}$, outlining a modification of the argument with dyadic boxes in place of rational boxes — but they did not supply a complete proof.

Problem Statement

Two independent open questions of different provenance: Part A belongs to the Tarski–Macintyre–Wilkie lineage, and Part B is the $\mathcal{R}_{int}$ analogue of the General Theorem of Igusa–Knight–Schweber (2017), which that paper outlined but did not completely prove. The two parts are logically independent; settling either part fully resolves that part.

Part A (Tarski's question, unconditional form). Is $T_{\exp}=\mathrm{Th}(\mathbb{R};+,\cdot,<,0,1,\exp)$ decidable without unproved hypotheses, that is, without assuming Schanuel's Conjecture or any of its weak forms? By the Macintyre–Wilkie equivalence (see Background), an unconditional decision procedure for $T_{\exp}$ would establish the Weak Schanuel axiom scheme — the first-order weakening of Schanuel's Conjecture under which $T_{\exp}$ is decidable — and a proof that $T_{\exp}$ is undecidable would refute it.

Part B (interval-structure General Theorem). Let $\mathcal{R}_{int}$ be the structure with universe $\mathbb{R}$ whose language contains the ordering $<$ and a unary predicate symbol for each half-open dyadic interval $[q,q')$ with dyadic rational endpoints $q<q'$, interpreted naturally. Here a structure $\mathcal{A}$ is generically Muchnik reducible to a structure $\mathcal{C}$, written $\mathcal{A}\leq^*_w\mathcal{C}$, if in every generic extension of the set-theoretic universe in which both structures are countable, from every copy (isomorphic presentation with domain the natural numbers) of $\mathcal{C}$ one can compute a copy of $\mathcal{A}$; write $\equiv^*_w$ for reducibility in both directions. Prove, or refute, the following statement: every o-minimal expansion $\mathcal{M}$ of $\mathcal{R}_{int}$ in a countable language — o-minimal meaning that every $\mathcal{M}$-definable subset of the real line is a finite union of points and open intervals — such that $\mathcal{M}$ has definable Skolem functions (a definable function selecting a witness for every existential formula), satisfies $\mathcal{M}\leq^*_w\mathcal{R}_{int}$. Igusa–Knight–Schweber proved the corresponding statement with base $\mathcal{R}_{\mathbb{Q}}=(\mathbb{R},<,(q)_{q\in\mathbb{Q}})$, the reals with the ordering and a constant naming each rational, and proved that Baire space $\mathcal{B}=\omega^{\omega}$ satisfies $\mathcal{B}\equiv^*_w\mathcal{R}_{int}\equiv^*_w\mathcal{R}_{\mathbb{Q}}$, but only outlined the dyadic-box modification of their argument for this variant; a complete proof is sought, or a counterexample consisting of an o-minimal expansion of $\mathcal{R}_{int}$, in a countable language with definable Skolem functions, that is not generically Muchnik reducible to $\mathcal{R}_{int}$.

The two parts are the two fronts on which the source paper's computational account of the real exponential field remains conditional or incomplete: Part A asks whether the theory parameter that the paper's construction consumes as a real oracle is intrinsically computable, and Part B asks whether the paper's reduction framework for tame expansions remains valid over the minimal dyadic-interval base that the paper itself isolates.

References

1. Alfred Tarski (1951). A Decision Method for Elementary Algebra and Geometry. University of California Press. DOI 10.2307/jj.8501420 (resolves to the publisher's digital edition, deposited 2023, ISBN 978-0-520-34809-7, of the 1951 monograph). https://doi.org/10.2307/jj.8501420
2. A. J. Wilkie (1996). Model completeness results for expansions of the ordered field of real numbers by restricted Pfaffian functions and the exponential function. Journal of the American Mathematical Society 9(4), 1051–1094. DOI 10.1090/S0894-0347-96-00216-0. https://doi.org/10.1090/S0894-0347-96-00216-0
3. Angus Macintyre and A. J. Wilkie (1996). On the decidability of the real exponential field. In: Piergiorgio Odifreddi (ed.), Kreiseliana: About and Around Georg Kreisel, A K Peters, Wellesley, MA, pp. 441–467. ISBN 1-56881-061-X, Zbl 0896.03012. https://zbmath.org/0896.03012
4. A. J. Wilkie (1997). Schanuel's conjecture and the decidability of the real exponential field. In: B. Hart et al. (eds.), Algebraic Model Theory, NATO ASI Series C, vol. 496, Kluwer Academic Publishers, Dordrecht, pp. 223–230. ISBN 0-7923-4666-1, Zbl 0888.03022. https://zbmath.org/0888.03022
5. Julia Knight, Antonio Montalbán, and Noah Schweber (2016). Computable structures in generic extensions. The Journal of Symbolic Logic 81(3), 814–832. DOI 10.1017/jsl.2015.30. https://doi.org/10.1017/jsl.2015.30
6. G. Igusa and J. F. Knight (2016). Comparing two versions of the reals. The Journal of Symbolic Logic 81(3), 1115–1123. DOI 10.1017/jsl.2015.77. https://doi.org/10.1017/jsl.2015.77
7. Rod Downey, Noam Greenberg, and Joseph S. Miller (2016). Generic Muchnik reducibility and presentations of fields. Israel Journal of Mathematics 216(1), 371–387. DOI 10.1007/s11856-016-1413-7. https://doi.org/10.1007/s11856-016-1413-7
8. Gregory Igusa, Julia F. Knight, and Noah David Schweber (2017). Computing strength of structures related to the field of real numbers. The Journal of Symbolic Logic 82(1), 137–150. DOI 10.1017/jsl.2016.55. https://doi.org/10.1017/jsl.2016.55
9. Matthew Harrison-Trainor (2018). Computable valued fields. Archive for Mathematical Logic 57(5–6), 473–495. DOI 10.1007/s00153-017-0589-9. https://doi.org/10.1007/s00153-017-0589-9
10. Ventsislav Chonev, Joel Ouaknine, and James Worrell (2023). On the zeros of exponential polynomials. Journal of the ACM 70(4), Article 26. DOI 10.1145/3603543. https://doi.org/10.1145/3603543
11. Uri Andrews, Julia F. Knight, Rutger Kuyper, Joseph S. Miller, and Mariya I. Soskova (2023). Expanding the reals by continuous functions adds no computational power. The Journal of Symbolic Logic 88(3), 1083–1102. DOI 10.1017/jsl.2022.66. https://doi.org/10.1017/jsl.2022.66
12. Lothar Sebastian Krapp (2024). Embedding the prime model of real exponentiation into o-minimal exponential fields. Bulletin of the London Mathematical Society 56(3), 907–913. DOI 10.1112/blms.12972. https://doi.org/10.1112/blms.12972
13. Uri Andrews, Joseph S. Miller, Noah Schweber, and Mariya Soskova (2024). Complexity profiles and generic Muchnik reducibility. Advances in Mathematics 436, 109397. DOI 10.1016/j.aim.2023.109397. https://doi.org/10.1016/j.aim.2023.109397
14. Alessandro Berarducci and Francesco Gallinaro (2026). On the elementary theory of the real exponential field. arXiv:2603.08365v2 [math.LO], 23 June 2026. https://arxiv.org/abs/2603.08365