Cole and Kihara (2010) proved that the ∀∃-theory of the Medvedev degrees of effectively closed (Π10\Pi^0_1) subclasses of Cantor space is decidable in the pure order language with constants 0\mathbf 0 and 1\mathbf 1, and posed two further questions: whether the full first-order theory in that order language is decidable (their Question 1), and whether the ∀∃-theory remains decidable in the richer lattice language L^={≤,∨,∧,0,1}\hat L=\{\le,\vee,\wedge,\mathbf 0,\mathbf 1\} with primitive join and meet (their Question 2). Shafer (2012) resolved Question 1 negatively by coding true arithmetic into this degree structure, and showed undecidability in the lattice language already at the Σ3\Sigma_3 level. The surviving open core, explicitly re-posed as open by Cole in 2025, is whether the ∀∃- (that is, Π2\Pi_2-) theory of (Ps,≤,∨,∧,0,1)(\mathcal{P}_s,\le,\vee,\wedge,\mathbf 0,\mathbf 1) is decidable — equivalently, whether the multi-extension-of-embeddings problem for finite configurations of Π10\Pi^0_1 mass problems admits an effective solution when join and meet are part of the language. This record documents the partial resolutions and states the open problem.

Background

A mass problem is a set of functions, viewed as the collection of all 'solutions' to some mathematical problem — for instance, the set of all complete consistent extensions of a given formal theory. Medvedev reducibility compares two mass problems by uniform computability: P≤sQP\le_s Q if a single Turing functional Φ\Phi (a single algorithm allowed to read any solution of QQ as an oracle) maps every solution of QQ to a solution of PP, written Φ(Q)⊆P\Phi(Q)\subseteq P. The Medvedev degrees are the equivalence classes of mass problems under mutual ≤s\le_s-reducibility. The weak variant, Muchnik reducibility, allows the algorithm to depend on the solution: P≤wQP\le_w Q iff every solution of QQ Turing-computes some solution of PP. This record concerns the degrees of effectively closed problems: a Π10\Pi^0_1 class (also called an effectively closed set) is the set of infinite paths through a computable binary tree, i.e., a closed subset of Cantor space 2ω2^\omega given by a computable enumeration of forbidden finite initial segments. The Medvedev degrees of nonempty Π10\Pi^0_1 subclasses of 2ω2^\omega form a countable distributive lattice Ps\mathcal{P}_s (also written Es\mathcal{E}_s in later literature): the join of two degrees is represented by the problem of pairing a solution of each, {p⊕q:p∈P,q∈Q}\{p\oplus q: p\in P, q\in Q\} where p⊕qp\oplus q interleaves the two functions, and the meet by the tagged union (0)⌢P∪(1)⌢Q(0)^\frown P\cup(1)^\frown Q, whose members solve one of the two problems, tagged by which. The least element 0\mathbf 0 is the degree of the 'solvable' problems, those containing a computable function; the greatest element 1\mathbf 1 is the degree of the Π10\Pi^0_1 class of complete consistent extensions of Peano Arithmetic, since a classical uniform basis theorem says that from any complete extension of PA one can uniformly compute a member of any nonempty Π10\Pi^0_1 class. For such a degree structure one asks which fragments of its first-order theory are decidable. A ∀∃-sentence is a prenex sentence ∀x1⋯∀xm ∃y1⋯∃yn θ\forall x_1\cdots\forall x_m\,\exists y_1\cdots\exists y_n\,\theta with quantifier-free matrix — a Π2\Pi_2 sentence; density statements and extension properties are typical examples. Before Cole and Kihara, the purely existential theory of Ps\mathcal{P}_s in the lattice language was known to be computable (they credit Binns, whose work with Simpson showed every countable distributive lattice embeds into the Muchnik degrees of Π10\Pi^0_1 classes and many into the Medvedev ones), and Cenzer and Hinman had proved that the ordering ≤\le on Ps\mathcal{P}_s is dense. Cole and Kihara then proved that the ∀∃-theory of (Ps,≤,0,1)(\mathcal{P}_s,\le,\mathbf 0,\mathbf 1) in the pure order language L={≤,0,1}L=\{\le,\mathbf 0,\mathbf 1\} is decidable. Their method reduces such a sentence to finitely many instances of the multi-extension-of-embeddings problem: given finite partially ordered sets P⊆Q0,…,Qk−1P\subseteq Q_0,\dots,Q_{k-1}, decide whether every embedding of PP into the degree structure extends to an embedding of some QiQ_i; they gave an effective combinatorial criterion for this inside Ps\mathcal{P}_s. Two limitations remained, and they motivate the open problem. First, although join and meet are first-order definable from ≤\le in any lattice, each definition hides an extra universal quantifier (zz is the join of xx and yy iff x≤zx\le z and y≤zy\le z and every ww with x≤wx\le w and y≤wy\le w satisfies z≤wz\le w), so decidability of the order-language ∀∃-theory does not transfer to the ∀∃-theory in the richer lattice language L^={≤,∨,∧,0,1}\hat L=\{\le,\vee,\wedge,\mathbf 0,\mathbf 1\}. Second, Shafer subsequently coded arithmetic into this same structure: the full first-order theory of Ps\mathcal{P}_s as a partial order is recursively isomorphic to true first-order arithmetic and hence undecidable — settling Cole and Kihara's Question 1 negatively — and even the Σ3\Sigma_3-theory of Ps\mathcal{P}_s in the lattice language is undecidable, one quantifier alternation above ∀∃. The known results thus bracket exactly one gap, the Π2\Pi_2 level in the lattice language, which no later work has closed.

Problem Statement

