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

From MaRDI portal
RedirectionBot (talk | contribs)
Changed an Item
Set OpenAlex properties.
(One intermediate revision by one other user not shown)
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / full work available at URL
 
Property / full work available at URL: https://doi.org/10.1006/aima.1996.0033 / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W2019646940 / rank
 
Normal rank

Revision as of 01:29, 20 March 2024

scientific article
Language Label Description Also known as
English
The decidability of the existential theory of the poset of recursively enumerable degrees with jump relations
scientific article

    Statements

    The decidability of the existential theory of the poset of recursively enumerable degrees with jump relations (English)
    0 references
    0 references
    0 references
    24 February 1997
    0 references
    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.
    0 references
    existential theory
    0 references
    poset of recursively enumerable degrees
    0 references
    jump relations
    0 references
    coding
    0 references
    decision procedure
    0 references
    iterated trees of strategies
    0 references
    higher level priority arguments
    0 references

    Identifiers