Decidability and invariant classes for degree structures

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}$.)