LOW LEVEL NONDEFINABILITY RESULTS: DOMINATION AND RECURSIVE ENUMERATION

MINGZHONG CAI AND RICHARD A. SHORE

Abstract. We study low level nondefinability in the Turing degrees. We prove a variety of results, including for example, that being array nonrecursive is not definable by a Σ_{1} or Π_{1} formula in the language (≤, REA) where REA stands for the “r.e. in and above” predicate. In contrast, this property is definable by a Π_{2} formula in this language. We also show that the Σ_{1}-theory of (D, ≤, REA) is decidable.

1. Introduction

A major focus of recent research on the Turing degrees, D, has been definability, which is also a major focus of mathematical logic in general. We discuss a topic that has received almost no attention but certainly deserves some: nondefinability in the Turing degrees.

This work was motivated by the suggestion of Miller and Martin [MM] that one could prove that the classes HI and HIF of hyperimmune and hyperimmune-free degrees, respectively, are not simply definable. (A degree x ∈ HIF if and only if every f ≤_{T} X is dominated by a recursive function. The class HI consists of the degrees not in HIF.) In addition to the basic language (≤), they suggest two extensions augmenting it by either the jump operator ′ or the relation RE for “recursively enumerable in.” They also allow parameters c̄ for any specific degrees in all their languages. They prove that HI is not definable by a quantifier free formula in the language (≤, c̄) (for any degrees c̄) and conjecture that this is also true for the language with jump, (≤,′ , c̄). We affirm their conjecture and prove other similar theorems about these and other sets of, and relations on, degrees.

In particular, we are interested in another complementary pair of sets of degrees related to domination properties: the array nonrecursive degrees, ANR, that compute a function not dominated by the modulus function for 0′, and the complementary class AR of array recursive degrees. In place of the relation RE, we instead study the relation REA, “recursively enumerable in and above”. Note that while REA is clearly definable from RE by a quantifier free formula, we show in §6 that the reverse is not true even by a one quantifier formula (without parameters). In addition, our intuitions about relativizing the relation RE really apply to REA and all the examples we know using RE actually only use REA. Most striking among these is the two quantifier definition in this language (without parameters) of ANR as {x|(∀y ≥ x)(∃z < y)(y REA z)} ([CS]; [C2]).

Date: January 25, 2013.

1991 Mathematics Subject Classification. 03D28.

The first author was partially supported by NSF Grant DMS-0852811.

The second author was partially supported by NSF Grants DMS-0852811 and DMS-1161175.

In studying these low level nondefinability results, we can also push the quantifier bound up in searching for possible definitions of these degree classes. For example, we still do not know whether HI is definable in D (even augmented with the REA predicate and parameters), and our results show that to define HI we need at least a twoquantifier formula with parameters or a three-quantifier formula without parameters. One might hope then that the obstacles we meet in proving that HI is not definable by formulae of a certain complexity can help suggest possible definitions of HI.

The definability of the predicates RE and REA is also a major open question in the field. In particular, we want to see how these two predicates are related to the partial order (Turing reducibility). Our work on the REA relation (Lemma 3.3 and Theorem 4.2) suggests that the characterization of this relation as given by the modulus lemma (recalled in the proof of Lemma 3.3 below) is an important technique in studying it.

While some of our results allow parameters, most do not. Including parameters makes many more classes of degrees easily definable. Classic examples include the degrees of the productive sets: {x|x ≥ 0′}; the immune sets: {x|x ≥ 0}; the functions dominating every recursive function: {x|x′≥ 0′′} and the degrees of arithmetic sets (by the Exact Pair Theorem [Sp]). However, unbridled use of parameters makes everything possible definable as by Slaman and Woodin [SW, Corollary 5.6], the biinterpretability conjecture holds for D with parameters and so every relation on D definable in second order arithmetic is definable from parameters (although their proof does not produce any simple definitions). In fact, they show that there is a single degree c such that every relation definable in second order arithmetic is definable from c.

The table below summarizes our current results listing classes and relations not definable by formulas in specific classes in one of the three languages indicated with or without parameters (c̄).

Class/Relation Not defined by formula in Language see Section(s)
HI  Σ_{0}  (≤,′ , c̄)  7
HI  Σ_{1}  (≤, c̄)  8
HI  Σ_{2}, Π_{2}  (≤)  9
ANR  Σ_{0}  (≤,′ , c̄)  7
ANR  Σ_{1}  (≤, c̄)  8
ANR  Σ_{1}, Π_{1}  (≤, REA)  5, 3
ANR  Σ_{2}  (≤)  9
HIF  Σ_{1}  (≤, REA, c̄)  3
AR  Σ_{1}  (≤, REA, c̄)  3
Jump  Σ_{1}  (≤, REA)  5
RE  Σ_{1}, Π_{1}  (≤, REA)  6
Arith  Σ_{1}, Π_{1}  (≤, REA)  5
Arith  Σ_{1}, Π_{1}  (≤,′)  9
Arith  Σ_{2}, Π_{2}  (≤)  9

An anonymous referee has pointed out that our construction in Section 3 actually leads to a stronger result that the classes AR and HIF are not Σ_{1} definable in the language (≤,′ , REA, c̄), and so results in Section 7 follows as corollaries. See details in the end of Section 3.

We note the particularly tight instances from this table. ANR is definable (as noted above) by a two quantifier formula in (≤, REA) but not by any one quantifier one. It is also not definable by a Σ_{2} formula in just (≤). The relation y = x′ is definable in (≤, REA) by a Π_{1} formula (y REA x ∧ ∀z(z REA x → z ≤ y)) but not by a Σ_{1} formula in this language. Arith, the class of degrees of arithmetic sets, is definable by a Σ_{3} formula in the language with just ≤. Rewrite [JS, Theorem 3.3] to eliminate the join:

