Decidability of the two-quantifier theory of the enumeration degrees

The structure $\mathcal{D}_e$ of enumeration degrees — degrees of the positive-information reducibility introduced by Friedberg and Rogers — strictly generalizes the Turing degrees, and its full first-order theory is as complicated as second-order arithmetic. Its one-quantifier theory is decidable; Lempp, Slaman and Soskova (2021) proved its three-quantifier ($\exists\forall\exists$) theory hereditarily undecidable via strong interval embeddings of finite distributive lattices, and decided the extension-of-embeddings problem, the $k=1$ subproblem of the two-quantifier theory. The central problem, stated in Section 6 of that paper and still open, is whether the full two-quantifier ($\exists\forall$, equivalently $\forall\exists$) theory of $\mathcal{D}_e$ is decidable — equivalently, whether the generalized extension-of-embeddings problem for $\mathcal{D}_e$ admits an algorithm. The source's Section 6 also states two further open problems: Conjecture 6.1, that every finite lattice (not only every finite distributive lattice) has a strong interval embedding into $\mathcal{D}_e$, and Question 6.3, a model-theoretic characterization of the $\exists\forall$-theory via a natural class of upper semilattices. The naive candidate characterization is refuted within the source itself (an incompatibility theorem of Jacobsen-Grocott and Soskova: strong-interval behavior cannot coexist with minimal pairs), and follow-up work through 2025 closed the algorithm route that the source's authors had suggested (strong minimal pairs exist, but the strong super minimal pairs that route required do not) while advancing the surrounding minimal-pair and Ahmad-pair phenomena — yet all three questions remain open; no resolution appears in the literature through August 2026.

Background

Enumeration reducibility, introduced by Friedberg and Rogers in 1959, is the positive-information counterpart of Turing reducibility: $A\leq_e B$ holds when there is a computably enumerable set of axioms $W$ with $A=\{n:\exists e\,(\langle n,e\rangle\in W \wedge D_e\subseteq B)\}$, where $D_e$ is the $e$-th finite set in a canonical listing — informally, from any enumeration of $B$ one can effectively produce an enumeration of $A$. The equivalence classes under $\equiv_e$ form the enumeration degrees $\mathcal{D}_e$, an upper semilattice (a partial order in which any two elements have a least upper bound $\vee$) with least element $\mathbf{0}_e$, the degree of the computably enumerable sets. The map $A\mapsto A\oplus\bar{A}$, where $C\oplus D=\{2x:x\in C\}\cup\{2x+1:x\in D\}$ is the tagged disjoint union, embeds the Turing degrees into $\mathcal{D}_e$, so $\mathcal{D}_e$ is a strict generalization of the Turing-degree structure and the natural ambient setting for relative computation of partial functions.

A standard program for a degree structure asks how complicated its first-order theory is and at what quantifier complexity decidability breaks down. For the Turing degrees, the many-one degrees, and the local degree structures below the jump (the Turing jump, which maps a set to its relativized halting problem), the answer has a uniform shape: the full theory is as complicated as second-order (respectively first-order) arithmetic, the $\forall\exists$-theory — sentences consisting of one universal quantifier block followed by one existential block — is decidable, and the $\exists\forall\exists$-theory is undecidable. For $\mathcal{D}_e$, Slaman and Woodin proved that the full theory is computably isomorphic to second-order arithmetic; every countable partial order embeds into $\mathcal{D}_e$, so the $\exists$-theory is decidable; and Lempp, Slaman and Soskova located the boundary one level higher: the $\exists\forall\exists$-theory of $\mathcal{D}_e$ is hereditarily undecidable (no subset of it containing all its validities is decidable), while the extension-of-embeddings problem is decidable. The status of the middle, two-quantifier level is the open gap. Since a sentence and its negation have dual quantifier prefixes, decidability of the $\exists\forall$-theory is equivalent to decidability of the $\forall\exists$-theory, and for an upper semilattice the latter is equivalent to a purely algebraic question (Problem 2.1 of the source): given finite partial orders $P\subseteq Q_0,\ldots,Q_{k-1}$, must every embedding of $P$ into $\mathcal{D}_e$ extend to an embedding of $Q_i$ for at least one $i<k$? The case $k=1$ is the extension-of-embeddings problem, which the source decides; the general problem for arbitrary $k$ is open.

