The ∀∃ theory of D(≤, ∨,′) is undecidable

Richard A. Shore^{∗} Department of Mathematics

Cornell University Ithaca NY 14853

Theodore A. Slaman^{†} Department of Mathematics University of California, Berkeley Berkeley CA 94720

November 30, 2003

Abstract

We prove that the two quantifier theory of the Turing degrees with order, join and jump is undecidable.

1 Introduction

Our interest here is in the structure D of all the Turing degrees but much of the motivation and setting is shared by work on other degree structures as well. In particular, Miller, Nies and Shore [2004] provides an undecidability result for the r.e. degrees R at the two quantifier level with added function symbols as we do here for D. To set the stage, we begin then with an adaptation of the introduction from that paper including statements of some of its results and so discuss R, the r.e. degrees and D(≤ 0′), the degrees below 0′ as well.

A major theme in the study of degree structures of all types has been the question of the decidability or undecidability of their theories. This is a natural and fundamental question that is an important goal in the analysis of these structures. It also serves as a guide and organizational principle for the development of construction techniques and algebraic information about the structures. A decision procedure implies (and requires) a full understanding and control of the first order properties of a structure. Undecidability results typically require and imply some measure of complexity and coding in the structure. Once a structure has been proven undecidable, it is natural to try to determine both the extent and source of the complexity. On the one hand, one wants to determine the degree of the theory. On the other hand, one strives to find the dividing line between decidability and undecidability in terms of fragments of the theory. The first has frequently brought with it considerable information about second order properties such as definability and automorphisms. The second requires the most algebraic information and development of construction techniques.

∗Partially supported by NSF Grant DMS-0100035. Thanks also to Andre Nies for some helpful conversations about this work.

†Partially supported by NSF Grant DMS-9988644.

For D and D(≤ 0′) the results came fairly early. The first paper on the structure D of the Turing degrees as a whole, Kleene-Post [1954], developed the finite extension method (essentially Cohen forcing for one quantifier formulas of arithmetic) and proved that all finite partial orderings can be embedded in both D and D(≤ 0′). As these structures are partial orderings, this suffices to show that the one quantifier (∃) theories are decidable. (An existential sentence is true in either structure if and only if it is consistent with the theory of partial orders, or equivalently, if there is a partial order with a domain of size the number of variables in the formula which satisfies the formula.)

Once the embedding problem is settled, the next level of algebraic questions about the structures concern extension of embeddings. The first example here is density (or, from the other side minimal covers). A long development of construction techniques building on Spector’s original construction [1956] of a minimal degree essentially by forcing with recursive trees lead to Lachlan’s [1968] result that every countable distributive lattice is isomorphic to an initial segment of D. This coding of distributive lattices is sufficient to get the undecidability of the theory as Lachlan [1968] notes. Combining these initial segment techniques with simultaneous control of the join and Spector’s [1956] exact pair theorem, Simpson [1977] showed that the theory of D is recursively isomorphic to T h^{2}(ℕ), true second order arithmetic.

Finding the dividing line between decidability and undecidability required Lerman’s [1971] result that every finite lattice (not just the distributive ones) is isomorphic to an initial segment of D. On one hand, combining this with the finite extension method solved the extension of embedding problem in such a way that it gave the decidability of the two quantifier (∀∃) theory of D (Shore [1978] and Lerman [see 1983, Appendix A]). (By the extension of embedding problem we mean determining for which partial orders X ⊆ Y does every embedding of X into D have an extension to one of Y.) The ability to code all finite lattices also sufficed for Schmerl (see Lerman [1983, Appendix A]) to prove that the three quantifier (∀∃∀) theory of D is undecidable.

A similar analysis of D(≤ 0′) was then carried out. First came a significant elaboration of the construction techniques to get enough initial segments results below 0′ to give undecidability (Epstein [1979] and Lerman). Lerman then proved the full analog that every finite (even recursive) lattice is isomorphic to an initial segment of D(≤ 0′) (Lerman [1983, XII]). This immediately gives the undecidability of the three quantifier theory. Then these results were extended and combined with extension of embedding results below an arbitrary r.e. degree (Lerman and Shore [1988]) to get the decidability of the two quantifier theory. They were also used to show (Shore [1981]) that the theory of D(≤ 0′) is recursively isomorphic to true first order arithmetic.

The road has been much longer for the analysis of the r.e. degrees, R. It began with the finite injury (or 0′) priority method of Friedberg [1957] and Muchnik [1956] that produced incomparable r.e. degrees and so an embedding of the simplest partial (nonlinear) order. This method sufficed to embed all finite (even countable) partial orderings (Sacks [1963]) and so decide the one quantifier theory of R in the same way that Kleene and Post’s work decided that of D and D(≤ 0′). As the r.e. degrees are dense (by the infinite injury (or 0′′) methods of Sacks [1964]), the next steps in the analysis could not follow the path laid out for D. Many years of development of construction techniques and algebraic information ensued. Lachlan’s monster (or 0′′′ injury) methods were eventually used by Harrington and Shelah [1982] to prove that R is undecidable. The degree of its theory, as by now one should expect, is also that of true first order arithmetic (Harrington and Slaman; Slaman and Woodin; Nies, Shore and Slaman [1998]).

This leaves us with determining the boundary line between decidability and undecidability for R. Once again, a long hiatus and much work on other developments led to the undecidability of the three quantifier theory by Lempp, Nies and Slaman [1998]. The extension of embedding problem was solved by Slaman and Soare [2001] but the question of the decidability of the two quantifier theory of R remains open. A major obstacle is the lattice embedding problem of determining which finite lattices can be embedded in R. Despite some forty years of effort by many researchers on both embedding and nonembedding results, this question is still unsolved. The best result to date is Lerman [2000] which shows that the question for an important class of lattices is of degree at most 0′′. Even if the lattice embedding problem is shown to be decidable, there are further difficulties related to Lachlan’s [1966] nondiamond result that there is no embedding of the four element Boolean algebra into R that preserves both 0 and 1.

The situation for these three degree structures is summarized in the following table:

R  D  D(≤ 0′)
∃(≤)  Dec  Dec  Dec
∀∃(≤)  ?  Dec  Dec
∀∃∀(≤) Undec Undec Undec
T h(≤) T h(N) T h^{2}(N) T h(N)

Thus we remain a long way from the decidability of the two quantifier theory of R. On the other hand, the methods used to prove undecidability of other degree structures, interpretation of theories with simple fragments known to be undecidable, cannot work for the two quantifier theory of R with just ≤_{T}, or even any extension by relation symbols, since the most we can code into this fragment is the validity (perhaps in all finite models) of an ∀∃ sentence in a finite relational language but this problem is always decidable. (The point here is that, since the language is relational, any such sentence with n variables is satisfiable if and only if it is satisfiable in some structure of size at most n. As there are only finitely many such structures, this question is decidable. The basic result is classical (Bernays and Schönfikel [1928] and Ramsey [1930]). Its application to interpretations in structures such as R is pointed out in Shore [1999, p. 179].)

The only hope for an undecidability result at the two quantifier level for R then is to add function symbols. One would then try to interpret some theory with function symbols or, more directly, to code register machines. (The coding of register machines is at the basis of much of the work on undecidability of various severely restricted quantification classes of formulas as in Börger, Grädel and Gurevich [1997].) This raises the natural question about the boundary between decidability and undecidability for all these degree structures: What happens when we add additional function symbols to the language?

In all these settings the most natural one to be considered is the join operator ∨. As the structures remain uniformly locally finite the arguments for the unlikeliness of interpretations of theories providing undecidability remain in place. (The closure of any finite set is finite with size bounded by a fixed recursive function of the cardinality of the starting set and so cannot, on its own, be used to generate the infinite (or at least unbounded) structures need for coding even register machines.) Indeed, for all the degrees, the ∀∃ theory of this structure, D(≤, ∨), is decidable by Jockusch and Slaman [1993].

The next thing to try in terms of the known structural work on R is the infimum operator ∧. This has the advantage that finitely generated substructures can be infinite (Lerman, Shore and Soare [1984]). The obvious problem with this approach is that not every pair of r.e. degrees has an infimum and so ∧ is not a total function on R as is required. We can, of course, consider total extensions of the partial infimum relation but would not want the undecidability to be an artifact of our (perhaps perverse) choice of extension. The solution of Miller, Nies and Shore is to prove undecidability in a sufficiently uniform way so that the proof is independent of the choice of extension.