Arith = {x|(∃y ≥ x)(∀z|y ∀w(w ≥ z, y → ∃u(w > u > z))}.

On the other hand, it does not have a Σ_{2} or Π_{2} definition in this language. With REA added to the language, Arith is Π_{2} definable as

{x|[∀a, b(∀c, d((c < a, b) ∧ (d REA c) → (d < a, b)) → x < a, b)]}.

However, it is not 1-quantifier definable even with REA in the language. In (≤,′), a similar formula saying that Arith is the least ideal closed under jump shows that it is Π_{2} definable but again it is not 1-quantifier definable.

All the analyses proceed by first finding an appropriate syntactic normal form for formulas of the class being analyzed. Typically a second step is to simplify the form by finding degrees in the class of degrees being considered with special properties such as avoiding cones determined by the parameters, being minimal or perhaps also r.e. in some other degree (or not). Then one needs to do a construction to show that whatever diagram provided by the witnesses that the special degrees are in the class can be duplicated with corresponding degrees outside it. This then shows that the formula cannot define the class being considered. The techniques for the two quantifier results with just ≤ depend on standard initial segment and extension of embedding results and follow similar ones for other classes in Lerman and Shore [LS] and Shore [S]. The constructions not involving REA are at the moment mostly ad hoc exploiting various forcing constructions and special facts. Most of our results involving REA depend on variations on a basic theorem providing a decision procedure for one quantifier formulas in the language (≤, REA) (see Section 4 and Theorem 4.2).

The first half of this paper focuses on the nondefinability results related to languages with the REA predicate, and the second half consists of miscellaneous results on languages without it. We finish with some remarks and open questions.

2. Basic Notions

Our notions of sets, functions, strings and trees are standard.

In the proofs below we follow the same type of argument for several Σ_{1} level nondefinability results. For example, to show that AR is not definable by a Σ_{1} formula ∃d̄θ(x, d̄, c̄) (where the c’s are parameters), we assume that there is such a definition and derive a contradiction. First, we construct an AR degree x (with some extra properties) and, by the assumed definition, have degrees d̄ which are witness for the given Σ_{1} formula. Now we produce an ANR degree y and some d̄^{∗} such that they satisfy the same atomic diagram with the parameters c̄ as do x and d̄. This gives us the desired contradiction. (The details are provided in the constructions below). We call the given degrees originals and the new ones photocopies of the corresponding originals. We also use the following notation: for each original degree z, z^{∗} denotes the photocopy of z (for example, x^{∗} = y in the above setting).

In our constructions involving REA, we use the following limit-modulus characterization of being REA. It is the relativization of the standard modulus lemma (see [So, Corollary III.3.4]) and is important in our analyses of the REA relation.

Lemma 2.1. For A ≥_{T} B, the degree of A is REA the degree of B if and only if A(x) has a limit approximation g(x, s) ≤_{T} B with modulus function m(x) ≤_{T} A, i.e., lim_{s} g(x, s) exists and equals A(x) and the approximation stops changing by s = m(x).

3. AR, HIF ∉ Σ_{1}(≤, REA, c̄)

We begin with the easier case of HIF not being definable by a Σ_{1}(≤, REA, c̄) formula.

Theorem 3.1. HIF is not definable by a Σ_{1}(≤, REA, c̄) formula.

Proof. Suppose, for the sake of a contradiction, that HIF is definable by ∃d̄θ(x, d̄, c̄), i.e., a degree x is HIF if and only if there are degrees d_{0}, d_{1}, …, d_{n} such that θ(x, c̄, d̄) holds (where c̄ is a fixed sequence of degrees corresponding to the constant symbols c̄). (For technical convenience we assume that one of the c̄ is 0.) Now we write θ in disjunctive normal form as ψ_{0} ∨ψ_{1} ∨⋯∨ψ_{k}. We can assume that each ψ_{i} is a complete diagram in all the degrees involved. For any particular HIF x, one of these disjuncts is satisfied and we will consider it for an x of our choosing. Our plan is to construct a y and some d^{∗}’s that satisfy the same atomic diagram with the parameters c’s as x and the d’s do. For convenience we let X be the set of degrees consisting of x and the d’s and c’s.

We define the required photocopies by constructing a generic g and joining g with x to get y = x ∨ g and g with some of the d_{i}’s to get d_{i}^{∗}; other d_{i}’s remain the same.

Now let us think about which of the d_{i}’s need modification. Of course, we need to join the generic g to the d_{i}’s above x. We can choose our original x minimal (as there are minimal degrees in HIF, see [Le, Chapter V]) and so we will not have to worry about degrees below x. It is possible that some d_{j} above x is REA d_{k} while d_{k} ≱ x. We also need to add g to d_{k} in this case. Now we must iterate this process. Let Z ⊂ X be the subset of degrees generated from x which is closed upwards and closed under the REA relation (if z ∈ Z and w ≥ z or zREAw, then w is also in Z). This Z is the set of degrees we need to change.

Of course, we want to make sure that no parameter c is in Z (since we are not able to change them). By analyzing the definition of Z, it is easy to see that if some c is in Z then x is arithmetic in c (i.e., recursive in c^{(n)} for some n ∈ ω). So we need to choose our original x not arithmetic in any of the parameters c. Again we can do this since there are continuum many minimal HIF degrees.

So we start with a minimal HIF degree x (minimality here is only to guarantee that x is not REA in any degree below it) which is not arithmetic in any of the c’s and so no c is in Z. Let d_{i} be the witnesses for the Σ_{1} definition of x ∈ HIF. Now we build a generic G and let g = deg(G). Define y = x ∨ g and

d_{i}^{∗} = \{ \begin{matrix}d_{i} ∨ g, & if d_{i} ∈ Z; \\ d_{i}, & otherwise. \end{matrix}

Now we must show that (y, d̄^{∗}, c̄) satisfy the same atomic diagram as do (x, d̄, c̄). It is easy to see that all positive relations are preserved by the construction. So we only need to take care of the negative relations. We need two lemmas.

Lemma 3.2. If g is 1-generic in a∨b and a ≰ b, then a ≰ b∨g (and so a∨g ≰ b∨g.)

Proof. This is a standard fact about 1-generics. □

Lemma 3.3. If g is 2-generic in a ∨ b and a is not REA b, then a ∨ g is not REA b ∨ g (and so a ∨ g is not REA b).

Proof. By Lemma 3.2, we can assume that b < a. By the same Lemma, we may also assume that a ≤ b′ as being 2-generic in a ∨ b makes G 1-generic in a ∨ b′ and so, if a ≰ b′, a ≰ b′ ∨ g =(b ∨ g)′ as required (every 1-generic is GL_{1}). By the limit lemma then, we can fix a B-recursive approximation A_{s} to A.

By the limit-modulus characterization of being REA (see Lemma 2.1), we want to see that for any 2-generic G, there is no pair (Φ, Ψ) of reductions such that Φ^{B⊕G}(x, s) is a limit approximation of A⊕G and Ψ^{A⊕G}(x) is a modulus function for this approximation. Consider then any (Φ, Ψ).

First, we can assume that the totality of Φ and Ψ is forced and so for any σ (a possible initial segment of G) and any input (x, s), there is always a τ ⊃ σ such that Φ^{B⊕τ}(x, s) and Ψ^{A⊕τ}(x) both converge. (This is a two quantifier question and we consider only conditions σ extending the one forcing totality.)

Next, we can assume that we consider only conditions extending one forcing that Φ^{B⊕G} gives a limit computation of A⊕G and that Ψ^{A⊕G} provides a modulus function for it. (These are again guaranteed by two quantifier statements: ∀x, s∃t > s(Φ^{B⊕G}(x, t) = (A ⊕ G)(x) and ∀x, v(Ψ^{A⊕G}(x) = v → ∀v′ ≥ v(Φ^{B⊕G}(x, v′) = (A ⊕ G)(x)).) Thus if Φ^{B⊕τ′}(2x, v) ↓≠ A(x), then there is a τ′′ ⊇ τ′ and a v′ > v such that Φ^{B⊕τ′′}(2x, v′) ↓= A(x) and if Ψ^{A⊕τ}(x) ↓= v and Φ^{B⊕τ}(2x, v) ↓= a then A(x) = a.

Now we argue that in this situation we can produce a B-recursive limit computation of A with an A-recursive modulus function for the desired contradiction. Given x and s consider all v, τ ⊆ τ′, t (all bounded by s) such that Ψ_{s}^{A_{t}⊕τ}(2x) = v and Φ_{s}^{B⊕τ′}(2x, v) = a. If there are no such v, τ ⊆ τ′, t then our approximation says A(x) = 0. If every such quadruple v, τ ⊆ τ′, t gives the same value a then we say A(x) = a. If different v, τ ⊆ τ′, t give different values for a, then for each of them we look for a τ′′ ⊇ τ′ and v′ ≥ v such that Φ^{B⊕τ′′}(2x, v′) ≠ Φ^{B⊕τ′}(2x, v). By our assumptions, we must find such τ′′ and v′ for all v, τ ⊆ τ′, t with Φ^{B⊕τ′}(2x, v) ≠ A(x). Thus we are left with only one seemingly viable possible value for A(x) and we say that it is the value of our approximation at s.

We want to show that this procedure gives a correct limit computation of A(x) for each x. Consider any v, τ ⊆ τ′ such that Ψ^{A⊕τ}(2x) ↓= v and Φ^{B⊕τ′}(2x, v) ↓= a and any t such that A_{t} is correct on the use of the first computation and also larger than the number of steps needed for both computations to converge. This tuple v, τ ⊆ τ′ and t will be one we find at every s ≥ t. Moreover, the computations of Ψ_{s}^{A_{t}⊕τ}(2x) = v and Φ_{s}^{B⊕τ′}(2x, v) = a at s are correct computations from A and B. If there were any τ′′ ⊇ τ and v′ > v such that Φ^{B⊕τ′′}(2x, v′) ≠ Φ^{B⊕τ′}(2x, v) we would contradict our having forced Φ^{B⊕G} to be a limit computation of A ⊕ G with modulus function Ψ^{A⊕G}. Thus, our procedure can never eliminate the value a and so that is the limit value of our approximation. Again, by our assumptions, it is also the correct value of A(x). Finally, it is clear that A (which, remember, computes B and so the approximation A_{s} as well) can find such a stage s and so a modulus function for our approximation. □

Using Lemmas 3.2 and 3.3, it is now not difficult to argue case by case that negative relations are also preserved. Consider first two degrees a ≰ b in X. Their photocopies are either unchanged or gotten by joining with g. It is obvious that a ∨ g ≰ b. The other two cases follow from Lemma 3.2.

Now take two degrees a not REA b. If a is not Turing above b, then a^{∗} is not Turing above b^{∗} by the above argument, and so not REA b^{∗}. So we can assume that a > b. In our procedure, if we join g to b to get b^{∗}, then we also join g to a to get a^{∗}. That is, we don’t need to consider the case a not REA b ∨ g. The remaining two cases follow from Lemma 3.3.

By genericity g and so y = x ∨ g is HI ([J2]) for the desired contradiction. □

We can now note that this argument gives the analogous result for AR.

Theorem 3.4. AR is not definable by a Σ_{1}(≤, REA, c̄) formula.

Proof. We again begin with an AR minimal degree x which is not arithmetic in any of the parameters (using standard minimal degree construction with cone avoiding) and build the required photocopies as above. Now note that any 2-generic is ANR (the set of conditions making the principal function of the generic be larger (at n many inputs) than the modulus function for 0′ are dense and Π_{1}^{0}). As ANR is, like HI, closed upward, our y = x ∨ g is also ANR as required. □

Remarks. It is natural to ask whether this last result holds with REA replaced by RE. In fact, it is actually not difficult to prove, in analogy with Lemma 3.3, that if a is not r.e. in b (not necessarily above), and g is 1-generic in a ∨ b, then a is not r.e. in b ∨ g either. Indeed if A is not r.e. in B then A ⊕ G is not r.e. in B ⊕ G. However, we do not know whether the degree a ∨ g is r.e. in b ∨ g or not.

In addition, as pointed out by an anonymous referee, based on the proofs above, we can actually show that HIF (or AR) is not definable by Σ_{1} formula in the language of order, jump and REA, i.e., we can add the jump to the language.

First of all, we need to split the formulas regarding double (or higher) jumps into single ones. For example, x′′ = b is rewritten as (x′ = y) ∧ (y′ = b) (with y bounded by an existential quantifier), so for our purpose we can regard the jump as a binary relation symbol.

The construction is essentially the same as in the proof above. We pick a sufficiently generic degree g and join it with the degrees in Z. Now we only need to show that both positive and negative “jump relations” are preserved.

Consider a = b′ as originals. If we join g to a in the construction, then we have to join g to b as well (since a is REA b). Note that 1-generic degrees are GL_{1}, and it easily relativizes to (b ∨ g)′ = b′ ∨ g = a ∨ g. Therefore the positive jump relations are preserved.

For the negative ones, by Lemmas 3.2 and 3.3, we only need to consider the case when a is REA b but a is not b′. Now again by Lemma 3.2, a ∨ g is not above b′ for any g which is 1-generic in a ∨ b′, therefore a ∨ g ≠ (b ∨ g)′.

Our results in Section 7 now follow as a corollary. We nonetheless provide a separate proof there because it illustrates a different approach and directly answers Miller and Martin’s original question.

4. Decidability of the Σ_{1} theory of (D, ≤, REA)

The construction in the previous section heavily uses the given partial order of the originals to preserve the positive relations. This idea cannot be used to solve similar problems for HI and ANR simply because both classes are upward closed and so, for example, there is no way to build a degree y above a given ANR x as its photocopy and have y be AR. So what we need to do is to build some photocopy y with some d^{∗}’s by some different construction and still make them look like the originals.

This is in general not easy: In addition to building such a y, we also need to build some d^{∗}’s satisfying some given order and REA relations. Especially in the ANR case, we probably need to build some d^{∗} below y such that y is REA d^{∗}. (Recall that every ANR degree is RRE, i.e. it is r.e. in some degree strictly below it [CS]). So as the first step towards the solution of our problem we try to investigate the embedding problem, i.e., which (finite) partial orders with some extra REA relations and their negations can be embedded into the Turing degrees (D, ≤, REA).

We begin by listing some obvious properties that such a partial order must satisfy. To simplify our analysis we take the REA relation to mean r.e. in and strictly above. This certainly entails no loss of generality as each version of the relation is definable from the other by a quantifier free formula.

Definition 4.1. An REA partial order (REA-PO) is a partial order ≤ with an extra binary relation REA satisfying the following two axioms:

Strict-Order: a REA b ⇒ a > b.

Transitivity: a REA b ∧ a > c > b ⇒ a REA c.

It is easy to see that, if one takes a finite collection of Turing degrees and considers the REA relations among them, they form an REA-PO with the natural definitions of the order and REA relations. Not too surprisingly, the converse also holds (although the proof is not as easy as might be expected).

Theorem 4.2. Every finite REA-PO can be embedded in (D, ≤, REA).

The proof of this theorem has several pieces.

Suppose we are given a finite REA-PO A = {a_{1}, a_{2}, …, a_{n}}. For each a_{i}, we want to construct a set G_{i} and some pairs l_{i}^{j}’s and m_{i}^{j}’s of functions. The G_{i} are generic objects similar to the ones used for the standard embedding of finite partial orders in D. Each pair l_{i}^{j}(x, s) and m_{i}^{j}(x) is devoted to the REA requirement a_{i} REA a_{j}. We try to make l_{i}^{j}(x, s) a limit computation of the set A_{i} we want to build of degree a_{i} with m_{i}^{j}(x) a modulus function for this approximation (see Lemma 2.1).

The degrees we are going to construct are defined inductively from the bottom of our REA-PO up. We let:

(†) : A_{i} = G_{i} ⊕ ⨁_{a_{i}>a_{j}} A_{j} ⊕ ⨁_{a_{i}REAa_{j}}(l_{i}^{j} ⊕ m_{i}^{j}) ⊕ ⨁_{a_{k}REAa_{i}} l_{k}^{i}.

Each A_{i} is simply a join of G’s, l’s and m’s. We let a_{i} = deg(A_{i}). (Note that each A_{i} is a function.) We say that the sets and functions (G’s, l’s and m’s and other A’s) mentioned in this formula appear in (the definition of) A_{i}.

4.1. Forcing notion. We now define a notion of forcing P. A condition in P is a collection p of finite initial segments of the G, l, m’s as above such that each m_{i}^{j} appears to be a modulus function for l_{i}^{j} which limit computes A_{i} as far as m_{i}^{j} can tell. This means that when m_{i}^{j}(x) has been defined at some x, then the corresponding limit computation l_{i}^{j}(x, s) cannot change beyond s = m_{i}^{j}(x), and the final value l_{i}^{j}(x, m_{i}^{j}(x)) equals A_{i}(x), which we require to be defined if m_{i}^{j}(x) has been defined.

We say such pair l_{i}^{j}(x, s), m_{i}^{j}(x) (or any one of them) is associated with the value A_{i}(x) (and vice versa). Note that in A_{i}, such m_{i}^{j}(x) is always coded in a position after A_{i}(x) by the formula (†) above (i.e., m_{i}^{j}(x) = A_{i}(x′) where x′ > x). This fact will be useful later.

A forcing condition q extends p if each finite initial segment extends the corresponding one. (This automatically implies that q does not violate the l-m rules p imposes.) It is easy to see that both the set of forcing conditions and the extension relation are recursive.

4.2. Positive order and REA requirements. To see that positive order requirements (A_{j} ≤_{T} A_{i}) and positive REA requirements (A_{i} REA A_{j}) are satisfied, we only need to show that, given a forcing condition p, one can find an extension q of p where the domains of A_{j} and A_{i} are extended, or equivalently, it suffices to know how to extend individual sets or functions G, l, m’s.

Note that in a forcing condition, it is possible that A_{i}(x) is defined but some associated limit computation l − m has not yet settled down, i.e., m_{i}^{j}(x) is still undefined.

To extend G, we simply extend it (indeed, arbitrarily) without changing anything else. It is easy to see that the extension q we get satisfies the definition of a condition.

To extend l, we only need to follow the rules m set up. That is, if some m_{i}^{j}(x) has been defined, then l_{i}^{j}(x, s) for s ≥ m_{i}^{j}(x) has to be defined to be the same as A_{i}(x). If the corresponding m has not yet been defined, then we can extend l freely.

To extend m, we first recall that, in the formula defining A_{i} ((†) as above), any modulus value m_{i}^{j}(x) is coded at a position x′ after the value A_{i}(x) with which it is associated. Therefore here we can assume that this A_{i}(x) value has already been defined. Then we find the initial segment where the corresponding l_{i}^{j} function has been defined. We may need to extend l_{i}^{j} for one more change to make it agree with the value of A_{i} it limit computes. Then we can define m_{i}^{j} to be the last number at which l_{i}^{j} changes. For example, suppose we want to define m_{i}^{j}(x). At the moment l_{i}^{j}(x, s) has been defined up to some s_{0} and the last value is t, where A_{i}(x) = t′ which might be different from t, and so we need to extend l_{i}^{j}(x, s) further with value t′. Then we define m_{i}^{j}(x) to be the last s where l_{i}^{j}(x, s) changes (for example, in this case m_{i}^{j}(x) = s_{0} +1).

Therefore when we construct a generic filter and let a_{i} = deg(A_{i}) all the positive order and REA requirements are automatically satisfied.

Now we must show that the negative order and REA relations in our REA-PO are also preserved. We first consider the nonorder requirements and argue that sufficient genericity suffices to satisfy them.

4.3. Negative order requirements. Say we have a fixed requirement A_{i} ≠ Φ(A_{j}) and a forcing condition p, and we want to find a forcing condition q extending p which forces A_{i} ≠ Φ(A_{j}).

Our construction here is not the easiest possible, but we want to introduce a module of “modification” that we will use later for the negative REA requirements.

We pick the first undefined number G_{i}(x′) = A_{i}(x) (this implies that all associated modulus m_{i}^{k}(x)’s are undefined in p). We ask whether there is a forcing extension q of p which forces Φ(A_{j}; x) ↓. If not, then p already forces A_{i} ≠ Φ(A_{j}). If so, we pick such q and check if its A_{i}(x) equals Φ(A_{j}; x) or not. Note that if A_{i}(x) is still undefined, then as argued in §4.2, we can extend q and define A_{i}(x) to be any value we want, and in particular we can make it different from Φ(A_{j}; x). If at p, A_{i}(x) is different from Φ(A_{j}; x), then p already forces A_{i} ≠ Φ(A_{j}). So we only need to handle the case when G_{i}(x′) = A_{i}(x) = Φ(A_{j}; x) at p.

Now the plan is to change q to q′ by modifying A_{i}(x) together with some associated l-m pairs. We call this a modification process. In q, we first change G_{i}(x′) = A_{i}(x) to be a different value. This value is associated with some limit computation l-m pairs (l_{i}^{k}(x, s)-m_{i}^{k}(x)) for A_{k} limit computing A_{i}. In order to make a new forcing condition q′, we may need to change some of the values of some of these l-m pairs. In this case, for each l-m pair whose limit value needs modification, we make m(x) large and extend l to change the limit value without changing the current values. For example, if the current m_{i}^{k}(x) has been defined and l_{i}^{k}(x, s) has been defined up to s = s_{0}, then we let the new value of m_{i}^{k}(x) be s_{0} + 1, and extend l_{i}^{k}(x, s) to change the limit value at s_{0} + 1 which agrees with the new A_{i}(x).

Note that in the forcing notion, each l_{i}^{k} limit computation corresponds to a unique modulus m_{i}^{k}, and so here there is no worry that the extended limit computation function l_{i}^{k} conflicts with other coding requirements.

For each m value modified, we need to inductively change its own associated limit computation (as a value of A(x)) in the same way. We will see that we eventually finish this modification process and get a new forcing condition q′ where A_{i}(x) is different.

Briefly, we have a queue of l-m pairs we need to modify. Each time we pick the first one from the queue, change its m value and extend l, and then add all existing l′-m′ pairs for limit computing the m value we just modified into the end of the queue. As we noted earlier, for such l′-m′ pairs, the m′ value is coded after the m value it is associated with, so this modification process will eventually stop.

Now we want to show that in q′, the computation of Φ(A_{j}; x) remains the same as that in q, i.e., the use of A_{j} is unchanged. Each m_{i}^{k} (the modulus of some limit computation for A_{i}) only appears in A_{i} and all A_{l} above A_{i}, therefore it is not difficult to prove by induction that in the above modification process, the only modified values are in A_{i} or in some A_{l} which are above A_{i}. Since a_{j} ≱ a_{i}, A_{j} will not be changed up to the use of Φ(A_{j}; x) at q. So the new forcing condition q′ forces A_{i} ≠ Φ(A_{j}). Here is the lemma (as proved above) which we will need later for the REA case.

Lemma 4.3. In this modification process, the only changed values (other than the initial one at G_{i}(x′) = A_{i}(x) are in m’s that correspond to limit computations of A_{i} or some A_{l} above A_{i}.

In addition, note that we chose A_{i}(x) to be undefined at p, and if some modulus function m is defined at p, then the associated A value is also defined at p (see definition of the notion of forcing in §4.1). Then it is easy to prove by induction that none of the modified values from q to q′ are already defined at p. As a result, q′ still extends p. This shows that we can always find an extension of a given p which forces A_{i} ≠ Φ(A_{j}).

4.4. Negative REA requirement. Now we want to deal with negative REA requirements: ¬(A_{i} REA A_{j}). First of all we only need to handle this requirement for pairs A_{i} > A_{j}. In addition, by the Transitivity Axiom we know that there is no a_{k} < a_{j} such that a_{i} REA a_{k}. This will turn out to be the crucial property we need to show that the A_{j} part of a condition is not changed in some modification processes. For example, for all l-m pairs in A_{i} which aim to limit compute A_{i}(G_{i}), neither l nor m appears in A_{j}. This fact will be used in the proof that A_{j} is unchanged after some modification process (see Lemmas 4.4 and 4.7).

Recall that we need to make sure that the degree of A_{i} is not REA the degree of A_{j}, so in order to satisfy the requirement, we need to make sure that none of the pairs λ(x, s) = Λ(A_{j}; x, s) and μ(x) = M(A_{i}; x) form a limit computation-modulus function pair for computing A_{i}. So suppose we are given a forcing condition p and such a pair of functionals (Λ, M) and we want to find a q which forces that (Λ, M) is not a limit computation pair for A_{i}. We use the notation M_{p}(α_{i}; x) to mean M(α_{i}; x) where α_{i} is the finite initial segment of A_{i} in the forcing condition p.

First we try to force totality of both functionals. We ask whether there is a forcing extension q ≤ p and a pair ⟨x, s⟩ such that no r < q makes Λ_{r}(α_{j}; x, s) converge. If so, q already forces the requirement. Similarly we can force the totality of M(A_{i}).

Now we ask if there is a forcing extension q of p and an x which sees that M_{q}(α_{i}; x) is not the modulus of Λ_{q}(α_{j}; x, s), i.e., M_{q}(α_{i}; x) ↓= t but Λ_{q}(α_{j}; x, s) changes after t. If so, such q also forces the requirement.

Similarly we can also ask if it is the case that the final value does not equal A_{i}(x). If so, we are also done. So if none of these questions have a positive answer, then we have a forcing condition p which forces totality of both Λ and M (in a weak sense as above), and forces that M is a modulus for Λ limit computing A_{i} in the sense that for every x and for every extension q ≤ p, if M_{q}(α_{i}; x) converges, then Λ_{q}(α_{j}; x, s) stops changing within modulus M_{q}(α_{i}; x), and the final value equals α_{i}(x) (at q).

Now we want to derive a contradiction. Similar to the negative order construction above, we find the first x such that A_{i}(x) = G_{i}(x′) has not yet been defined at p. The plan is to use what we have forced above to construct an extension of p which forces that (Λ, M) is not a limit computation pair witnessing A_{i} REA A_{j}. In other words, we want to derive a contradiction and so the above scenario cannot happen in the construction.

By our assumption, we can find an extension q ≤ p such that A_{i}(x), M_{q}(α_{i}; x) = s_{0}, Λ_{q}(α_{j}; x, s_{0}) = A_{i}(x) have all been defined.

In q, we want to change A_{i}(x) = G_{i}(x′) (say = 0) to a different value (1). In order to make a new forcing condition, we may have to change various l-m functions as well.

The plan here at this step is the same as that in the negative order construction (§4.3): For each l-m pair we need to modify, we change the value of m to a large number and extend the l part. So the values that need to be changed are all in m’s. It follows by induction that these values are in some m’s that only appear in A_{i} or in A’s above this A_{i}. In particular, the A_{j} part of q is preserved in this process (Lemma 4.3). Let us call the new forcing condition q′. Also note that by the same argument as in the last paragraph of §4.3, this q′ extends our original forcing condition p.

Now again by our assumption, we can extend q′ to r′ where M_{r′}(α_{i}; x) ↓= s_{1} and Λ_{r′}(α_{j}; x, s_{1}) = 1, i.e., the new value of A_{i}(x). It is obvious that s_{1} > s_{0} since q′ does not change the A_{j} part of q and so Λ_{q′}(α_{j}; x, s_{0}) = Λ_{q}(α_{j}; x, s_{0}) = 0.

Then we want to change r′ “back” to r such that the A_{i} part is changed back to what it was in q. That is, change A_{i}(x) back to 0 and do another chain reaction modification.

The modification process here is a bit trickier than what we used above to go from q to q′. The new rule is as follows: Step by step we modify values and add the new l-m pairs we need to modify to the end of a queue. Each time we take the first pair from the queue. If the place at which the m in the l-m pair needs modification is z and m(z) = A_{i}(z′) is already defined at q, then we change m(z) back to its old value at q and change all l values after the old modulus at q back to their old limit values. Then, we add all existing l′-m′ pairs for computing m and the l values we just modified into the queue. Otherwise (even if they are in the current A_{i} but the m value is not defined at q) we redefine m to be large and extend the l part, and add the associated l′-m′ pairs for computing m to the queue. (The reason why this process will eventually stop requires some extra work, see Lemma 4.5 below.)

In the first option, we say both l and m are modified, and in the second option, we say m is modified but l is extended.

Now we need a few lemmas to show that this new forcing condition r gives a desired contradiction.

Lemma 4.4. The values that are modified in this process are either in l’s appearing in some A_{k} that enumerates A_{i} (and hence not below A_{j}) or in m’s appearing in sets above any of these A_{k}’s or A_{i}.

Proof. When we changed q to q′, the modified values are in m’s which are modulus functions which correspond to limit computations for A_{i} or for some A_{l} above A_{i} (Lemma 4.3). So here when we apply the first option modification, it must be the case that the m’s we changed back correspond to limit computations that compute A_{i} but do not appear in any sets strictly below A_{i}. Therefore according to the construction, the only case in which some l values get modified is when they are in some A_{k} that enumerates A_{i}. The second option modification only changes m without changing l (i.e., the chain reaction for such modifications only result in modifying functions appearing in higher A’s), and so the lemma follows. □

Lemma 4.5. The second modification process eventually stops.

Proof. By the proof of the previous lemma, the only modified l values are those which are used for some A_{k} enumerating A_{i} and which were extended in the first modification process (from q to q′). There are only finitely many l positions to modify, and remaining modifications happen only in modulus values which are coded after the values they are associated with. Therefore the modification eventually stops, as the forcing condition is finite. □

Lemma 4.6. After this modification, r is a valid forcing condition.

Proof. This is straightforward. In both cases, when we change some value A(z) which has limit computation l-m, we always guarantee that we modify (or extend) this pair as well so that the limit computation is correct. □

Lemma 4.7. After this modification, the A_{j} part of r′ is compatible with that of r.

Proof. By Lemma 4.4, no values in A_{j} will be modified in this construction (though it may get extended). □

Lemma 4.8. After this modification, the A_{i} part of r is compatible with that at q.

Proof. In particular, this is because the values that need second option modification in sets below A_{i} are all undefined at q. When we changed q to q′, we modified m and extended l, and so when we change m back, all l’s that are modified are undefined at q. Now it is not difficult to prove that step by step following the same procedure as in the modification from q to q′, the first option changes A_{i} back to its old version at q. □

It is also easy to prove by induction that r < p since none of these modifications affect p where A_{i}(x) is undefined. Now we get a contradiction. By Lemma 4.8 M_{r}(α_{i}; x) = M_{q}(α_{i}; x) = s_{0} but by Lemma 4.7 Λ_{r}(α_{j}; x, s_{1}) = Λ_{r′}(α_{j}; x, s_{1}) = 1 ≠ A_{i}(x). This finishes the proof of Theorem.4.2.

Corollary 4.9. The Σ_{1} theory of (D, ≤, REA) is decidable.

Remark. It is possible to prove Theorem 4.2 for countable REA-PO’s by modifying the notion of forcing to allow the sets and functions to be drawn from the natural countable set but restricting any condition to mention only finitely many of them.

5. Some nondefinability corollaries

We first try to analyze the construction of the previous section and see how low down in the degrees we can embed our REA-PO.

It seems that we asked 0′′ questions in satisfying the negative REA requirements. However, the proof can be rephrased as a 0′ construction.

We start with p and pick A_{i}(x) to be undefined. We first try to force M(α_{i}; x) to converge (one question to 0′) and if this is possible we then try to force convergence of Λ(α_{j}; x, M(α_{i}; x)) (one question to 0′). So we get a forcing extension q ≤ p.

We change q to q′ as in the proof by changing the value of A_{i}(x) (recursive construction) and extend q′ to r′ (again two questions to 0′). Then we change r′ back to r by changing A_{i}(x) back (recursive construction) and the proof ensures that r extends p and forces that A_{i} is not limit computed from Λ(A_{j}) via modulus M(A_{i}).

In summary, we only need to ask at most four questions to 0′ to get the forcing extension we need. Moreover, it is easy to see that forcing negative order requirements only requires one question to 0′, and one can add in requirements to force the jump of each A_{i}, so by standard arguments one can embed the REA-PO in the superlow degrees (a degree a is superlow if a′ ≤_{wtt} 0′). Every superlow degree is array recursive (see [Sc, Prop 6.3]), and so every finite REA-PO can be embedded into the array recursive degrees. By a similar argument as before, we get the following:

Theorem 5.1. ANR is not definable in (D, ≤, REA) by a Σ_{1} formula.

In addition, we get the exact definability bound of the Turing jump in (D, ≤, REA):

Theorem 5.2. The Turing jump is definable in (D, ≤, REA) by a Π_{1} formula but not by a Σ_{1} formula.

Proof. For the claim about definability, note that y = x′ is the maximum degree which is REA x, i.e., y = x′ if an only if (y REA x) ∧ ∀z(z REA x ⇒ z ≤ y).

For the nondefinability claim, assume that the jump is defined (as a relation) by ∃d̄θ(x, y, d̄). Consider any y = x′ and the corresponding witnesses d̄. One can embed the REA-PO given by x, y, d̄ into the superlow degrees and there the photocopy y^{∗} cannot be the jump of x^{∗}, which gives the desired contradiction. □

It is not difficult to see that we can embed a finite REA-PO into Arith, the degrees of arithmetic sets, and also into non-Arith, the complementary class of degrees of nonarithmetic sets. Therefore the same argument as above yields the following.

Theorem 5.3. Arith is not definable in (D, ≤, REA) by a Σ_{1} or Π_{1} formula.

6. r.e.,non-r.e. ∉ Σ_{1}(≤, REA)

In this section we use the same methods to show that “r.e. in” (y is r.e. in x) is not definable in (D, ≤, REA) by a Σ_{1} or a Π_{1} formula.

First of all, to show that “not r.e. in” is not definable by Σ_{1} formula, we start with incomparable originals x and y such that y is not r.e. in x (simply take two minimal degrees that are “far away” from each other). Now we have a list of witnesses d̄ and an REA-PO (x, y, d̄).

To this REA-PO we add a new element m and make it below both x and y, and so m is automatically below the elements which are above either x and y. In addition, we make it incomparable with all the other elements (elements that are above neither x nor y). For the REA relation, we make y REA m but no other new REA relation hold. It is not difficult to check that the new partial order (x, y, m, d̄) is an REA-PO, and so by Theorem 4.2 we can embed this REA-PO into (D, ≤, REA). After removing the degree which corresponds to m, we get photocopies of our original degrees with the desired contradiction that y^{∗} is now r.e. in x^{∗} since it is REA in m which is below x^{∗}.

To show that “r.e. in” is not definable by Σ_{1} formula, we need a bit more work. We start with incomparable originals x and y such that y is r.e. in x and y is minimal. (We can find such a pair by, for example, the construction of a minimal degree which is Σ_{2} but not Δ_{2} from [S2].)

Now by our argument we have an original REA-PO (x, y, d̄) with the extra property that there is no d below both x and y such that y bounds some z which is REA d (by our extra condition on x and y above).

We follow the same forcing construction as in Theorem 4.2 to make photocopies with an extra requirement that y^{∗} is not r.e. in x^{∗}.

So it suffices to deal with this extra requirement here. For convenience we use a_{j} and a_{i} to respectively denote x and y (so we want to make deg(A_{i}) not r.e. in A_{j}).

Here we want to diagonalize against all triples of functionals (Φ, Ψ, W) where Φ and Ψ give the reductions between A_{i} and some set Y in the same degree (Ψ(Φ(A_{i})) = Ψ(Y) = A_{i}), and W (A_{j}) gives an A_{j}-r.e. set which equals Y.

Of course we can start to diagonalize against a given triple (Φ, Ψ, W) by asking whether we can force Φ or Ψ to be partial, or if their composition gives some set which is different from A_{i}, or whether we can force Y = Φ(A_{i}) ≠ W (A_{j}). If all these attempts fail, we show that along the generic filter Y ≤_{T} A_{j} and so get a contradiction (we can make A_{i} and A_{j} Turing incomparable).

We only need to show that Y is co-r.e. in A_{j}. To tell if some y ∉ Y, we try to find a forcing extension q of p such that the A_{j} part of q is the true one (agrees with the generic filter in the end) and Φ_{q}(α_{i}; y) = 0. Whenever we find such q we claim that y ∉ Y.

It is easy to see that if y is not in Y, then along the generic filter we can always find such a forcing condition q. The hard part is to show that if y is in Y then we cannot find such q. We assume for a contradiction that there is a q ≤ p such that its A_{j} part is correct (compatible with the generic filter) and Φ_{q}(α_{i}; y) = 0 but W (A_{j}; y) = 1. Now we want to extend this q to get a forcing condition which forces that Φ(A_{i}) ≠ W (A_{j}). The idea is, of course, that we can extend the α_{j} part of q until we see W (A_{j}; y) = 1. The problem is that, q might have promised some modulus requirements which may not be compatible with the real A_{j} up to the use which enumerates y into W (A_{j}).

This is handled in a modification process similar to what we used in Section 4. Starting from q, we extend the α_{j} at q following the real A_{j} up to the use of W (A_{j}; y) = 1. If the added values do not cause a contradiction (i.e., they still obey the forcing condition requirements), then we do nothing. Once we detect that there is a contradiction, we want to modify some values. The contradiction comes from either G, l or m which appears in A_{j}. There will be no problem for m, because the corresponding limit computation l also appears in A_{j} (we know A_{j} itself, which comes from the generic filter, is consistent); there will be no problem for G either, since at q, if we have decided some modulus function, then the corresponding G is also defined. The only trouble is to extend l where the m function does not appear in A_{j}. For example, some m function (appearing in some A_{k} REA A_{j}) may have decided a small modulus, but A_{j} may have changes after that small modulus.

Once we see such a situation, we know that this pair l-m needs modification and add them to the queue. The modification process goes exactly as in §4.3, i.e., we change the modulus to be large and extend the limit computation, then add in the corresponding l′-m′ we need modify into the end of the queue.

Lemma 6.1. The values that are modified in this process are m values which appear in some A_{k} which is REA some A_{l} appearing in A_{j} (including A_{j} itself), or a set above any of such A_{k}’s. In addition, such A_{k} do not appear in A_{j}.

Proof. By our argument above, the first modification happens when A_{j} contains some limit computation l but not the modulus, which corresponds to limit computing some A_{k} REA A_{l} in the lemma. Then the chain reaction only happen at m’s which are above such A_{k}’s. Since A_{j} does not contain the modulus which needs modification, such A_{k} are not below A_{j}. □

By our extra condition (recall that x is minimal and so not above any degree REA any degree below y) and by the above lemma, one can see that A_{i} will remain unmodified in the process. Also by the lemma, we know that A_{j} will remain unmodified (but could be extended). So we can get a new forcing condition q′ < p (it is easy to see that the p part of the forcing condition is unmodified in the process) such that its A_{i} part is the same as that in q (Φ_{q′}(α_{i}; y) = Φ_{q}(α_{i}; y) = 0) but W_{q′}(A_{j}; y) = 1. This gives the desired contradiction.

7. ANR, HI ∉ Σ_{0}(≤,′ , c̄)

With the jump added to our language, things get more complicated. Suppose we need to build two degrees y > x. When we build x, there is a lot of freedom to choose y. Even if we require y REA x, we can still choose from a countable class of degrees. However if we have y = x′, then we have no choice at all when we fix x. In particular, the following question is still open:

Question 7.1. Which degrees above 0′ are jumps of HIF degrees?

We don’t even know whether this class (jumps of HIF degrees) is closed downwards (for degrees above 0′, of course).

This is actually a big obstacle for nondefinability results even in the quantifier-free case. For example, it is hard and sometimes impossible to construct an HIF degree whose jump is above a fixed c > 0′ (If the jump of a degree is above 0′′, then the degree is automatically hyperimmune, see for example [J1]). Miller and Martin conjectured that HI is not definable by quantifier-free formulae in (≤,′ , c̄), and here we confirm this conjecture by proving the equivalent proposition that HIF is not quantifier-free definable.

Theorem 7.1. HIF is not definable by a quantifier free formula in (≤,′ , c̄).

Proof. Using the same type of argument as in §3, we have an original x which is HIF and a quantifier free definition of HIF with constants c̄. As before, we will choose a particular x. For example, we can take our x to be incomparable with all nonrecursive constants appearing in the formula. We regard all the jumps of constants as constants, i.e., for each constant c, if c′ appears in the formula we will add a new constant c̃ and add c′ = c̃ as a conjunct (for convenience we still write c′ but regard it as a constant). Once x is chosen, we can assume that our formula is a conjunct of atomic formulas or their negations which specify a complete diagram in ≤ for the (finitely many) x, x′, … and c̄ appearing in it.

We now think of the conjuncts (atomic formulae or negations of atomic formulae) appearing in our formula as a list of requirements. We can remove the requirements that involve a degree and its own jump (or iterated jumps) such as x ≤ x′ or x′ ≤ x′′′ which, by basic results about the jump, must be satisfied by all degrees. Similarly we omit any conjunct of the form 0 ≤ z. We can also assume that no obviously false conjuncts are included, i.e. the diagram is consistent with the axioms for a jump partial order ([HS]).

So the remaining requirements look like the following:

ψ : P (x′) ∧ ⋀_{i∈I_{1}}(x ≰ a_{i}) ∧ ⋀_{i∈I_{2}}(b_{i} ≰ x),

where P (x′) is the collection of all conjuncts about x′ (or higher jumps such as x′′ and x′′′) but not about x.

Our plan is to build a photocopy hyperimmune degree y whose jump is x′ (so y automatically satisfy P (x′)) and such that y satisfies all remaining conjuncts in ψ. Then we get our contradiction because y satisfies ψ, but is hyperimmune.

To get such a degree we build y low above x. This guarantees that its jump is the same as x′ and it is hyperimmune since it is relatively Δ_{2} ([MM, Theorem 1.2]). (Note that using x′ as an oracle, it is easy to make sure that y ≤ x′.) We use finite forcing to build initial segments σ_{i} recursively in x′ and let ∪_{i}σ_{i} = Y. We then take y = deg(X ⊕ Y) where X ∈ x and so guarantee that y ≥ x. In the construction we force the jump of X ⊕ Y as we go along. Therefore (X ⊕ Y)′ ≤_{T} X′, i.e., y′ = x′. To finish the proof we discuss how to satisfy all the requirements in the conjuncts listed in ψ.

Avoiding lower cones (y ≰ a_{i}) is automatic: each a_{i} is not above x, so it cannot be above y as y ≥ x.

For upper cones, note that we only need to consider those b_{i}’s that are below x′: otherwise y cannot be above such b_{i}. Now given σ we can ask whether there are two extensions τ_{0} and τ_{1} of σ such that (X ⊕ τ_{0})|_{e}(X ⊕ τ_{1}), i.e., there is an n such that φ_{e}^{X⊕τ_{0}}(n) ↓≠ φ_{e}^{X⊕τ_{1}}(n). If so, we take the one which differs with a fixed B_{i} ∈ b_{i}. If not, we can easily argue that the function φ_{e}^{X⊕Y} is recursive in X if it is total, and so it is not equal to B_{i} as b_{i} ≰ x. In either case we can satisfy the requirement b_{i} ≰ y. □

Corollary 7.2. AR is not definable by a quantifier free formula in (≤,′ , c̄).

Proof. As HIF implies AR, we can begin with a quantifier free definition of AR in (≤,′ , c̄) and analyze it as in the proof of the Theorem for the same x. The same construction of y can easily be augmented to make it ANR simply by making its principal function infinitely often be larger than the modulus function for 0′ while staying recursive in x′. This produces an ANR degree y which, as above, satisfies the assumed quantifier free definition of AR for the desired contradiction. □

8. HI, ANR ∉ Σ_{1}(≤, c̄)

Theorem 8.1. HI and ANR are not definable by Σ_{1}(≤, c̄) formulas.

Proof. The proof is essentially the same for both classes. We give the analysis for HI and simply note any comments needed for ANR in brackets []. We follow the same general strategy and use the same notations as in the previous sections. That is, we have a hyperimmune [array nonrecursive] degree x and a sequence of witnesses d_{0}, …, d_{n} which satisfy a Σ_{1} formula ∃d̄φ(x, d̄, c̄) where c’s are parameters. We write φ in disjunctive normal form and by a suitable choice of x can pick one disjunct ψ (which is a conjunction of atomic formulae or their negations) which says that x is not in the lower cone or the upper cone of any c_{i}. Our plan is to find some new d_{0}^{∗}, …, d_{n}^{∗} and a new hyperimmune-free [and so array recursive] y which satisfy ψ.

Recall our notation which, given an original degree z, has z^{∗} denote the corresponding photocopy. In this construction, if z = x, then z^{∗} = y; if z = d_{i}, then z^{∗} = d_{i}^{∗}; and if z = c_{i}, then z^{∗} = c_{i}. In the same fashion, if we have a set S of degrees, we let S^{∗} = {z^{∗} : z ∈ S}. Now we fix S as the set of degrees x and all d_{i} which are below x.

We will need to impose some extra conditions on ψ before we begin our construction but initially our plan is as follows: First, we find y and some degrees d_{i}^{∗} below it such that the these degrees provide the same partial order on S^{∗} as that given on S by x and the d_{i}’s below x. We then use a construction similar to the one used in Section 3 to build the other d^{∗}’s above members of S^{∗}.

For convenience we let d_{0}, …, d_{l} be the d’s below x. The problem is that, for example, if d_{0} is below some c_{i}, then it is difficult to build our d_{0}^{∗}. In particular, it might be very hard to make it hyperimmune-free (as we need to make y hyperimmunefree [and so array recursive]).

Thus we also assume that in ψ, there is no formula of the form d_{i} ≤ c for 0 ≤ i ≤ l and any constant c. The reason we can make this assumption is that we can take x to be a hyperimmune degree which avoids all upper cones above any nonrecursive d which is below any constant c. This is a countable list of requirements and we can use standard constructions to get a 1-generic hyperimmune [and so array nonrecursive] degree which avoids these cones.

Now we follow our plan: first we build y and d_{0}^{∗}, …, d_{l}^{∗} which provide the same partial order on S^{∗} as x and d_{0}, …, d_{l} do on S and make sure that y is hyperimmunefree [and so array recursive] and the following holds:

(∗) For any subset of degrees T^{∗} of S^{∗}, any finite set R of constants and any fixed degree z among the x, c_{i}’s and d_{i}’s, if the join of all degrees in T ∪ R is not above z, then the join of all degrees in T^{∗} ∪ R is not above z^{∗}.

This property seems ad hoc, but in fact it is natural and essential in the construction. For example, it implies that y is not above or below any of the c_{i}’s. Later this property will also guarantee that when we construct other d^{∗}’s, we do not get a degree which is too high by joining it with some degrees we already have.

To carry out the construction of S^{∗} with property (∗), we use the uniform tree constructions using usl tables which are used to build initial segments of D and with which we assume familiarity (see [Le, Chapter VI]). We need to satisfy the usual conditions preserving the usl relations as given by those on S as well as those that force totality to guarantee that the degrees constructed (and in particular the top one y) are hyperimmune-free. We do not need to satisfy the most complicated conditions that would make S^{∗} an initial segment but do need some extra requirements to satisfy (∗).

Consider a tree and a requirement Z^{∗} ≠ φ_{e}^{⨁ D_{i}^{∗}⊕⨁ C_{i}} (where Y may be viewed as included among the D_{i}^{∗}). If Z is some constant C, then we simply ask whether we can find e-splittings on the tree for φ_{e}^{⨁ D_{i}^{∗}⊕⨁ C_{i}}. If so, we can choose one to diagonalize against Z. If not, then it is easy to see that, if φ_{e}^{⨁ D_{i}^{∗}⊕⨁ C_{i}} is total, Z ≤_{T} ⨁ C_{i} which contradicts our assumption. If Z is X or some D_{j}, then we pick two nodes τ_{0}, τ_{1} on the tree which are congruent modulo ⨁ D_{i}^{∗} but disagree on Z^{∗} (say, at x). This is possible since Z ≰_{T} ⨁ D_{i} and by our usl representation we are able to make Z^{∗} ≰_{T} ⨁ D_{i}^{∗}. Then, we try to extend τ_{0} to τ′ where we have a convergent computation of φ_{e}^{⨁ D_{i}^{∗}⊕⨁ C_{i}}(x). If there is no such τ′, then we take the full subtree above τ_{0} to satisfy our requirement. If there is such a τ′, then we extend τ_{1} in the same way to τ′′ such that τ′ and τ′′ are congruent modulo ⨁ D_{i}^{∗} (by uniformity). Therefore at τ′ and τ′′, the computations φ_{e}^{⨁ D_{i}^{∗}⊕⨁ C_{i}}(x) give the same value. We can pick one whose Z^{∗}(x) is different from this value and take the full subtree above it.

Now we need to show that these d_{i}^{∗}’s satisfy the same relations with the constants as their originals: For each original d_{i} (i = 1, 2, …, l or x), d_{i} is not in any of the upper or lower cone of any constant c. So we only need to show that d_{i}^{∗} is incomparable with each of the constants. It is not difficult to see that these relations are guaranteed by property (∗).

Next let d_{l+1}, …, d_{k} be the d’s that are above any degree in S. We need to build new d_{l+1}^{∗}, …, d_{k}^{∗} which satisfy the same diagram (we regard the remaining d’s as constants). This construction follows the same idea as in Section 3. We find g_{l+1}, …, g_{k} which are mutually 1-generic over S^{∗} ∪ R where R is the set of all constants. We let the d^{∗}’s be the following joins:

d_{i}^{∗} = ⋁_{d_{j}≤d_{i}} g_{j} ∨ ⋁_{z≤d_{i},z∈S∪R} z^{∗}.

We need to show that each d_{i}^{∗} (among d_{l+1}^{∗}, …, d_{k}^{∗}) satisfies the same relations with different z^{∗} as its original d_{i} does (with z). We discuss this by cases:

If z is below d_{i}, then it is automatic by the definition of d_{i}^{∗} that z^{∗} ≤ d_{i}^{∗}. If z is above d_{i}, then it can only be the case that z is some d_{j} and we are back in the first case. So we only need to take care of the negative order relations that say z is incomparable with d_{i}. Here we further divide into subcases.

If z is x (or a constant c, or a degree d in S, as the arguments for them are essentially the same), we need to show that d_{i}^{∗} is incomparable with y. First, y is not above d_{i}^{∗} because g_{i} is not below y; ⋁_{z≤d_{i},z∈S∪R} z^{∗} is not above y by property (∗) (since their originals do not join to some degree above x), and so by Lemma 3.2 joining it with some mutually 1-generic degrees does not make d_{i}^{∗} above y.

If z is some other d_{j} among d_{l+1}, …, d_{k}, then since d_{i} and d_{j} are incomparable, g_{i} and g_{j} only appear in one join but not the other. By 1-genericity d_{i}^{∗} and d_{j}^{∗} are incomparable.

This gives the desired contradiction that y with witnesses d^{∗}’s satisfy the same formula ∃d_{0}∃d_{1} … ∃d_{n}φ(x, d_{0}, d_{1}, …, d_{n}) but y is hyperimmune-free [and so array recursive]. □

9. Remarks

9.1. Nondefinability in the language (≤). Shore [S, Proposition 7.6], following related results in [LS], showed that neither the Low_{2} nor non-Low_{2} degrees are definable by a Π_{2} formula in the language of order alone (without parameters). The only property needed of these classes for the proofs there is that one can embed every finite lattice as an initial segment in them. The rest of the proofs rely only on general algebraic facts about D and Kleene-Post type results about extension of embeddings. Thus we can use the same argument to get the same nondefinability result for any class of degrees that contains copies of all finite lattices as initial segments of D.

This argument works for HI, HIF, AR, Arith and non-Arith (by classical results on embedding initial segments, see [Le]). We do not know whether ANR is definable by a Π_{2} formula in the language with just order (with REA added in, it is definable as mentioned in the Introduction).

9.2. Nondefinability in the language (≤,′). Following the outline of the arguments in Sections 5, one can get similar Σ_{1}-nondefinability results for the language with jump from embedding theorems about jump partial orders. For example, it is known that every finite jump partial order ([HS]), or even finite jump upper-semi lattice ([M]), is embeddable in the Turing degrees. By modifying their constructions one can easily make one of the elements HI or ANR, and so we know that HIF and AR are not Σ_{1} definable in (≤,′). In addition, one can also make sure that the degrees constructed are either all arithmetic or all nonarithmetic. This shows that Arith is not definable by Σ_{1} or Π_{1} formulae in (≤,′) (while there is a Π_{2} definition again as mentioned in the Introduction).

9.3. Open Questions. First of all, at the Σ_{1} level, there is one obvious remaining open question: Is HI definable by Σ_{1} formula in (≤, REA)? We believe arguments similar to those in Section 5 may work (in particular. we would want to build a REA-PO and make a certain element HIF), but our first attempts seem have meet some obstacles.

Most of our analysis applies to the language with REA but not RE. It is an interesting question whether similar results can be obtained for RE. If so, they seem likely to require priority type arguments rather than (or in addition to) forcing arguments. In another direction, we can also try to find possible definitions of RE in the language augmented by REA, which might be easier than the language with order alone.

Of course, many other degree classes can be analyzed for definability and nondefinability results.

References

[CS] M. Cai and R. A. Shore, Domination, forcing, array nonrecursiveness and relative recursive enumerability, Journal of Symbolic Logic, Volume 77, 2012, Pages 33–48.

[C1] M. Cai, A hyperimmune minimal degree and an ANR 2-minimal degree, Notre Dame Journal of Formal Logic, Vol. 51, Number 4, 2010, Pages 443–455.

[C2] M. Cai, Array nonrecursiveness and relative recursive enumerability, Journal of Symbolic Logic, Volume 77, 2012, Pages 21–32.

[DJS] R. Downey, C. Jockusch and M. Stob, Array nonrecursive degrees and genericity, London Mathematical Society Lecture Notes Series 224, 1996, University Press, Pages 93–105.

[F] R. M. Friedberg, A criterion for completeness of degrees of unsolvability, Journal of Symbolic Logic, Vol. 22, 1957, pages 159–160.

[HS] P. G. Hinman and T.A. Slaman, Jump embeddings in the Turing degrees, Journal of Symbolic Logic, vol. 56 (1991), pages 563–591.

[J1] C. Jockusch, The Degrees of Hyperhyperimmune Sets, The Journal of Symbolic Logic, Volume 34, Issue 3 (1969), pages 489–493.

[J2] C. G. Jockusch, Degrees of generic sets, in Recursion Theory: its Generalisations and Applications, F. R. Drake and S. S. Wainer (editors), Cambridge University Press, 1980, pages 110–139.

[JS] C. G. Jockusch, Jr. and R. A. Shore, Pseudo-jump operators II: transfinite iterations, hierarchies and minimal covers, Journal of Symbolic Logic, Vol. 49, 1984, pages 1205–1236.

[Le] M. Lerman, Degrees of Unsolvability: Local and Global Theory, Perspectives in Mathematical Logic, Volume 11, Springer-Verlag, 1983.

[LS] M. Lerman and R. A. Shore, Decidability and invariant classes for degree structures, Transactions of the American Mathematical Society, 310 (1988), pages 669–692.

[L] A. E. M. Lewis, Π_{1}^{0} classes, strong minimal covers and hyperimmune-free degrees, Bulletin of the London Mathematical Society, volume 39, number 6, 2007, pages 892–910.

[MM] W. Miller and D. A. Martin, The Degrees of Hyperimmune Sets, Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, vol. 14 (1968), pages 159–166.

[M] A. Montalbán Embedding Jump Upper Semilattices into the Turing Degrees, Journal of Symbolic Logic , Vol. 68, No. 3 (2003), pages 989–1014

[Sc] B. Schaeffer, Dynamic notions of genericity and array noncomputability, Annals of Pure and Applied Logic, Volume 95, 1998, pages 37–69.

[So] R. I. Soare, Recursively enumerable sets and degrees, Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1987.

[S] R. A. Shore, Direct and local definitions of the Turing jump, Journal of Mathematical Logic, Vol. 7, 2007, pages 229–262.

[S2] R. A. Shore, Minimal degrees which are Σ_{2}^{0} but not Δ_{2}^{0}, Proc. American Mathematical Society, 132 (2004), pages 563–565.

[SS] R. A. Shore and T. A. Slaman, Defining the Turing jump, Mathematical Research Letters, Vol. 6, 1999, pages 711–722.

[SW] T. A. Slaman, Global properties of the Turing degrees and the Turing jump, in Computational prospects of infinity, Part I, Tutorials, Lect. Notes Ser. Inst. Math. Sci. Natl. Univ. Singapore, 2008, World Sci. Publ., Hackensack, NJ, pages 83–101.

[Sp] C. Spector, On Degrees of Recursive Unsolvability, Annals of Mathematics, Vol 64, No. 3, 1956, pages 581–592.

Department of Mathematics, University of Wisconsin, Madison WI 53705

E-mail address: mcai@math.wisc.edu

Department of Mathematics, Cornell University, Ithaca NY 14853

E-mail address: shore@math.cornell.edu