Decidability of the two-quantifier ($\Pi_2$) theory of the $\Sigma^0_2$-enumeration degrees

The enumeration degrees order sets of natural numbers by enumeration reducibility, the positive-information analogue of Turing reducibility, and the degrees of the $\Sigma^0_2$ sets form the local structure $\mathcal{D}_e(\le\mathbf{0}'_e)$, the enumeration-degree counterpart of the Turing degrees below $\mathbf{0}'$. Its first-order theory in the language $\{\le\}$ breaks sharply by quantifier complexity: the existential theory is decidable, the three-quantifier theory is undecidable (Kent, 2006), and the full theory is computably isomorphic to true arithmetic. Exactly one level is unaccounted for. This problem asks whether the two-quantifier ($\forall\exists$, i.e. $\Pi_2$) theory of $\mathcal{D}_e(\le\mathbf{0}'_e)$ is decidable. Equivalently: given finite partial orders $P \subseteq Q_0,\dots,Q_n$ for arbitrary $n \ge 0$, is there an algorithm deciding whether every embedding of $P$ into the $\Sigma^0_2$-enumeration degrees extends to an embedding of at least one $Q_i$, where the choice of $i$ may depend on the embedding of $P$? The case $n=0$, the extension-of-embeddings problem, was decided affirmatively by Lempp-Slaman-Sorbi (2005); the cases $n \ge 1$ remain open, with current research concentrated on Ahmad pairs, the basic configurations that block extensions. As of August 2026 the question is open, with active work underway (Ravishankar, 2025; Goh-Lempp-Ng-Soskova, in preparation).

Background

Degrees of unsolvability measure how much computational information one set of natural numbers shares with another. The classical Turing degrees compare sets using total algorithms; enumeration reducibility, introduced by Friedberg and Rogers (1959), is the positive-information counterpart: $A \le_e B$ holds when there is a computably enumerable set of requirements, each pairing a number $n$ with a finite set $D$, such that $A$ consists exactly of those $n$ for which some requirement $\langle n,D\rangle$ has $D \subseteq B$. Informally, any enumeration of $B$ can be uniformly converted into an enumeration of $A$, without ever asking whether an element is absent from $B$. The resulting equivalence classes, ordered by the induced relation, form the structure $\mathcal{D}_e$ of enumeration degrees. It contains the Turing degrees as a proper substructure (a set $A$ is mapped to the degree of $A \oplus \overline{A}$, where $\overline{A}$ is the complement of $A$ and $\oplus$ is disjoint union), so it is a strictly finer measure of information content. The enumeration jump of the least degree $\mathbf{0}_e$ (the analogue of the Turing jump for enumeration reducibility) plays the role of the halting problem, and the degrees below it are exactly the enumeration degrees of the $\Sigma^0_2$ sets, that is, the sets definable by a formula of the form $n \in A \Leftrightarrow \exists u\,\forall v\,R(n,u,v)$ with $R$ a computable predicate, equivalently the sets enumerable relative to the halting problem. This interval, denoted $\mathcal{D}_e(\le\mathbf{0}'_e)$ and called the local structure, is the enumeration-degree analogue of the Turing degrees below $\mathbf{0}'$. Unlike that structure it is dense: Cooper (1984) proved that between any two comparable $\Sigma^0_2$-enumeration degrees there is a third, and Bianchini's extension of Cooper's theorem shows that every countable partial order embeds into $\mathcal{D}_e(\le\mathbf{0}'_e)$ (see Soskova, 2020), so in particular every finite partial order embeds. The first-order theory of a degree structure is studied fragment by fragment, in a language whose only non-logical symbol is the order $\le$. A fragment is decidable if an algorithm determines, for each sentence of the prescribed quantifier shape, whether the structure satisfies it. The $\exists$-fragment asks which finite partial-order diagrams are realized; the two-quantifier or $\Pi_2$ fragment consists of the $\forall\exists$-sentences (by closure under negation, deciding these is the same as deciding all sentences with at most two blocks of quantifiers); the three-quantifier fragment is the next level. For $\mathcal{D}_e(\le\mathbf{0}'_e)$ the boundary is pinned to a single level. The $\exists$-theory is decidable, since an $\exists$-sentence describes a finite partial order and all of these embed. The three-quantifier ($\Pi_3$) theory is undecidable (Kent, 2006), sharpening the five-quantifier-level undecidability that follows from Slaman-Woodin's (1997) uniform embedding of all finite graphs; the full theory is computably isomorphic to first-order true arithmetic, meaning the true sentences of the two structures are intertranslatable by computable maps (Kent, 2010; Ganchev-Soskova, 2012); and for the global structure $\mathcal{D}_e$ the full theory is computably isomorphic to the theory of second-order arithmetic and the three-quantifier theory is hereditarily undecidable, that is, no subtheory of it containing its validities is decidable (Slaman-Woodin, 1997; Lempp-Slaman-Soskova, 2021). The two-quantifier level is the one remaining gap. The two-quantifier question has a standard algebraic reformulation. A quantifier-free description of a tuple of degrees is a finite partial order $P$, and a $\forall\exists$-sentence asserts: whenever a copy of $P$ is embedded in the degree structure, the embedding extends to realize one of finitely many finite extensions $Q_0,\dots,Q_n$ of $P$, where the choice may depend on the embedding. Deciding all $\forall\exists$-sentences is therefore equivalent to deciding, for all $n \ge 0$ and all finite partial orders $P \subseteq Q_0,\dots,Q_n$, whether every embedding of $P$ into $\mathcal{D}_e(\le\mathbf{0}'_e)$ extends to an embedding of some $Q_i$. The case $n=0$, the extension-of-embeddings problem, was answered affirmatively by Lempp-Slaman-Sorbi (2005), the enumeration-degree analogue of Slaman-Soare's (2001) theorem for the computably enumerable Turing degrees. Their analysis reduced non-extendability to finitely many obstruction types, the leading one being Ahmad pairs: incomparable degrees $a,b$ such that every degree strictly below $a$ lies below $b$. Ahmad pairs exist and no symmetric Ahmad pair exists (Ahmad's thesis, published account in Ahmad-Lachlan, 1998, doi:10.1002/malq.19980440402); if a two-element antichain is embedded as an Ahmad pair, no extension placing an element below the left half but not below the right half is possible. The same two-versus-three-quantifier boundary is the standard testing ground across degree structures: for the Turing degrees and the many-one degrees the $\forall\exists$-theory is decidable and the $\exists\forall\exists$-theory undecidable, while for the computably enumerable Turing degrees, as for both the global and the local enumeration degrees, the $\forall\exists$-theory is open (see Lempp-Slaman-Soskova, 2021, for a unified discussion). Density blocks the initial-segment embedding method that settled the Turing-degree case, in which the finite poset is realized as an initial segment (a downward-closed substructure) of the degrees so that the obstacles to extension can be read off combinatorially (Soskova, 2020), so genuinely new methods are needed.

Problem Statement

Determine whether the two-quantifier ($\Pi_2$, i.e. $\forall\exists$) theory of the partial order $\mathcal{D}_e(\le\mathbf{0}'_e)$ of $\Sigma^0_2$-enumeration degrees, in the language whose only relation symbol is $\le$, is decidable. Concretely, establish exactly one of the following. (1) Positive answer: exhibit an algorithm which, on input finite partial orders $P \subseteq Q_0,\dots,Q_n$ for arbitrary $n \ge 0$, halts and outputs yes or no, and prove that the output is yes exactly when every embedding of $P$ into $\mathcal{D}_e(\le\mathbf{0}'_e)$ can be extended to an embedding of $Q_i$ for at least one $i \le n$, where the choice of $i$ may depend on the embedding of $P$; such an algorithm decides every $\forall\exists$-sentence of the structure. (2) Negative answer: prove that no such algorithm exists, i.e. that the $\forall\exists$-theory of $\mathcal{D}_e(\le\mathbf{0}'_e)$ is undecidable. The case $n=0$ of the extension problem is already settled affirmatively (Lempp-Slaman-Sorbi, 2005), so the open content is the cases $n \ge 1$; by closure of the theory under negation, deciding all $\forall\exists$-sentences is equivalent to deciding all two-quantifier sentences. This formulation is faithful to Question 1.4.1 of Kent's thesis and the open problem left in Kent (2006), to Open Question 1.7 of Lempp-Slaman-Sorbi (2005), and to Question 4.6 of Soskova's survey (2020).

References

1. Friedberg, R.; Rogers, H. (1959). Reducibility and completeness for sets of integers. Zeitschrift fuer Mathematische Logik und Grundlagen der Mathematik 5, 117-125. doi:10.1002/malq.19590050703
2. Cooper, S. B. (1984). Partial degrees and the density problem. Part 2: The enumeration degrees of the $\Sigma_2$ sets are dense. Journal of Symbolic Logic 49(2), 503-513. doi:10.2307/2274181
3. Ahmad, S.; Lachlan, A. H. (1998). Some special pairs of $\Sigma_2$ e-degrees. Mathematical Logic Quarterly 44(4), 431-449. doi:10.1002/malq.19980440402
4. Slaman, T. A.; Woodin, W. H. (1997). Definability in the enumeration degrees. Archive for Mathematical Logic 36(6), 255-267. doi:10.1007/s001530050064
5. Slaman, T. A.; Soare, R. I. (2001). Extension of embeddings in the computably enumerable degrees. Annals of Mathematics (2) 154(1), 1-43. doi:10.2307/3062109
6. Lempp, S.; Slaman, T. A.; Sorbi, A. (2005). On extensions of embeddings into the enumeration degrees of the $\Sigma^0_2$-sets. Journal of Mathematical Logic 5(2), 247-298. doi:10.1142/S0219061305000432
7. Kent, T. F. (2005). Decidability and definability in the $\Sigma^0_2$-enumeration degrees. Ph.D. thesis, University of Wisconsin-Madison. https://web.math.wisc.edu/logic/theses/kent.pdf
8. Kent, T. F. (2006). The $\Pi_3$-theory of the $\Sigma^0_2$-enumeration degrees is undecidable. Journal of Symbolic Logic 71(4), 1284-1302. doi:10.2178/jsl/1164060455
9. Kent, T. F.; Sorbi, A. (2007). Bounding nonsplitting enumeration degrees. Journal of Symbolic Logic 72(4), 1405-1417. doi:10.2178/jsl/1203350795
10. Kent, T. F. (2010). Interpreting true arithmetic in the $\Sigma^0_2$-enumeration degrees. Journal of Symbolic Logic 75(2), 522-550. doi:10.2178/jsl/1268917493
11. Ganchev, H.; Soskova, M. I. (2012). Interpreting true arithmetic in the local structure of the enumeration degrees. Journal of Symbolic Logic 77(4), 1184-1194. doi:10.2178/jsl.7704070
12. Soskova, M. I. (2020). The theory of the enumeration degrees, definability, and automorphisms. In: A. Rezus (ed.), Contemporary Logic and Computing (Landscapes in Logic 1), College Publications, London, 706-730. ISBN 978-1-84890-340-1. https://zbmath.org/1505.03087
13. Lempp, S.; Slaman, T. A.; Soskova, M. I. (2021). Fragments of the theory of the enumeration degrees. Advances in Mathematics 383, 107686. doi:10.1016/j.aim.2021.107686
14. Goh, J. L.; Lempp, S.; Ng, K. M.; Soskova, M. I. (2022). Extensions of two constructions of Ahmad. Computability 11(3-4), 269-297. doi:10.3233/COM-210380
15. Kalimullin, I. Sh.; Lempp, S.; Ng, K. M.; Yamaleev, M. M. (2024). On cupping and Ahmad pairs. Journal of Symbolic Logic 89(3), 1358-1369. doi:10.1017/jsl.2022.84
16. Ravishankar, K. (2025). Contrasting the halves of an Ahmad pair. arXiv:2511.22901. https://arxiv.org/abs/2511.22901