Theorem 1.1 (Miller, Nies and Shore [2004]) For any total extension ∧ of the partial infimum relation on R, the two quantifier (∀∃) theory of R(≤, ∨, ∧) is undecidable.

They noted that the coding methods used for this result can be applied to both D and D(≤ 0′) along with known initial segment constructions to get similar results.

Corollary 1.2 (Miller, Nies and Shore [2004]) For any total extension ∧ of the partial infimum relation on D (D(≤ 0′)), the two quantifier (∀∃) theory of D (D(≤ 0′)) with ≤, ∨ and ∧ is undecidable.

In the setting of the degrees as a whole, however, there is a second natural operator to consider adding to our language, the jump operator. The jump is definable in D by Shore and Slaman [1999] but the definition involves coding models of arithmetic and discussing automorphisms. Its complexity is very high and so sheds no light on the boundary between decidability and undecidability in D(≤,′), the degrees with jump which is our topic here.

Decidability results to date on the theory with the jump operator include the following:

Theorem 1.3 (Jockusch and Soare, see Lerman [1983] III.4.21) The theory of D with just ′ (no ≤) is decidable.

Theorem 1.4 (Hinman and Slaman [1991]): The ∃-theory of D(≤,′) is decidable.

Theorem 1.5 (Montalban [2003]): The ∃-theory of D(≤, ∨,′) is decidable.

We show that Montalban’s decidability result is the best possible (actually, our result was proven first so he provided the proof of sharpness for our result) and so solve problem IV.7 (attributed to Jockusch) of Arslanov and Lempp [1999]:

Theorem 1.6 The ∀∃-theory of D(≤, ∨,′) is undecidable.

Our route to undecidability is via the coding of register machines as in Miller, Nies and Shore [2004]. We describe the machines and their coding in predicate logic in the next section. Once we see how they are interpreted in predicate logic it will be clear that our undecidability result would follow immediately from the existence of a Δ_{0} formula with x free and additional free variables such that, as the additional variables range over the degrees, the sets defined by the formula range over all countable subsets of D. This result is provided by our main technical theorem.

Theorem 1.7 Given {y_{i}|i ∈ ω} and {z_{j}|j ∈ ω} disjoint countable sets of degrees, there are g and h such that ∀i, j ∈ ω ( (y_{i} ⊕ g)′ ≤_{T} (y_{i} ⊕ h)′ & (z_{j} ⊕ g)′ ≰_{T} (z_{j} ⊕ h)′).

Corollary 1.8 If C is any countable set of degrees then it is uniformly Δ_{0}-definable in parameters, i.e. there is a single formula which defines every such C as the parameters vary.

Proof. Choose any strict upper bound z for C. Let {y_{i}} = {x < z : x ∈ C} and {z_{j}} = {x < z : x ∉ C}. Apply the theorem to get the degrees g and h. C is then {x < z : (x ∨ g)′ ≤_{T} (x ∨ h)′} and so our desired formula is x < w & (x ∨ u)′ ≤_{T} (x ∨ v)′. □

We prove this theorem in §3. In the final section we summarize the state of affairs and point out some new problems suggested by our view of these matters.

2 Coding Register Machines

In this section we will explain the algebraic aspects of our codings and derive the main theorem, assuming these codings can be interpreted in R. The next section will provide the recursion theoretic arguments to show that the structures described here can be realized in the r.e. degrees. For completeness, we reprise (with some small simplification allowed by our construction here) the presentation of coding register machines in Miller, Nies and Shore [2004] beginning with a standard description of the k-register machines of Shepherdson and Sturgis [1963] and Minsky [1961] and their representation in predicate logic as in Nerode and Shore [1997, III.8] or Börger, Grädel and Gurevich [1997, 2.1].

A k-register machine consists of k many storage locations called registers. Each register contains a natural number. There are only two types of operations that these machines can perform in implementing a program. First, they can increase the content of any register by one and then proceed to the next instruction. Second, they can check if any given register contains the number 0 or not. If so, they go on to the next instruction. If not, they decrease the given register by one and can be told to proceed to any instruction in the program. Formally, we define register machine programs and their execution as follows:

A k-register machine program I is a finite sequence I_{1}, …, I_{t}, I_{t+1} of instructions operating on a sequence of numbers x_{1}, …, x_{k}, where each instruction I_{m}, for m ≤ t, is of one of the following two forms:

(i) x_{i} := x_{i} + 1 (replace x_{i} by x_{i} + 1)

(ii) If x_{i} ≠ 0, then x_{i} := x_{i} − 1 and go to j. (If x_{i} ≠ 0, replace it by x_{i} − 1 and proceed to instruction I_{j}.)

It is assumed that after executing some instruction I_{m}, the execution proceeds to I_{m+1}, the next instruction on the list, unless I_{m} directs otherwise. The execution of such a program proceeds in the obvious way on any input of values for x_{1}, …, x_{k} (the initial content of the registers) to change the values of the x_{i} and progress through the list of instructions. The final instruction, I_{t+1}, is always a halt instruction. Thus, if I_{t+1} is ever reached, the execution terminates with the current values of the x_{i}. In general, we denote the assertion that an execution of the program I is at instruction I_{m} with values n_{1}, …, n_{k} of the variables by I_{m}(n_{1}, …, n_{k}).

The standard translation of a register machine M describes the action of M by a system of universal axioms in the language of one unary function s thought of as the successor function on ℕ. For technical reasons peculiar to our later coding, we want to use distinct domains D_{i} with least elements 0_{i}. In our application here, these sets will be of the form {q_{i}^{(n)}|n ∈ ω} for arithmetically independent degrees q_{i}. The successor operators s_{i} will all be the jump operator. For now, we describe the axioms needed in predicate logic with additional k-ary relations P_{m} corresponding to the instructions I_{m}.

For each instruction I_{m}, 1 ≤ m ≤ t, include an axiom of the appropriate form:

(i) P_{m}(x_{1}, …, x_{k}) → P_{m+1}(x_{1}, …, x_{i−1}, s_{i}(x_{i}), x_{i+1}, …, x_{k}).

(ii) P_{m}(x_{1}, …, x_{i−1}, 0, x_{i+1}, …, x_{k}) → P_{m+1}(x_{1}, …, x_{i−1}, 0, x_{i+1}, …, x_{k}) ∧ P_{m}(x_{1}, …, x_{i−1}, s_{i}(y), x_{i+1}, … x_{k}) → P_{j}(x_{1}, …, x_{i−1}, y, x_{i+1}, …, x_{k}).

(Note that being a successor is equivalent to being nonzero, i.e. not equal to q_{i} which is the 0_{i} of D_{i}.)

Let P (I) be the finite set of universal axioms corresponding in this translation to register program I. It is easy to prove that, program I halts on input (n_{1}, …, n_{k}) if and only if the sentence F_{k}(n_{1}, …, n_{k}) ≡ P_{1}(s^{n_{1}}(0), … s^{n_{k}}(0)) → ∃x_{1}, …, ∃x_{k}[P_{t+1}(x_{1}, …, x_{k})] is a logical consequence of P (I). As it is a classical fact (Shepherdson and Sturgis [1963]; Minsky [1961]) that the halting problem for 2-register machine programs is r.e. complete, it suffices to code all such models with binary predicates to get undecidability.