The source's undecidability proof runs through a new embedding notion. A strong interval embedding of a finite lattice $L$ into $\mathcal{D}_e$ is an isomorphism of $L$ onto an interval $[\mathbf a,\mathbf b]$ such that every degree $\mathbf x\leq\mathbf b$ outside the image satisfies $\mathbf x\leq\mathbf a$; for the two-element lattice this is exactly a strong minimal cover ($\mathbf a<\mathbf b$ with every $\mathbf x<\mathbf b$ below $\mathbf a$), instances of which exist by work of Kent, Lewis-Pye and Sorbi. Lempp, Slaman and Soskova proved that every finite distributive lattice (a lattice in which meet distributes over join) admits such an embedding. This makes the class of finite distributive lattices elementarily definable with two parameters in $\mathcal{D}_e$, and the Nies transfer lemma — a general recipe for transferring hereditary undecidability from a class of structures definable in a degree structure — then yields the $\exists\forall\exists$ undecidability. On the algebraic side, $\mathcal{D}_e$ is downward dense (there is a degree strictly between $\mathbf{0}_e$ and any nonzero degree), so finite lattices can never embed as initial segments, and the classical decision procedure for the Turing degrees, which rests on initial-segment embeddings, cannot be imitated. A proposed substitute — combining the strong downward density of Slaman and Sorbi (every countable partial order embeds below any nonzero enumeration degree) with minimal-pair behavior (a minimal pair is a pair of nonzero degrees whose greatest common lower bound is $\mathbf{0}_e$) — fails: Jacobsen-Grocott and Soskova proved that if every degree strictly below $\mathbf a\vee\mathbf b$ is bounded by $\mathbf a$ or by $\mathbf b$, then $\{\mathbf a,\mathbf b\}$ is not a minimal pair, so strong-interval behavior and minimal-pair behavior cannot coexist. For the local structure of the $\Sigma^0_2$ enumeration degrees ($\Sigma^0_2$, the second level of the arithmetical hierarchy of sets of integers; equivalently, the degrees below $\mathbf{0}'_e$), the analogous two-quantifier question is also open; there, Kent proved $\exists\forall\exists$ undecidability, and the principal known obstructions are Ahmad pairs — incomparable degrees $\mathbf a,\mathbf b$ with every $\mathbf x<\mathbf a$ below $\mathbf b$ — which Goh, Lempp, Ng and Soskova showed cannot be chained into triples; a degree is join-irreducible if it is not the least upper bound of two strictly smaller degrees, and the left halves of Ahmad pairs are join-irreducible.

The source's Section 6 also states two further open problems. Conjecture 6.1: every finite lattice — not only every finite distributive lattice — admits a strong interval embedding into $\mathcal{D}_e$. Question 6.3: does there exist a natural class $\mathcal{U}$ of upper semilattices with least element such that an $\exists\forall$-sentence $\varphi$ is true in $\mathcal{D}_e$ if and only if $\varphi$ is true in some $U\in\mathcal{U}$? The naive candidate class, combining strong downward density with minimal-pair behavior, is refuted by the Jacobsen-Grocott-Soskova incompatibility theorem (Theorem 6.2 of the source), and the source observes that confirming Conjecture 6.1 would not in itself lead to an algorithm deciding the $\exists\forall$-theory of $\mathcal{D}_e$.

Problem Statement

Let $\mathcal{D}_e$ be the upper semilattice of enumeration degrees in the language of partial orders, with join $\vee$ and least element $\mathbf{0}_e$.

Central question (stated as 'the most glaring open problem' in Section 6 of Lempp, Slaman and Soskova, 2021): is the $\exists\forall$-theory of $\mathcal{D}_e$ decidable? Equivalently (by negating sentences), is the $\forall\exists$-theory decidable — that is, is there an algorithm which, given finite partial orders $P\subseteq Q_0,\ldots,Q_{k-1}$ (for arbitrary $k$), decides whether every embedding of $P$ into $\mathcal{D}_e$ extends to an embedding of $Q_i$ for at least one $i<k$ (the generalized extension-of-embeddings problem, Problem 2.1 of the source)?

