Decidability and invariant classes for degree structures

Abstract:

We present a decision procedure for the $\forall \exists$-theory of $\mathcal {D}[{\mathbf {0}}, {\mathbf {0}}’ ]$, the Turing degrees below ${\mathbf {0}}’$. The two main ingredients are a new extension of embeddings result and a strengthening of the initial segments results below ${\mathbf {0}}’$ of [Le1]. First, given any finite subuppersemilattice $U$ of $\mathcal {D}[{\mathbf {0}}, {\mathbf {0}}’ ]$ with top element ${\mathbf {0}}’$ and an isomorphism type $V$ of a poset extending $U$ consistently with its structure as an usl such that $V$ and $U$ have the same top element and $V$ is an end extension of $U - \{ {\mathbf {0}}’ \}$, we construct an extension of $U$ inside $\mathcal {D}[{\mathbf {0}}, {\mathbf {0}}’ ]$ isomorphic to $V$. Second, we obtain an initial segment $W$ of $\mathcal {D}[{\mathbf {0}}, {\mathbf {0}}’ ]$ which is isomorphic to $U - \{ {\mathbf {0}}’ \}$ such that $W \cup \{ {\mathbf {0}}’ \}$ is a subusl of $\mathcal {D}$. The decision procedure follows easily from these results. As a corollary to the $\forall \exists$-decision procedure for $\mathcal {D}$, we show that no degree ${\mathbf {a}} > {\mathbf {0}}$ is definable by any $\exists \forall$-formula of degree theory. As a start on restricting the formulas which could possibly define the various jump classes we classify the generalized jump classes which are invariant for any $\forall$ or $\exists$-formula. The analysis again uses the decision procedure for the $\forall \exists$-theory of $\mathcal {D}$. A similar analysis is carried out for the high/low hierarchy using the decision procedure for the $\forall \exists$-theory of $\mathcal {D}[{\mathbf {0}}, {\mathbf {0}}’ ]$. (A jump class $\mathcal {C}$ is $\sigma$-invariant if $\sigma ({\mathbf {a}})$ holds for every ${\mathbf {a}}$ in $\mathcal {C}$.)