As usual for interpretations, we now want to provide formulas Δ_{i}(q⃗, x), Π_{m}(q⃗, x, y) defining, for each choice of parameters q⃗, sets D_{i} (i = 1, 2) and binary relations P_{m} on D_{1} × D_{2} (1 ≤ m ≤ t + 1). (Remember s_{i} will be interpreted as the jump operator.) We take q_{1} and q_{2} to be the interpretations of 0 in D_{1} and D_{2} respectively. We now interpret our formulas P (I) → F (n_{1}, …, n_{k}) in the usual way. We relativize the quantifiers to the appropriate domain, i.e. ∃x_{i}(…) becomes ∃x_{i}(Δ_{i}(q⃗, x_{i}) ∧ …) and ∀x_{i}(…) becomes ∀x_{i}(Δ_{i}(q⃗, x_{i}) → …). We then replace occurrences of s_{i}(x_{i}) by x′_{i} and ones of P_{m}(x_{1}, x_{2}) by Π_{m}(q⃗, x_{1}, x_{2}). We indicate this translation by ∗. We also need a correctness condition Θ that says that q_{i} ∈ D_{i} and the jump is a function on the D_{i}: Δ_{1}(q⃗, q_{1}) ∧ Δ_{2}(q⃗, q_{2}) ∧ ∀x_{1}(Δ_{1}(q⃗, x_{1}) → Δ_{1}(q⃗, x′_{1}) ∧ ∀x_{2}(Δ_{2}(q⃗, x_{2}) → Δ_{2}(q⃗, x′_{2}). The class of sentences of R(≤ , ∨, ∧) that we want will then be those of the form ∀q⃗[Θ → (P (I)^{∗} → F_{2}^{∗})] where I ranges over programs for 2-register machines.

It is clear that to get these sentences to be ∀∃ ones it is sufficient to get quantifier free definitions (Δ_{i} and Π_{m}) of the domains and relations (and the worst that would work would be equivalent Σ_{1} and Π_{1} definitions). For the undecidability it suffices, of course, for the D_{i} to include ones isomorphic to {q_{i}^{(n)}} and the relations to include all binary relations on the D_{1} × D_{2} as the parameters vary. If we take q_{1} and q_{2} to be arithmetically independent, i.e. q_{i}^{(m)} ≤_{T} q_{1}^{(n_{1})} ∨ q_{2}^{(n_{2})} ⇔ m ≤ n_{i} then we can code any relation R_{m} ⊆ D_{1} × D_{2} in a Δ_{0} way from the D_{j} and one additional countable set of degrees T_{m} = {q_{1}^{(n_{1})} ∨ q_{2}^{(n_{2})} : ⟨n_{1}, n_{2}⟩ ∈ R_{m}} by R_{m}(x_{1}, x_{2}) ⇔ x_{1} ∈ D_{1} & x_{2} ∈ D_{2} & x_{1}^{(n_{1})} ∨ x_{2}^{(n_{2})} ∈ T_{m}.

So to prove our ∀∃ undecidability result for D(≤,′) it suffices to be able to define arbitrary countable subsets of D by a Δ_{0} formula in parameters. As we pointed out at the end of the introduction, Theorem 1.7 provides this Δ_{0} formula.

3 The Coding Theorem

We now prove our main technical result that says that by joining arbitrary given degrees with degrees g and h of our choosing we can make the jumps of the results be comparable or not as desired.

Theorem 1.7 Given {y_{i}|i ∈ ω} and {z_{j}|j ∈ ω} disjoint countable sets of degrees, there are g and h such that ∀i, j ∈ ω ( (y_{i} ⊕ g)′ ≤_{T} (y_{i} ⊕ h)′ & (z_{j} ⊕ g)′ ≰_{T} (z_{j} ⊕ h)′).

We fix representatives Y_{i} and Z_{j} (i, j ∈ ω) of the degrees y_{i} and z_{j}, respectively and construct sets G and H such that for every i, j ∈ ω the following requirements are satisfied:

• C_{i} : (Y_{i} ⊕ G)′ ≤_{T} (Y_{i} ⊕ H)′.

• D_{j} : (Z_{j} ⊕ G)′ ≰_{T} (Z_{j} ⊕ H)′.

Our construction will be a forcing argument. Our coding procedure for the C_{i} requirements relies on the fact that, for any A and B, A′ ∈ Π_{2}^{B} ⇒ A′ ≤_{T} B′ (Theorem 4.3 of Soare [1987, IV] relativized to B). Thus our plan for satisfying C_{i} is to make sure that, for almost every n, if (we force) n ∈ (Y_{i} ⊕ G)′ then we immediately force some canonically chosen Π_{2}^{0} fact (the h(n)^{th} one for some recursive h) about Y_{i} ⊕ H to be true. On the other hand, if (we force) n ∉ (Y_{i} ⊕ G) we want to immediately force this fact to be false. Thus h provides a one-one reduction from A′ to the complete Π_{2}^{B} set and so shows that A′ ∈ Π_{2}^{B}. We make a list of the corresponding subrequirements C_{i,n} where h is some specific recursive function that we will define later:

• C_{i,n} : n ∈ (Y_{i} ⊕ G)′ ⇔ h(n) ∉ (Y_{i} ⊕ H)′′.

To satisfy C_{i} we must satisfy C_{i,n} for almost every n.

Our diagonalization strategy to satisfy the requirements D_{j} is based on the fact that if A′ ≤_{T} B′ then Σ_{1}^{A} ∈ Δ_{2}^{B} and so Π_{2}^{A} ∈ Π_{2}^{B}. Thus there is a Δ_{0} formula θ such that if (Z_{j} ⊕ G)′ ≤_{T} (Z_{j} ⊕ H)′ then there is a recursive function f_{k} such that n ∉ (Z_{j} ⊕ G)′′ ⇔ ∀u∃vθ(f_{k}(n), u, v, Z_{j}, H). (Here we have listed all the recursive functions as f_{k}, k ∈ ω.) Our plan is then for each k (i.e. for each recursive function) to choose an n and, at some stage s of the construction, meet the following subrequirement:

• D_{j,k} : ∃n¬[n ∉ (Z_{j} ⊕ G)′′ ⇔ ∀u∃vθ(f_{k}(n), u, v, Z_{j}, H)].

We will accomplish this by arranging that either we force ∃u∀v¬θ(f_{k}(n), u, v, Z_{j}, H) at stage s while immediately forcing the Π_{2}^{Z_{j}⊕G} fact that n ∉ (Z_{j} ⊕ G)′′ to be true or, at stage s we force ∀u∃vθ(f_{k}(n), u, v, Z_{j}, H) while immediately making the Σ_{2}^{Z_{j}⊕G} fact n ∈ (Z_{j} ⊕G)′′ true. In either case we violate the biconditional equivalent to (Z_{j} ⊕G)′ ≤_{T} (Z_{j} ⊕ H) and meeting D_{j,k} for all k guarantees that (Z_{j} ⊕ G)′ ≰_{T} (Z_{j} ⊕ H) as required to satisfy D_{j}.

To give us immediate control (both positively and negatively) over a canonical list of Π_{2} facts, we employ a variation of Kumabe-Slaman forcing (See Shore and Slaman [1999]). That forcing builds a (not necessarily recursive) Turing functional Φ and allows one to immediately guarantee that, for any set X, Φ(X) is a finite function (a canonical Σ_{2}^{X⊕Φ} fact). We wish to extend this to allow such control over a recursive set of such facts and to also allow “immediate forcing” of their negations. The first goal is achieved by considering the action of Φ(X) on individual columns (of inputs) rather than all possible inputs. The second is met by adding on an additional second set of restraints on extensions that prevent the Σ_{2} fact of interest from ever being immediately forced (for any witness). General genericity arguments will then guarantee that once we have done this, the Π_{2} fact will immediately be forced.

We now supply the formal definitions of our forcing relation.

Definition 3.1 A Turing functional Φ is a set of sequences (x, y, σ) (the axioms) such that x is a natural number (the input), y is either 0 or 1 (the output), and σ is a finite binary sequence (the use). Furthermore, for all x, for all y_{1} and y_{2}, and for all compatible σ_{1} and σ_{2}, if (x, y_{1}, σ_{1}) ∈ Φ and (x, y_{2}, σ_{2}) ∈ Φ, then y_{1} = y_{2} and σ_{1} = σ_{2}. (This says that only one axiom in Φ applies to a particular oracle on any particular input. It is technically useful.)

We write Φ(x, σ) = y to indicate that there is an initial segment τ of σ, possibly equal to σ, such that (x, y, τ) ∈ Φ. If X ⊆ ω, we write Φ(x, X) = y to indicate that there is an ℓ such that Φ(x, X ↾ ℓ) = y, and write Φ(X) for the function evaluated in this way. (Note that the set of axioms need not be recursively enumerable so the functions computed are partial recursive in the functional Φ plus the input set X.)

Definition 3.2 Conditions p in our forcing notion P are triples ⟨Φ_{p}, X_{p}, W_{p}⟩ where Φ_{p} is a finite Turing functional and both X_{p} and W_{p} are finite collections of pairs ⟨X, n⟩ (or ⟨W, n⟩) consisting of one set and one natural number such that X_{p} ∩ W_{p} = ∅. We say that q extends p, q ≤ p, if

1. Φ_{p} ⊆ Φ_{q} &( [(x, y, σ) ∈ Φ_{p} & (x′, y′, σ′) ∈ Φ_{q} − Φ_{p}] → |σ| < |σ′|).

2. X_{p} ⊆ X_{q} & W_{p} ⊆ W_{q}.

3. (∀x, y, ⟨X, n⟩ ∈ X_{p})(Φ_{q}(⟨n, x⟩, X) = y → Φ_{p}(⟨n, x⟩, X) = y).

If K is a filter on P then Φ_{K} = ∪{Φ_{p}|p ∈ K} is a Turing functional. It is this functional that will be our generic object Φ and about which we will be able to speak in our forcing language. The second clause of (1) says that only longer axioms than the ones we already have can be added on by an extension. Clause (3) says that no new axioms can be added which apply to the oracle X on any input in column n.

One can now give a common definition (in the setting of forcing in arithmetic) of p ⊩ ψ for p ∈ P and ψ a sentence of arithmetic with bounded as well as unbounded quantifiers and an added unary relation symbol Φ (for the generic Turing functional) as well as ones Y_{i} and Z_{j} for our fixed choice of representatives of the degrees mentioned in Theorem 1.7.

Definition 3.3 We define p ⊩ ψ by induction on formulas where we view ∀x as an abbreviation for ¬∃x¬ and consider sentences with leading (unbounded) quantifiers (∃ and ∀) and negation symbols followed by a bounded formula.

1. If ψ is Δ_{0} (i.e. has only bounded quantifiers) then p ⊩ ψ if and only if ψ(Φ_{K}) is true for every filter K on P containing p. (Thus if ψ and ψ′ are logically equivalent Δ_{0} formulas then p ⊩ ψ ⇔ p ⊩ ψ′.)

2. p ⊩ ∃nψ(n) if and only if there is an n ∈ ω such that p ⊩ ψ(n).

3. p ⊩ ¬ψ if and only if no q ≤ p forces ψ.

We say that a filter K on P is 1-generic if for every Δ_{0} formula ψ(x) there is a p ∈ K such that either p ⊩ ∃xψ(x) or p ⊩ ¬∃xψ(x) (or equivalently, p ⊩ ∀x¬ψ(x)).

Clause (3) of Definition 3.2 is the key to making our canonical Π_{2} facts false as putting ⟨X, n⟩ into X_{p} immediately forces Φ(X) ↾ ω^{[n]} to be finite. The restriction that X_{p} ∩ W_{p} = ∅ means that once a pair ⟨W, n⟩ has gone into W_{p} then it can never go into X_{p} and so, if Φ is sufficiently generic (even 1-generic) Φ(W) will be total on ω^{[n]}. Thus we see that our canonical Π_{2}^{X⊕Φ} facts can be taken to be that Φ(X) is total on ω^{[n]}. Putting ⟨X, n⟩ into X_{p} will immediately force this sentence to be false while putting it into W_{p} will make it true as long as K is at least 1-generic. In the terminology of the subrequirements C_{i,n} this corresponds to choosing a recursive h such that h(n) ∉ (X ⊕ Φ)′′ ⇔ ∀x∃y(Φ(⟨n, x⟩, X) = y) for every Φ and X.

We now list some of the basic facts about this forcing relation. Key among them are that forcing for bounded sentences is recursive (in the set parameters) and that, if p belongs to a 1-generic filter K, p ⊩ Θ(Φ) where Θ is Σ_{2} or Π_{2} then Θ(Φ_{K}) holds. These facts allow us to control the forcing relation when needed and guarantee that forcing the sentences relevant to our requirements makes them true of the functionals associated with the 1-genreic filters that we construct.

Remark 3.4 If ψ is Δ_{0} and K is a filter on P then we have the following facts:

1. p ⊩ ∃uψ(u, Φ) ⇒ ∃q ≤ p∃u[(Φ_{q}, ∅, ∅) ⊩ ψ(u, Φ)] since some initial segment Φ_{q} of any Φ_{K} with p ∈ K suffices to guarantee the truth of the Δ_{0} sentence. Of course, if p ∈ K then ∃xψ(x, Φ_{K}) is true. Conversely, if ∃xψ(x, Φ_{K}) is true then ∃p ∈ P(p ⊩ ∃xψ(x, Φ) for the same reason and the fact that the definition of the forcing order guarantees that once a use σ is included in an axiom of Φ then no axioms (with codes) smaller than σ can ever be inserted.

2. (Φ_{q}, ∅, ∅) ⊩ ψ(u, Φ) is a uniformly recursive relation in q, u, ψ, Φ and the Y_{i} and Z_{j} appearing in ψ as the truth of ψ(u, Φ_{K}) depends only on initial segments of Φ_{K} (and the Y_{i} and Z_{j}). We abbreviate this relation as Φ_{q} ⊩ ψ(u, Φ).

3. If p ⊩ ∀uψ(u, Φ) then [(Φ_{p}, X_{p}, ∅) ⊩ ∀uψ(u, Φ)] as otherwise there would be a u ∈ ω and q ≤ (Φ_{p}, X_{p}, ∅) such that q ⊩ ¬ψ(u, Φ) and so a q′ ≤ q such that (Φ_{q′}, ∅, ∅) ⊩ ¬ψ(u, Φ) but then (Φ_{q′}, X_{p}, W_{p}) extends p but also forces ¬ψ(u, Φ) for a contradiction.

4. If p ⊩ ∀uψ(u, Φ) and p ∈ K then ∀uψ(u, Φ_{K}) as otherwise there would be a u such that ¬ψ(u, Φ_{K}) and so a q ∈ K such that q ⊩ ¬ψ(u, Φ) contradicting the compatibility required by p, q ∈ K and the definition of forcing. Conversely, if K is 1-generic and ∀uψ(u, Φ_{K}) then ∃p ∈ K(p ⊩ ∀uψ(u, Φ) as otherwise there would be a q ∈ K such that q ⊩ ∃u¬ψ(u, Φ) and so ∃u¬ψ(u, Φ_{K}) would hold for a contradiction.

5. If p ⊩ ∃x∀yψ(x, y, Φ) and p ∈ K then ∃x∀yψ(x, y, Φ_{K}) by the definition of forcing and (4). Similarly, if K is 1-generic, p ∈ K and p ⊩ ∀x∃yψ(x, y, Φ) then ∀x∃yψ(x, y, Φ_{K}) as otherwise there would be an x such that ¬∃yψ(x, y, Φ_{K}), and so (by 4) a q ∈ K such that q ⊩ ¬∃yψ(x, y, Φ). Again the compatibility of p and q gives us an r extending both for a contradiction (as r ≤ q, r ⊩ ∃x¬∃yψ(x, y, Φ) but as r ≤ p, this contradicts the assumption that p ⊩ ∀x∃yψ(x, y, Φ).

We will build G and H to be the Turing functionals corresponding to two 1-generic filters K and L for this forcing and to satisfy a specific list of other conditions by building two sequences p_{s}, q_{s} such that ∪Φ_{p_{s}} = Φ_{K} = G and ∪Φ_{q_{s}} = Φ_{L} = H. The requirements that we have to satisfy in addition to those for 1-genericity are ones to guarantee that C_{i} and D_{j} are true of G and H.

As described above, our plans with our now known list of canonical Π_{2} facts are as follows. To satisfy C_{i} we make sure that, for almost every n, if n ∈ (Y_{i} ⊕ G)′ then we put ⟨Y_{i}, n⟩ into W_{q_{m}} for some m while if n ∉ (Y_{i} ⊕ G)′ we put it into X_{q_{m}} for some m. In the first case, this makes h(n) ∉ (Y_{i} ⊕ H)′′, indeed dom Φ_{L}(Y_{i}) ↾ ω^{[n]} = ω^{[n]} for any 1-generic L containing q. In the second case, this makes dom Φ_{L}(Y_{i}) ↾ ω^{[n]} finite and so h(n) ∈ (Y_{i} ⊕ H)′′. Thus, if for almost all n we meet the requirements C_{i,n}, then (Y_{i} ⊕ G)′ ∈ Π_{2}^{Y_{i}⊕H} and (Y_{i} ⊕ G)′ ≤_{T} (Y_{i} ⊕ H)′ as required.

To satisfy D_{j}, our plan is, for each k, to choose an n such that n ∉ (Z_{j} ⊕ G)′′ ⇔ (G(Z_{j}) ↾ ω^{[n]} is total) and, at some stage s of the construction, meet the subrequirement D_{j,k} that ¬[n ∉ (Z_{j} ⊕ G)′′ ⇔ ∀u∃vθ(f_{k}(n), u, v, Z_{j}, H)], i.e. ¬[G(Z_{j}) ↾ ω^{[n]} is total ⇔ ∀u∃vθ(f_{k}(n), u, v, Z_{j}, H)] by arranging that either q_{s} ⊩ ∃u∀v¬θ(f_{k}(n), u, v, Z_{j}, Φ) while ⟨Z_{j}, n⟩ ∈ W_{p_{s}} which guarantees that G(Z_{j}) ↾ ω^{[n]} is total; or q_{s} ⊩ ∀u∃vθ(f_{k}(n), u, v, Z_{j}, Φ) while ⟨Z_{j}, n⟩ ∈ X_{p_{s}} which guarantees that G(Z_{j}) ↾ ω^{[n]} is finite. In either case we violate the biconditional equivalent to (Z_{j} ⊕ G)′ ≤_{T} (Z_{j} ⊕ H)′. Meeting D_{j,k} for all k guarantees that (Z_{j} ⊕ G)′ ≰_{T} (Z_{j} ⊕ H) as required. We now give the details of the construction.

Construction: We make an ω-list of the subrequirements C_{i,n}, D_{j,k} described above as well as others P_{m} to decide the one quantifier sentences ∃wψ_{m} about G and H. We begin at stage 0 with the empty conditions p_{0} = q_{0} = ⟨∅, ∅, ∅⟩. Suppose we are at stage s + 1 with p_{s}, q_{s} defined. We let t_{i} be the least s at which Y_{i} is mentioned in one of the conditions, i.e. ⟨Y_{i}, m⟩ ∈ X_{p_{s}} ∪ W_{p_{s}} ∪ X_{q_{s}} ∪ W_{q_{s}} for some m. Our action depends on the requirement assigned to s, i.e. the s^{th} one on our list.

P_{m} : If there is a finite Φ′ ⊇ Φ_{p_{s}} (consistent with p_{s}, i.e. (Φ′, X_{p_{s}}, W_{p_{s}}) ≤ p_{s}) and a w such that ⟨Φ′, X_{p_{s}}, W_{p_{s}}⟩ ⊩ ψ_{m}(w, Φ) then we choose one and set p_{s+1} = ⟨Φ′, X_{p_{s}}, W_{p_{s}}⟩. If not we let p_{s+1} = p_{s}. We then do the same for H to define q_{s+1} from q_{s}.

C_{i,n} : If ⟨Y_{i}, n⟩ is already on either list in q_{s} let p_{s+1} = p_{s} and q_{s+1} = q_{s}. Otherwise, ask if there is a finite Φ′ ⊇ Φ_{p_{s}} (consistent with p_{s}) such that ⟨Φ′, X_{p_{s}}, W_{p_{s}}⟩ ⊩ n ∈ (Y_{i} ⊕ Φ)′. If so, choose one and let p_{s+1} = ⟨Φ′, X_{p_{s}}, W_{p_{s}}⟩ and q_{s+1} = ⟨q_{s}, X_{q_{s}}, W_{q_{s}} ∪ {⟨Y_{i}, n⟩}⟩. If not, let p_{s+1} = p_{s} and q_{s+1} = ⟨Φ_{q_{s}}, X_{q_{s}} ∪ {⟨Y_{i}, n⟩}, W_{q_{s}}⟩.

D_{j,k} : Choose an n such that ⟨Z_{j}, n⟩ does not appear on either list in p_{s}. Ask if there is a u and q′ ≤ q_{s} (which by Remark 3.4 can be to assumed to have W_{q′} = W_{q_{s}}) such that q′ ⊩ ∀v¬θ(f_{k}(n), u, v, Z_{j}, Φ) and a p′ ≤ p_{s} (which again by Remark 3.4 can be assumed to have W_{p′} = W_{p_{s}}) so that for any m and any t_{i} ≤ s such that Y_{i} ≤_{T} Z_{j} and ⟨Y_{i}, m⟩ ∈ X_{q′} −X_{q_{t_{i}}} we have that p′ ⊩ m ∉ (Y_{i} ⊕ Φ)′.

If not (Π_{2} outcome), then we let p_{s+1} = ⟨Φ_{p_{s}}, X_{p_{s}} ∪ {⟨Z_{j}, n⟩}, W_{p_{s}}⟩ and q_{s+1} = q_{s}. If there are such u, q′ and p′ (Σ_{2} outcome) then we claim (and will verify in Lemma

3.8 below) that we can choose such a q′ with no ⟨Y_{i}, l⟩ ∈ X_{q′} − X_{q_{s}} with Y_{i} ≰_{T} Z_{j} and a p′ for which ⟨Z_{j}, n⟩ ∉ X_{p′}. We choose such and set p_{s+1} = ⟨Φ_{p′}, X_{p′}, W_{p′} ∪ {⟨Z_{j}, n⟩}⟩ and q_{s+1} = q′.

Verifications: It is clear that there are no difficulties carrying out these instructions when the requirement being considered is P_{m} or C_{i,n}. Moreover, it is also clear that, in the case of P_{m}, we have guaranteed that the Σ_{1} formula is forced at s + 1 if possible and otherwise no extension forces it. Thus K and L are 1-generic. Similarly, in the case of C_{i,n}, as long as from some stage t onward no actions other than for C_{i,m} put any ⟨Y_{i}, m⟩ on any list in q_{s} without our forcing the corresponding outcome for m ∈ (Y_{i} ⊕G)′, then we satisfy C_{i}. In fact, our actions guarantee a bit more. If ⟨Y_{i}, m⟩ is put into X_{q_{s}} at s ≥ t_{i} (by C_{i,m} or some D_{j,k} acting for its Σ_{2} outcome as described above) then p_{s+1} ⊩ m ∉ (Y_{i} ⊕ Φ)′ as required; and no action other than for C_{i,m} can put ⟨Y_{i}, m⟩ into W_{q_{s}} for s ≥ t_{i}. Thus we are left with analyzing the way we decide the Π_{2} questions for D_{j,k} at s_{j,k}.

The simpler case is the Π_{2} outcome. Here we only have to show that, for each u, when we consider the requirement P_{m} for the formula ∃vθ(f_{k}(n), u, v, Z_{j}, Φ) for H at s > s_{j,k} that we force the Σ_{1} outcome. If not, then by our construction, q_{s} ⊩ ∀v¬θ(f_{k}(n), u, v, Z_{j}, Φ) and q_{s} ≤ q_{s_{j,k}}. We now claim that if ⟨Y_{i}, m⟩ ∈ X_{q_{s}} − X_{q_{t_{i}}} then p_{s} ⊩ m ∉ (Y_{i} ⊕ Φ)′ which would put us in the Σ_{2} outcome for a contradiction. To verify the claim consider how ⟨Y_{i}, m⟩ could have entered X_{q_{s}}. No action for P_{m} adds anything to either list. Action for C_{h,l} adds at most ⟨Y_{h}, l⟩ to the X list but only when it already forces l ∉ (Y_{h} ⊕ Φ)′ (for G) as required. Finally, by the claim in the Σ_{2} case of the construction (Lemma 3.8 below) action for some D_{h,l} at a stage t after t_{i} (and before s) puts ⟨Y_{i}, m⟩ into X_{q_{s}} only when it also makes p_{t+1} ⊩ m ∉ (Y_{i} ⊕ Φ)′ as required.

The Σ_{2} case requires a deeper analysis of the forcing relation along the lines of Shore and Slaman [1999] albeit somewhat more elaborate combinatorially. The idea here (as in Shore and Slaman [1999]) is that if there is a q′ ≤ q such that q′ ⊩ ∀v¬θ(f_{k}(n), u, v, Z_{j}, Φ) then, first, it can be taken to be of the form (Φ′, X′, W_{q}). Next, by the basic properties of forcing, no extension q′′ = (Φ′′, X′′, W_{q}) of q′ forces ∃vθ(f_{k}(n), u, v, Z_{j}, Φ) so, if for some m, some Φ′′ ⊇ Φ′ makes θ(f_{k}(n), u, m, Z_{j}, H) true then it must be incompatible with the conditions imposed by X′, i.e. some axiom in Φ′′ − Φ′ with input in column e applies to an X_{i} with ⟨X_{i}, e⟩ ∈ X′. We can form a tree of approximations to such an X′ by considering those sequences ⟨σ_{l}, s_{l}⟩ such that any such Φ′′ has an axiom compatible with one of the ⟨σ_{l}, s_{l}⟩. Now we must also associate with any such q′ a condition p′ ≤ p that forces m ∉ (Y_{i} ⊕ Φ)′ for the i and m that we worry about in the definition of the Σ_{2} outcome. This adds one more layer of approximations to produce p′ from a path in the appropriate tree along with q′. We are thus led to the following definitions.

Definition 3.5 Suppose we are given conditions p and q and an instance of one of our formulas ∀v¬θ(a, u, v, Z, Φ) where we are thinking about H as the interpretation of Φ and have written a for f_{k}(n) and Z for Z_{j}. We say that i is crucial (for p and q) if Y_{i} ≤_{T} Z and Y_{i} is on some list in p or q. Let t be larger than all numbers mentioned in p or q (either in one of the lists or one of the Turing functionals) and such that U ↾ t ≠ V ↾ t for any sets U ≠ V appearing on any list in p or q. For each m ≥ t and finite Turing functionals Γ and Θ such that ⟨Γ, X_{p}, W_{p}⟩ ≤ p and ⟨Θ, X_{q}, W_{q}⟩ ≤ q we define the tree T_{m}(Γ, Θ, p, q) = T whose nodes are sequences ⟨⟨σ_{l}, s_{l}⟩, τ⃗_{l}⟩_{l≤m} (coded as numbers in some fixed way as are all finite sets and sequences) where each τ⃗_{l} is itself a sequence ⟨τ_{l,e}, t_{l,e}⟩_{e≤m} with the following properties:

1. |σ_{l}|, |τ_{l,e}| ≥ m and all of these lengths are the same; ⟨W, s_{l}⟩ ∈ W_{q} ⇒ σ_{l} ↾ m ⊈ W ↾ m; ⟨W, t_{l,e}⟩ ∈ W_{p} ⇒ τ_{l,e} ↾ m ⊈ W ↾ m.

2. If Θ′ ⊇ Θ with the code for Θ′ less than the one for the node and Θ′ ⊩ θ(a, u, v, Z, Φ) for some v also less than the code for the node, then Θ′ − Θ contains an axiom (⟨s, z⟩, y, σ) such that, for some l ≤ m, s = s_{l} and σ is compatible with σ_{l}.

3. If σ_{l} ⊆ Y_{i} for some crucial i, Γ′ ⊇ Γ with the code for Γ′ less than the one for the node and Γ′ ⊩ s_{l} ∈ (Y_{i} ⊕ Φ)′ with a witness for convergence also less than the code for the node then Γ′ − Γ contains an axiom (⟨t, z⟩, y, τ) such that, for some e ≤ m, t = t_{l,e} and τ is compatible with τ_{l,e}.

We order the nodes of T in the expected way: ⟨⟨σ′_{l}, s′_{l}⟩, τ′_{l}⟩ ⪯_{T} ⟨⟨σ_{l}, s_{l}⟩, τ⃗_{l}⟩ ⇔ (∀l ≤ m)(σ′_{l} ⊆ σ_{l} & s_{l} = s′_{l} & (∀e ≤ m)(τ′_{l,e} ⊆ τ_{l,e} & t_{l,e} = t′_{l,e})).

Lemma 3.6 T is a finitely branching tree recursive in Z.

Proof. T is obviously finitely branching since the σ_{l} and τ_{l,e} are binary sequences. As m is fixed the information needed in (1) is finite so it is a recursive condition. Since forcing a Δ_{0} formula is recursive (in the set parameters), (2) is recursive in Z. The list of Y_{i} mentioned in p or q and recursive in Z is finite and Z can tell if σ_{l} is an initial segment of one of these Y_{i} while the rest of the condition is recursive given our bound on the witness for convergence in s_{l} ∈ (Y_{i} ⊕ Φ)′. □

Lemma 3.7 If there are q′ = (Θ, X_{q′}, W_{q}) and p′ = (Γ, X_{p′}, W_{p}) as required in the definition of the Σ_{2} outcome for D_{j,k} then for for some (large enough) m, T_{m}(Γ, Θ, p, q) = T has an infinite path.

Proof. We claim that if X_{q′} = {⟨S_{l}, s_{l}⟩|l ≤ m} and X_{p′} = {⟨T_{e}, t_{e}⟩|e ≤ m} (we allow duplications to keep the indexing the same and m ≥ t) then {⟨⟨S_{l} ↾ n, s_{l}⟩_{l≤m}, τ⃗_{l,n}⟩|n > m} is a path in T where τ⃗_{l,n} = ⟨T_{e} ↾ n, t_{e}⟩_{e≤m}. Here we have chosen m larger than t and the cardinalities of X_{q′} and X_{p′} as well as to insure that if U ≠ V are mentioned in p′ or q′ then U ↾ m ≠ V ↾ m. Note that if ⟨X, n⟩ ∈ X_{q′} − X_{q} and ⟨W, n⟩ ∈ W_{q} then X ≠ W by the definition of the forcing ordering and so X ↾ m ≠ W ↾ m and similarly for p. To see that these nodes are on T check that each condition is satisfied for ⟨⟨S_{l} ↾ n, s_{l}⟩_{l≤m}, τ⃗_{l,n}⟩:

1. The lengths are all larger than m by definition. The restrictions associated with W_{q} and W_{p} are satisfied by our choice of m and the note above.

2. If Θ′ ⊇ Θ and Θ′ ⊩ θ(a, u, v, Z, Φ) for some v then Θ′ is not consistent with q′ and so Θ′ − Θ must contain an axiom (⟨s, z⟩, y, σ) such that there is an l ≤ m such that s_{l} = s and σ ⊆ S_{l}. Clearly this σ is compatible with S_{l} ↾ n.

3. If S_{l} ↾ n ⊆ Y_{i} and i is crucial (and so, in particular, S_{l} = Y_{i} by our choice of m), Y_{i} ≤_{T} Z, Γ′ ⊇ Γ and Γ′ ⊩ s_{l} ∈ (Y_{i} ⊕ Φ)′ then Γ′ is not consistent with p′ since by our requirements when we acted for D_{j,k}, p′ ⊩ s_{l} ∉ (S_{l} ⊕ Φ)′ and so Γ′ − Γ must contain an axiom (⟨t, z⟩, y, τ) such that there is an e ≤ m such that t = t_{e} and τ ⊆ T_{e}. Clearly this τ is compatible with T_{e} ↾ n. □

Lemma 3.8 If there is an infinite path P = {⟨⟨σ_{n,l}, s_{l}⟩, τ⃗_{n,l}⟩⟩_{l≤m}|n ∈ ω} in some T_{m}(Γ, Θ, p, q) = T then there are q′ and p′ as required by the claim in the implementation of the Σ_{2} outcome for D_{j,k}.

Proof. Any infinite path clearly produces sets S_{l} = ∪{σ_{n,l}|n ∈ ω} for l ≤ m and R_{l,e} = ∪{τ_{n,l,e}|n ∈ ω} for e ≤ m if S_{l} = Y_{i} some crucial i. As T is recursive in Z and has an infinite path we can choose one that does not compute any Y_{i} ≰_{T} Z by Jockusch and Soare [1972] and so we may assume that no S_{l} = Y_{i} for any crucial i. We let q′ = (Θ, X_{q} ∪ {⟨S_{l}, s_{l}⟩|l ≤ m}, W_{q}) which is clearly a condition since no ⟨S_{l}, s_{l}⟩ ∈ W_{q} by clause (1) of the definition of T. We first argue that q′ ⊩ ∀v¬θ(a, u, v, Z, H). If not, then by Remark 3.4, there would be a (Θ′, X_{q′}, W_{q′}) ≤ q′ and a v such that Θ′ ⊩ θ(a, u, v, Z, Φ). By clause (2) of the definition of T there would then be an axiom (⟨s, z⟩, y, σ) ∈ Θ′ − Θ and an l ≤ m such that s = s_{l} and σ is compatible with σ_{n,l} ⊆ S_{l} for infinitely many n and so σ ⊆ S_{l}. As this contradicts the definition of (Θ′, X_{q′}, W_{q′}) ≤ q′, we have that q′ ⊩ ∀v¬θ(a, u, v, Z, Φ) and there is no ⟨Y_{i}, h⟩ ∈ X_{q′} − X_{q} with Y_{i} ≤_{T} Z as required.

We next argue that p̄ = (Γ, X_{p} ∪ {R_{l,e}|S_{l} = Y_{i} some crucial i and e ≤ m}, W_{p}) ⊩ s_{l} ∉ (S_{l} ⊕ Φ)′ for every ⟨S_{l}, s_{l}⟩ ∈ X_{q′} − X_{q_{t_{i}}} with S_{l} = Y_{i} for some crucial i. Suppose S_{l} = Y_{i} for some crucial i but p̄ ⊮ s_{l} ∉ (S_{l} ⊕ Φ)′. In this case, there is a Γ′ ⊇ Γ consistent with p̄ such that Γ′ ⊩ s_{l} ∈ (S_{l} ⊕ Φ)′. By clause (3) of the definition of T, there must be a (⟨t, z⟩, y, τ) ∈ Γ′ − Γ such that, for some e ≤ m, t = t_{l,e} and τ is compatible with τ_{n,l,e} for infinitely many n. Thus τ ⊆ R_{l,e} ∈ Xp̄ and so Γ′ is not consistent with p̄ for the desired contradiction.

Finally, we argue that we can find a p′ ≤ p such that ⟨Z, n⟩ ∉ X_{p′} and p′ ⊩ s_{l} ∉ (S_{l} ⊕ Φ)′ for all the l’s for which S_{l} = Y_{i} for a crucial i and ⟨S_{l}, s_{l}⟩ ∉ X_{q_{t_{i}}} which will complete the proof. For each such l we consider the tree T_{m,l} whose nodes are sequences ⟨τ_{e}, t_{e}⟩_{e≤m} such that (∀e, e′ ≤ m)(|τ_{e}| = |τ_{e′}| > m & (⟨W, t_{e}⟩ ∈ W_{p} → τ_{e} ↾ m ≠ W ↾ m)) and (∀Γ′ ⊇ Γ) (if the code for Γ′ is less than the one for τ⃗ and Γ′ ⊩ s_{l} ∈ (Y_{i} ⊕ Φ)′ with a witness for convergence also less than the code for τ⃗ then Γ′ − Γ contains an axiom (⟨t, z⟩, y, τ) such that, for some e ≤ m, t = t_{e} and τ is compatible with τ_{e}). We order T_{m.l} by ⟨τ′_{e}, t′_{e}⟩_{e≤m} ⪯_{T_{m,l}} ⟨τ_{e}, t_{e}⟩_{e≤m} ⇔ (∀e ≤ m)(t′_{e} = t_{e} & τ′_{e} ⊆ τ_{e}).

This tree is finitely branching and recursive in Y_{i}. Our original sequence ⟨τ⃗_{n,l}|n ∈ ω⟩ is a path in T_{m,l} and so there is one that does not compute Z ≰_{T} Y_{i}. (Note here that as i is crucial Y_{i} ≤_{T} Z but by the assumption of the Theorem they have different degree.) Let ⟨τ′_{n,l}|n ∈ ω⟩ be such a path for each l as required and let R′_{l,e} = ∪{τ′_{n,l,e}|n ∈ ω}. As before we know that p_{l} = (Γ, X_{p} ∪ {⟨R_{l,e}, t′_{l,e}⟩|e ≤ m}, W_{p}) ⊩ s_{l} ∉ (S_{l} ⊕ Φ)′ while no R′_{l,e} is Z. We can now get the required p′ as (Γ, X_{p} ∪{⟨R′_{l,e}, t′_{l,e}⟩|S_{l} = Y_{i} for some crucial i and ⟨S_{l}, s_{l}⟩ ∉ X_{q_{t_{i}}} & e ≤ m}, W_{p}). As p′ extends every p_{l} for l on our list, p′ ⊩ s_{l} ∉ (S_{l} ⊕ Φ)′ for all these l’s while ⟨Z, n⟩ ∉ X_{p} by our choice of n and no R_{l,e} = Z, p′ is as required to implement the Σ_{2} outcome for D_{j,k}. □

4 Conclusions and Questions

We summarize much of the current state of affairs about the dividing line between decidability and undecidability in the structures R, D and D(≤ 0′) in various languages in the following tables.

R  D D(≤ 0′)
∃(≤, ∨)  Dec  Dec  Dec
∀∃(≤, ∨)  ?  Dec  ?
∀∃∀(≤, ∨) Undec Undec Undec
R  D D(≤ 0′)
∃(≤, ∨, ∧) ? Dec Dec
∀∃(≤, ∨, ∧) Undec Undec Undec
D
∃(≤, ∨,′) Dec
∀∃(≤, ∨,′) Undec

The first and third tables are straightforward. The second requires some explanation of the use of ∧. We understand decidability in the ∃ line to mean that every finite lattice is embeddable, indeed this is true even if we preserve 0 and 1 (if it exists). (For R the question of which lattices are embeddable even without preserving 0 or 1 is, of course, still open.) Undecidability in the ∀∃ line means that the theory is undecidable (via the same set of sentences) for every total extension of the partial infimum relation.

In addition to the long standing and well known open questions about R, these tables suggest two other natural areas for investigation on the boundary between decidability and undecidability. The first is the ∀∃ theory of D(≤,′). This is a very rich theory that includes many interesting and difficult subproblems and a number of partial results. For example, it includes the ∃ theory of D(≤, ∨,′) shown decidable by Montalban [2003]. It is also possible to define 0 at this level without any added complexity and so it is equivalent to the ∀∃ theory of D(0, ≤,′) which includes ∃ theory of D(0, ≤, ∨,′). Now, for all the other decidability results in these tables which do not involve the jump operator, adding 0 to the language presents no serious extra difficulties. This is far from true once we allow the jump. Indeed even the ∃ theory of D(0, ≤,′) is a complex problem about which there are many difficult and interesting partial results. The crucial point is that the addition of 0 requires very fine control over the complexity of the degrees realizing some given ∃ statement in the language with just ≤ and ′. The formula can now specify that witnesses lie in precise intervals with endpoints of the form 0^{(n)}. In contrast, the realizations in the decidability results for the ∃ theory of D(≤,′) and D(≤, ∨,′) (Hinman and Slaman [1991]; Montalban [2003]) produce witnesses which are not even hyperarithmetic.

Among the partial results on the ∃ theory with 0 we mention Lerman [1985] which proves the decidability of the ∃ theory of D with ≤ and additional predicates for the classes in the High/Low hierarchy. Montalban [2004] (answering a question of Lerman [1985]) proves the decidability of ∃ theory of D with ≤, 0 and additional predicates for the classes GL_{n}, GH_{n} and GI (for n ≥ 0) in the generalized high/low hierarchies (which also falls within the ∃ theory of D(0, ≤, ∨,′)). Lempp and Lerman [1996] prove the ∃ theory of R with 0, 1, ≤ and predicates for x^{(n)} ≤_{T} y^{(n)} for every n is decidable. And so, a fortiori, also the ∃ theory of D with 0, ≤ and all of these predicates. Indeed, they can even add ∨ to the language as long as 1 (0′) is omitted). It seems plausible that their methods (which are very complex) may suffice to prove the decidability of the ∃ theory of D(0, ≤,′) and perhaps even with ∨ added to the language.

As for the full ∀∃ theory of D(≤,′), there are many difficult open problems along the road to decidability (including, for example, controlling the jumps of initial segments). On the other hand, the path to undecidability seems quite dark. It is not immediately blocked by our general comments in the introduction on proving undecidability of ∀∃ theories since we do have a function symbol ′ that generates ω-sequences. The problem is how to define them (and relations on them) in a Δ_{0} way using only ≤ and ′.

The new area suggested by these charts is the decision problem for the ∀∃ theory of D(≤ 0′) with ≤ and ∨. This problem turns out to be far from straightforward. It would seem that our only hope is to prove decidability. We have the required initial segment results for decidability from the proof of decidability without ∨ (Lerman and Shore [1988]). The extension of embeddings part, however, has, surprisingly, something of the flavor of the ∀∃ theory of R.

Montalban has shown that we cannot reduce the full ∀∃ decision problem to the extension of embedding problem as has been done in all the other successful proofs of decidability at the ∀∃ level. (The extension of embedding problem for a structure M asks for a characterization of the partial orders X ⊆ Y such that every embedding f : X → M can be extended to one g : Y → M. The decision problem for ∀∃ sentences about one of the degree structures is equivalent to deciding all problems of the form “every embedding of X can be extended to an embedding of some Y_{i} from a specified list. A reduction argument shows that the list can always be taken to have only one element.)

Proposition 4.1 (Montalban) For every x_{1} < x_{2} in (0, 0′) there is either a y such that 0 < y < x_{1} or one such that x_{1} < y < 1 and x_{2} ∨ y = 1 but neither disjunct holds for every x_{1} < x_{2} in (0, 0′).

Proof. If x_{1} ∉ L_{2} then it is not minimal and so there is a nonrecursive y < x_{1}. On the other hand, if x_{1} ∈ L_{2} then 0′ is high over x_{1} and so by the join theorem for high degrees (Posner [1977] or see Lerman [1983 IV.9]) there is a y which joins x_{2} up to 0′. However, there are counterexamples to each disjunct.

Of course, any minimal degree x_{1} < 0′ and any x_{2} between x_{1} and 0′ supply a counterexample to the first disjunct. On the other hand, if we consider the construction of Slaman and Steel [1989] of nonrecursive r.e. degrees a < b such that no degree c < b joins a to b and apply the pseudojump inversion theorem of Jockusch and Shore [1983], we get x_{1} < x_{2} < 0′ (replacing 0 < a < b) such that no y below 0′ and above x_{1} joins x_{2} up to 0′ as required. □

This is reminiscent of the nondiamond (and other) phenomenon in R. (The nondiamond theorem of Lachlan [1966] says that for every pair of incomparable r.e. degrees x_{1}, x_{2} there is either a y with x_{1}, x_{2} ≤_{T} y <_{T} 0′ or one with 0 <_{T} y ≤_{T} x_{1}, x_{2}. On the other hand, there are x_{1}, x_{2} such that x_{1} ∨ x_{2} = 0′ and ones such that x_{1} ∧ x_{2} = 0.) It suggests that there are many problems to consider here.

5 Bibliography

Arslanov, M. M. and Lempp, S. eds. [1999], Recursion theory and Complexity, Proceedings of the Kazan ’97 Workshop, Walter de Gruyter, Berlin.

Bernays, P. and Schoenfikel, M. [1928], Zum Entscheidungsproblem der mathematischen Logik, Math. Ann. 99, 342-372.

Börger, E., Grädel, E. and Gurevich, Y. [1997], The Classical Decision Problem, Springer, Berlin.

Epstein, R. L. [1979], Degrees of Unsolvability: Structure and Theory, LNM 759, Springer-Verlag, Berlin.

Friedberg, R. M. [1957], Two recursively enumerable sets of incomparable degrees of unsolvability, Proc. Nat. Ac. Sci. 43, 236-238.

Harrington, L. and Shelah, S. [1982], The undecidability of the recursively enumerable degrees (research announcement), Bull. Am. Math. Soc., N. S. 6, 79-80.

Hinman, P. G. and Slaman, T. A. [1991], Jump embeddings in the Turing degrees, J. Symbolic Logic 56, 563–591.

Jockusch, C. G. Jr. and Slaman, T. A. [1993], On the Σ_{2}-theory of the upper semilattice of Turing degrees, J. Symbolic Logic 58, 193–204.

Jockusch, C. G. Jr. and Shore, R. A. [1983], Pseudojump operators. I. The r.e. case. Trans. Amer. Math. Soc. 275, 599–609.

Jockusch, C. G. Jr. and Soare, R. I. [1972], Π_{1}^{0} classes and degrees of theories, Trans. Amer. Math. Soc. 173, 33–56.

Kleene, S. C. and Post, E. L. [1954] The upper semi-lattice of degrees of recursive unsolvability, Ann. Math. (2) 59, 379–407

Lachlan, A. H. [1966], The impossibility of finding relative complements for recursively enumerable degrees, J. Symbolic Logic 31, 434-454.

Lachlan, A. H. [1968], Distributive initial segments of the degrees of unsolvability, Z. Math. Logik Grundlagen Math. 14, 457-472.

Lempp, S. and Lerman, M. [1996], The decidability of the existential theory of the poset of recursively enumerable degrees with jump relations, Adv. Math. 120, 1–142.

Lempp, S., Nies, A. and Slaman, T. A. [1998], The Π_{3}-theory of the computably enumerable Turing degrees is undecidable, Trans. Am. Math. Soc. 350, 2719-2736.

Lerman, M. [1971], Initial segments of the degrees of unsolvability, Ann. Math. (2) 93, 365-389.

Lerman, M. [1983], Degrees of Unsolvability, Springer-Verlag, Berlin.

Lerman [1985], On the ordering of classes in high/low hierarchies, Recursion theory week (Oberwolfach, 1984), H.-D. Ebbinghaus, G. H. Müller and G. E. Sacks eds., LNM 1141, Springer, Berlin, 260–270.

Lerman, M. [2000] A necessary and sufficient condition for embedding principally decomposable finite lattices into the computably enumerable degrees, Annals of Pure and Applied Logic 101, 275–297.

Lerman, M. and Shore, R. A [1988], Decidability and invariant classes for degree structures, Trans. Am. Math. Soc. 310, 669-692.

Lerman, M., Shore, R. A. and Soare, R. I. [1984], The elementary theory of the recursively enumerable degrees is not ℵ_{0}-categorical, Adv. Math. 53, 301-320.

Miller, R. G., Nies, A. O. and Shore, R. A. [2004], The ∀∃-theory of R(≤, ∨, ∧) is undecidable, Trans. Am. Math. Soc., to appear.

Minsky, M. L. [1961], Recursive unsolvability of Post’s problem of tag and other topics in the theory of Turing machines, Ann. Math. 74, 437-454.

Montalban, A. [2003], Embedding jump upper semilattices into the Turing degrees, J. Symbolic Logic 68, 989-1014.

Montalban, A. [2004], There is no ordering on the classes in the generalized high/low hierarchy, in preperation.

Muchnik, A. A. [1956], On the unsolvability of the problem of reducibility in the theory of algorithms, Dokl. Akad. Nauk SSSR N.S. 108, 29-32.

Nerode, A. and Shore, R. A. [1997], Logic for Applications, Springer, New York, 2nd ed.

Nies, A., Shore, R. A. and Slaman, T. A. [1998], Interpretability and definability in the recursively enumerable degrees, Proc. London Math. Soc. (3) 77, 241-291.

Posner [1977], High Degrees, Ph.D. Thesis, Univeristy of California, Berkeley.

Ramsey, F. P. [1930], On a problem of formal logic, Proc. London Math. Soc. (2) 30, 338-384.

Sacks, G. E. [1963], Recursive enumerability and the jump operator, Trans. Am. Math. Soc. 108, 223-239.

Sacks, G. E. [1964], The recursively enumerable degrees are dense, Ann. Math. (2) 80, 300-312.

Shepherdson, J. and Sturgis, H. [1963], Computability of recursive functions, J. Assoc. Comp. Mach 10, 217-255.

Shore, R. A. [1978], On the ∀∃-sentences of α-recursion theory, in Generalized Recursion Theory II, J. E. Fenstad, R. O. Gandy and G. E. Sacks eds., Studies in Logic and the Foundations of Mathematics 94, North-Holland, Amsterdam, 331-354.

Shore, R. A. [1981], The theory of the degrees below 0′, J. London Math. Soc. 24 (1981), 1-14.

Shore, R. A. [1999], The recursively enumerable degrees, in Handbook of Computability Theory, Studies in Logic and the Foundations of Mathematics 140, North-Holland, Amsterdam, 169–197.

Shore, R. A. and Slaman, T. A. [1999], Defining the Turing jump, Math. Res. Lett. 6, 711–722.

Simpson, S. G. [1977], First order theory of the degrees of recursive unsolvability, Ann. Math. (2), 105, 121-139.

Slaman, T. A. and Soare, R. I. [2001], Extension of embeddings in the computably enumerable degrees, Ann. Math., 153, 1-43.

Slaman, T. A and Steel, J. R. [1989], Complementation in the Turing degrees, J. Symbolic Logic 54, 160–176.

Soare, R. I. [1987], Recursively Enumerable Sets and Degrees, Springer-Verlag, Berlin. Spector, C. [1956], On degrees of recursive unsolvability, Ann. Math. (2) 64, 581-592.