Decidability of the $\exists\forall$-theory of $\mathcal{D}_e$ is witnessed by a uniform decision procedure for all $\exists\forall$-sentences about $\mathcal{D}_e$ — equivalently, for the generalized extension-of-embeddings problem for all finite $P$ and $Q_0,\ldots,Q_{k-1}$, with no restriction on $k$, on the shape of the partial orders, or on the class of embeddings — together with a proof of its correctness; undecidability is witnessed by a proof that the $\exists\forall$-theory of $\mathcal{D}_e$ is undecidable.

References

1. Steffen Lempp, Theodore A. Slaman, and Mariya I. Soskova. Fragments of the theory of the enumeration degrees. Advances in Mathematics 383:107686, 2021. DOI 10.1016/j.aim.2021.107686. https://doi.org/10.1016/j.aim.2021.107686 (author PDF: https://people.math.wisc.edu/~slempp/papers/fragments.pdf)
2. Josiah Jacobsen-Grocott. Strong minimal pairs in the enumeration degrees. Annals of Pure and Applied Logic 175(10):103464, 2024. DOI 10.1016/j.apal.2024.103464. https://doi.org/10.1016/j.apal.2024.103464
3. Jun Le Goh, Steffen Lempp, Keng Meng Ng, and Mariya I. Soskova. Extensions of two constructions of Ahmad. Computability 11(3-4):269-297, 2022. DOI 10.3233/COM-210380. https://doi.org/10.3233/COM-210380
4. Karthik Ravishankar. Contrasting the Halves of an Ahmad Pair. arXiv:2511.22901, 2025. https://arxiv.org/abs/2511.22901
5. Josiah Jacobsen-Grocott, Steffen Lempp, and Isabella Scott. On the structure of the Ziegler degrees. Preprint (submitted); PDF at https://josiahjg.github.io/papers/Ziegler.pdf
6. Rodney G. Downey, Steffen Lempp, and Isabella Scott. The theory of the Ziegler degrees. arXiv:2607.02870, 2026. https://arxiv.org/abs/2607.02870
7. Theodore A. Slaman and W. Hugh Woodin. Definability in the enumeration degrees. Archive for Mathematical Logic 36(4-5):255-267, 1997. DOI 10.1007/s001530050064. https://doi.org/10.1007/s001530050064
8. Thomas F. Kent. The $\Pi_3$-theory of the $\Sigma^0_2$-enumeration degrees is undecidable. Journal of Symbolic Logic 71(4):1284-1302, 2006. DOI 10.2178/jsl/1164060455. https://doi.org/10.2178/jsl/1164060455
9. Thomas F. Kent, Andrew E. M. Lewis-Pye, and Andrea Sorbi. Empty intervals in the enumeration degrees. Annals of Pure and Applied Logic 163(5):567-574, 2012. DOI 10.1016/j.apal.2011.06.012. https://doi.org/10.1016/j.apal.2011.06.012
10. Theodore A. Slaman and Andrea Sorbi. A note on initial segments of the enumeration degrees. Journal of Symbolic Logic 79(2):633-643, 2014. DOI 10.1017/jsl.2013.1. https://doi.org/10.1017/jsl.2013.1
11. Iskander Sh. Kalimullin, Steffen Lempp, Keng Meng Ng, and Mars M. Yamaleev. On cupping and Ahmad pairs. Journal of Symbolic Logic 89(3):1358-1369, 2024 (online 2022). DOI 10.1017/jsl.2022.84. https://doi.org/10.1017/jsl.2022.84
12. Richard M. Friedberg and Hartley Rogers, Jr. Reducibility and completeness for sets of integers. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 5:117-125, 1959 (the journal is now Mathematical Logic Quarterly). DOI 10.1002/malq.19590050703. https://doi.org/10.1002/malq.19590050703
13. André O. Nies. Undecidable fragments of elementary theories. Algebra Universalis 35(1):8-33, 1996. DOI 10.1007/bf01190967. https://doi.org/10.1007/bf01190967