The decidability of the existential theory of the poset of recursively enumerable degrees with jump relations (Q1921269): Difference between revisions

There is a long history of analysis of the structure of the poset of enumerable degrees in the language with predicate \(\leq\). Harrington and Shelah proved that the full theory is undecidable. Harrington and Slaman, and later Slaman and Woodin demonstrated that the theory is as bad as possible by calculating the degree of the theory. On the other hand, early work of Sacks proved that the one quantifier theory is decidable: any partial ordering can be realized densely. The situation with the two quantifier theory is far less clear and even the special case of deciding which lattices are embeddable into the enumerable degrees as lattices remains open. Another central concept in the theory of degrees is the jump operator. The paper at hand considers the structure of the enumerable degrees with, for each \(n\in \mathbb{N}\), additional predicates of the form \(\leq_n\) which has the interpretation \({\mathbf a}\leq_n {\mathbf b}\) means \({\mathbf a}^{(n)}\leq {\mathbf b}^{(n)}\). Note that \({\mathbf a}\leq {\mathbf b}\) implies \({\mathbf a}^{(n)}\leq {\mathbf b}^{(n)}\) for all \(n\), but it is possible for \({\mathbf a}\not\leq {\mathbf b}\) yet \({\mathbf a}^{(n)}\leq {\mathbf b}^{(n)}\). The authors provide a decision procedure for the theory of the enumerable degrees with the predicates \(\leq_n\). The proof demonstrates that any consistent configuration can be realized. One very significant part of the paper is the proof itself. The proof uses iterated trees of strategies, formalizing earlier ideas of Harrington, Slaman, and Ash. The basic idea is that one decomposes a level \(n\) requirement into a strategy tree where each node codes a tree of the previous level. For the reader who is aware of previous ``worker'' or ``\(\alpha\)-system'' arguments, it is notable that the argument is not an ``iterated three worker argument'', but \(\leq_n\) needs a genuine level \(n\) argument presented formally, perhaps for the first time. The details are immensely complex and use some general machinery developed for the task. In this reviewer's opinion it is not altogether clear if the methodology will find wide application because each application would seem to need modifications to the Lempp-Lerman machinery. However, the authors should be congratulated for such an impressive intellectual achievement. The paper will reward the determined reader with a wealth of deep ideas about higher level priority arguments.