Let Ps\mathcal{P}_s be the lattice of Medvedev degrees of nonempty Π10\Pi^0_1 subclasses of Cantor space 2ω2^\omega, with least element 0\mathbf 0 and greatest element 1\mathbf 1, and let L^={≤,∨,∧,0,1}\hat L=\{\le,\vee,\wedge,\mathbf 0,\mathbf 1\} be the first-order language obtained from the order language by adding primitive symbols for binary join and meet. Question (Cole and Kihara 2010, Question 2; re-posed as open by Cole 2025, Question 3): is the ∀∃-theory of (Ps,≤,∨,∧,0,1)(\mathcal{P}_s,\le,\vee,\wedge,\mathbf 0,\mathbf 1) decidable? That is, does there exist a single computable procedure which, given any sentence ∀x1⋯∀xm ∃y1⋯∃yn θ\forall x_1\cdots\forall x_m\,\exists y_1\cdots\exists y_n\,\theta with θ\theta quantifier-free in L^\hat L, halts and correctly decides whether the sentence holds in Ps\mathcal{P}_s? A negative answer would prove that the Π2\Pi_2 level of the lattice-language theory of Ps\mathcal{P}_s is already undecidable. Cole (2025) poses the same question for the Medvedev degrees of Π10\Pi^0_1 subclasses of Baire space; those two degree structures are now known not to coincide, so the Cantor-space and Baire-space versions may be settled together or separately.

References

  1. Joshua A. Cole and Takayuki Kihara, 'The ∀∃-theory of the effectively closed Medvedev degrees is decidable', Archive for Mathematical Logic 49(1):1–16 (2010). DOI: 10.1007/s00153-009-0150-6, https://doi.org/10.1007/s00153-009-0150-6
  2. Paul Shafer, 'Coding true arithmetic in the Medvedev and Muchnik degrees', Journal of Symbolic Logic 76(1):267–288 (2011). DOI: 10.2178/jsl/1294171000, https://doi.org/10.2178/jsl/1294171000
  3. Paul Shafer, 'Coding true arithmetic in the Medvedev degrees of Π⁰₁ classes', Annals of Pure and Applied Logic 163(3):321–337 (2012). DOI: 10.1016/j.apal.2011.10.002, https://doi.org/10.1016/j.apal.2011.10.002
  4. Andrew Lewis, André Nies and Andrea Sorbi, 'The First Order Theories of the Medvedev and Muchnik Lattices', in Klaus Ambos-Spies, Benedikt Löwe and Wolfgang Merkle (eds.), Mathematical Theory and Computational Practice: 5th Conference on Computability in Europe, CiE 2009, Heidelberg, Germany, July 19–24, 2009, Proceedings, Lecture Notes in Computer Science 5635, 324–331 (2009). DOI: 10.1007/978-3-642-03073-4_33, https://doi.org/10.1007/978-3-642-03073-4_33
  5. Joshua A. Cole, 'A closed subset of Baire space not Medvedev equivalent to any closed set of Cantor space', Archive for Mathematical Logic 64(7–8):997–1005 (2025). DOI: 10.1007/s00153-025-00973-6, https://doi.org/10.1007/s00153-025-00973-6 (preprint: arXiv:2407.10015, https://arxiv.org/abs/2407.10015)
  6. Kojiro Higuchi and Takayuki Kihara, 'Inside the Muchnik degrees I: Discontinuity, learnability and constructivism', Annals of Pure and Applied Logic 165(5):1058–1114 (2014). DOI: 10.1016/j.apal.2014.01.003, https://doi.org/10.1016/j.apal.2014.01.003 (preprint: arXiv:1210.0697, https://arxiv.org/abs/1210.0697)
  7. Kojiro Higuchi and Takayuki Kihara, 'Inside the Muchnik degrees II: The degree structures induced by the arithmetical hierarchy of countably continuous functions', Annals of Pure and Applied Logic 165(6):1201–1241 (2014). DOI: 10.1016/j.apal.2014.03.001, https://doi.org/10.1016/j.apal.2014.03.001 (preprint: arXiv:1309.1937, https://arxiv.org/abs/1309.1937)
  8. Peter G. Hinman, 'A Survey of Mučnik and Medvedev Degrees', Bulletin of Symbolic Logic 18(2):161–229 (2012). DOI: 10.2178/bsl/1333560805, https://doi.org/10.2178/bsl/1333560805 (preprint: arXiv:1007.2376, https://arxiv.org/abs/1007.2376, titled 'A Survey of Muchnik and Medvedev degrees')
  9. Douglas Cenzer and Peter G. Hinman, 'Density of the Medvedev lattice of Π⁰₁ classes', Archive for Mathematical Logic 42(6):583–600 (2003). DOI: 10.1007/s00153-002-0166-7, https://doi.org/10.1007/s00153-002-0166-7
  10. Stephen Binns and Stephen G. Simpson, 'Embeddings into the Medvedev and Muchnik lattices of Π⁰₁ classes', Archive for Mathematical Logic 43(3):399–414 (2004). DOI: 10.1007/s00153-003-0195-x, https://doi.org/10.1007/s00153-003-0195-x
  11. Stephen Binns, Richard A. Shore and Stephen G. Simpson, 'Mass problems and density', Journal of Mathematical Logic 16(2), article 1650006 (2016). DOI: 10.1142/S0219061316500069, https://doi.org/10.1142/S0219061316500069
  12. Paul Shafer, 'On the Complexity of Mathematical Problems: Medvedev Degrees and Reverse Mathematics', PhD thesis, Cornell University (2011). https://www.semanticscholar.org/paper/b46f99bfd756bc4b738b4d41437cbfc10bfa1070