The ∀∃-Theory of R(≤, ∨, ∧) is Undecidable

Russell G. Miller Department of Mathematics

Cornell University Ithaca NY 14853 Andre O. Nies Office 592 Department of Computer Science University of Auckland Private Bag 92019 Auckland, NZ

Richard A. Shore Department of Mathematics Cornell University Ithaca NY 14853

May 15, 2003

Abstract

The three quantifier theory of (R, ≤_{T}), the recursively enumerable degrees under Turing reducibility, was proven undecidable by Lempp, Nies and Slaman [1998]. The two quantifier theory includes the lattice embedding problem and its decidability is a long standing open question. A negative solution to this problem seems out of reach of the standard methods of interpretation of theories because the language is relational. We prove the undecidability of a fragment of the theory of R that lies between the two and three quantifier theories with ≤_{T} but includes function symbols.

Theorem: The two quantifier theory of (R, ≤, ∨, ∧), the r.e. degrees with Turing reducibility, supremum and infimum (taken to be any total function extending the infimum relation on R) is undecidable. The same result holds for various lattices of ideals of R which are natural extensions of R preserving join and infimum when it exits.

The first author was partially supported by a VIGRE Postdoctoral Fellowship under NSF grant number 9983660 to Cornell University. The third author was partially supported by NSF Grant DMS-0100035. The authors offer their thanks to the referee for several helpful comments.

1 Introduction

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. One 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.

Our interest here is in R, the r.e. degrees under Turing reducibility, and some natural extensions of this structure, but, for the sake of comparison, we also discuss D and D(≤ 0′), the Turing degrees of all sets and the ones below 0′. For D; 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.)

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 the finite extension method, 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 by 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, ch. 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 nontrivial Boolean algebra. The 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]).

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)

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.

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 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].) The natural function on R is the join operator ∨. However, it is uniformly locally finite, i.e. 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. 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. Our solution is to prove undecidability in a sufficiently uniform way so that the proof is independent of the choice of extension. This we do for our main result.

Theorem 1.1 For any total extension ∧ of the partial infimum relation on R, the two quantifier (∀∃) theory of R(≤, ∨, ∧) is undecidable.

Now it is routine to eliminate ∨ by replacing it with its definition (as least upper bound) at the expense of adding one quantifier. Thus, for example, ∀x, y∃z(x ∨ y ≥ z) is equivalent to ∀x, y∃z∀w(x, y ≤ w → w ≥ z). This translation shows that the ∀∃-theory of R(≤, ∨) is reducible to the ∀∃∀-theory of R(≤). The same would be true of ∧ (as greatest lower bound) were it a total infimum function, i.e. ∀x, y∃z(x∧y ≤ z) would be equivalent to ∀x, y∃z∀w(x, y ≥ w → w ≤ z). This needn’t be true for arbitrary extensions of the partial infimum relation on R but the care that we take with our coding to guarantee that it works for all extensions allows us to argue that the ∀∃ sentences of R(≤, ∨, ∧) that witness undecidability can, in fact, be replaced uniformly by equivalent ∀∃∀ sentences of R(≤) so that the previous best result on undecidability is also a consequence of our proof.

Corollary 3.1 (Lempp, Nies and Slaman [1998]): The three quantifier (∀∃∀) theory of R(≤) is undecidable.

We will give the details of the proof in Section 3, once we explain the specific coding of register machines that we employ. As essentially similar codings of register machines can easily be carried out in lattices, the usual interpretation of lattices in D as initial segments shows that our main result also holds for the degrees as a whole and those below 0′.

Corollary 3.2 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.

As for R, the arguments here also imply the previous result that the ∀∃∀ theories of these structures are undecidable. At least in case of D, the boundary here is very fine as Jockusch and Slaman [1993] have proven that the ∀∃ theory of D(≤, ∨) is decidable.

A new corollary of our proof of undecidability is one for the (lattice) structure I(R) of ideals of R with ∨ and ∧. Here both operations are naturally total on the structure. I ∨ J is the ideal generated by I ∪ J, i.e. the downward closure of {a ∨ b | a ∈ I & b ∈ J}, and I ∧ J is the ideal I ∩ J. This structure is an interesting one that has been studied, for example, by Calhoun [1993], Lerman and Calhoun [2001] and Nies [2003]. Also of interest are the structures I_{n}(R) for n ≥ 4 of the Σ_{n}^{0} ideals of R (those ideals I such that {e | deg(W_{e}) ∈ I} is Σ_{n}^{0}) which are each lattices with the same operations as I(R). (Note that by standard index set results I_{n}(R) is trivial for n = 1, 2: If an ideal I of R does not contain 0′ (but does contain 0) then by Yates’ representation theorem [1966] (see Soare [1987 XII, 1.3) applied to K, the complete Π_{4}^{0} set is of the form {k | ∀e(W_{f(k)}^{[e]} ∈ I)} for some recursive f and so I must be at least Σ_{3}^{0}. On the other hand, the class of Σ_{3}^{0} ideals is not closed under ∨, as can be seen by considering a high degree h and a splitting of h into two low degrees a, b. The principal ideals generated by a and b are Σ_{3}^{0} but their join is the one generated by h which is Σ_{4}^{0} but not Σ_{3}^{0}.) Each of these lattices (I(R) and I_{n}(R) for n ≥ 4) is a natural extension of R in the sense that the natural embedding taking a degree in R to the principal ideal it generates is an embedding that preserves order and join as well as infimum when it is defined.

Corollary 3.3 The two quantifier (∀∃) theory of I(R) (I_{n}(R) for n ≥ 4), the lattice of (Σ_{n}) ideals of R, with ⊆, ∨ and ∧ is undecidable.

Once again, after we have the details of the coding in place, an algebraic analysis shows that the principal ideals generated by the degrees doing the coding in R perform the same job in I(R). As both ∨ and ∧ are total functions on I(R), their routine elimination as described above gives the undecidability of the three quantifier theory.

Corollary 3.4 The three quantifier (∀∃∀) theory of I(R) (I_{n}(R) for n ≥ 4), the lattice of (Σ_{n}) ideals of R, with just ⊆ is undecidable.

We also remark that similar algebraic observations show that we can characterize the degrees of the theories of these ideal structures. Indeed the ideas of Nies, Shore and Slaman [1998] would have sufficed as well.

Corollary 3.5 The theory of I(R) is recursively isomorphic to that of true second order arithmetic and that of I_{n}(R) to that of true first order arithmetic for each n ≥ 4.

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 proofs of the corollaries about other degree structures. The final section will supply the recursion theoretic arguments to show that the structures described here can be realized in the r.e. degrees.

We begin 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 in R, we want to use distinct domains D_{i} with least elements 0_{i} and successor functions s_{i} for each register. In our application, these sets and operations will be defined from parameters in R. 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.)

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). More specifically for our purposes, the machine halts if and only if F_{k}(n_{1}, …, n_{k}) is true in every model of P (I) in any class of structures that contains ones isomorphic to the standard model (where each s_{i} on D_{i} is isomorphic to the standard successor function s on ℕ) with all possible recursively enumerable k-ary relations P_{m} on D_{1} × ⋯ × D_{k}. (Validity implies truth in all the structures in our class and if I fails to halt, the standard interpretation of the predicates as the r.e. relations I_{m}(n_{1}, …, n_{k}) gives a structure of the required form in which F (n_{1}, …, n_{k}) is false.) 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 standard models with binary predicates to get undecidability.

As usual for interpretations, we now want to provide formulas Δ_{i}(q⃗, x), Π_{m}(q⃗, x, y) and terms σ_{i}(q⃗, x) of R(≤, ∨, ∧) defining, for each choice of parameters q⃗, sets D_{i} (i = 1, 2), binary relations P_{m} on D_{1} × D_{2} (1 ≤ m ≤ t + 1) and unary functions s_{i} on D_{i} (i = 1, 2). 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) ∧ …) and ∀x_{i}(…) becomes ∀x_{i}(Δ_{i}(q⃗, x) → …). We then replace occurrences of s_{i}(x_{i}) by σ_{i}(q⃗, 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 σ_{i} define functions on the D_{i}: Δ_{1}(q⃗, q_{1}) ∧ Δ_{2}(q⃗, q_{2}) ∧ ∀x_{1}(Δ_{1}(q⃗, x_{1}) → Δ_{1}(q⃗, σ_{1}(x_{1})) ∧ ∀x_{2}(Δ_{2}(q⃗, x_{2}) → Δ_{2}(q⃗, σ_{2}(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.

As long as the class of structures given by all choices of parameters q⃗ includes ones isomorphic to the standard model with all possible r.e. relations as the P_{m}, truth in R for this class of sentences will be undecidable. 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). As long as there are realizations of the D_{i} as a uniformly low independent set of degrees in R, we can define arbitrary r.e. relations on them from parameters in a quantifier free form by using the following special case of Lemma 7.1 of Nies, Shore and Slaman [1998]:

Lemma 2.1 (Nies, Shore and Slaman [1998]) If ⟨a_{j}⟩ is a uniformly r.e. independent set with ⊕a_{i} low and S is any r.e. set then there are u, v such that S = {i : u ≤ a_{i} ∨ v}.

If we assume, for example, that D_{i} = {g_{2j+i} : j ∈ ω} (identified with ℕ in the obvious way) for some independent set of degrees g_{l} with ⊕g_{l} low, then we can apply the lemma to the set of degrees {g_{2j} ∨ g_{2k+1} : j, k ∈ ω} with S_{m} = {⟨j, k⟩ : P_{m}(j, k)} for any r.e. relation P_{m} to provide parameters u_{m}, v_{m} such that the formula u_{m} ≤ x_{1} ∨ x_{2} ∨ v_{m} defines the isomorphic copy of P_{m} on D_{1} × D_{2} and can be taken as the desired quantifier free Π_{m}. Thus the source of all our concerns is providing a quantifier free definition from parameters of a uniformly r.e. independent set ⟨g_{l}⟩ with a term of R that gives the successor relation on them. (Once we have such a set we can pick out the even and odd parts using the same lemma (or exact pairs) and then take the successor functions on each of these two disjoint sets to be simply the two-fold iteration of the original successor function.)

The two known methods for constructing independent sets definable from parameters are essentially those of Harrington and Shelah [1982] and Slaman and Woodin (see Nies, Shore and Slaman [1998]). The sets they defined from parameters are as follows:

• HS(r, b, c) = {g ≤ r : g is maximal s.t. g ∨ b ≱ c}

• SW(r, p, q) = {g ≤ r : g is minimal s.t. g ∨ p ≥ q}.

Here the elements g_{i} of the sets typically constructed are uniformly r.e. and independent while r is taken to be their effective sum and can be made low. Thus the only problem is that the definitions of these sets requires a universal quantifier. We could reduce this to a quantifier free definition by requiring that they define the same set G, for then • G(r, b, c, p, q) = {g ≤ r : g ∨ p ≥ q & g ∨ b ≱ c}.

As a technical convenience that simplifies the construction we note that if we have an HS set ⟨g_{i}⟩ defined from parameters r, b and c then we can weaken the conditions corresponding to the definition of the SW set to require only that, for each i, g_{i} ∨ p ≥ q and, for any w ≤ g_{i}, if w ∨ p ≥ q then w = g_{i}. This clearly suffices to show that G(r, b, c, p, q) = HS(r, b, c). (That HS(r, b, c) ⊆ G(r, b, c, p, q) follows from the condition that g_{i}∨p ≥ q for each g_{i} ∈ HS(r, b, c). To see that G(r, b, c, p, q) ⊆ HS(r, b, c), consider any w ∈ G(r, b, c, p, q). By the maximality condition on HS(r, b, c) there is a g_{i}∈ HS(r, b, c) such that w ≤ g_{i}. Now our weakened requirements guarantee that w = g_{i} as required.) Thus we wish to show that there are parameters r, b, c, p, q such that the set G =⟨g_{i} : i ∈ ω⟩ they define is uniformly r.e. and independent with a low sum.

In addition, we want to define a successor function on these degrees. Actually, we define one on the g_{2j} taking g_{2j} to g_{2j+2} and so our required domain will be these degrees. (Again they can be defined from parameters using the lemma as described above but in fact our construction will also build a degree f_{1} such that D = {g_{2i}}_{i∈ω} = {x : x ∈ G & x ≤ f_{1} ∨ x = g_{0}}.) We use the effective successor structure from Shore [1981] employed in Nies, Shore and Slaman [1998]. This calls for the construction of additional parameters e_{0}, e_{1}, f_{0}, f_{1} such that, for i ∈ ω, (g_{2i} ∨ e_{0}) ∧ f_{0} = g_{2i+1} and (g_{2i+1} ∨ e_{1}) ∧ f_{1} = g_{2i+2}. We can then define the desired successor function on D by s(g_{2i}) = (((g_{2i} ∨ e_{0}) ∧ f_{0}) ∨ e_{1}) ∧ f_{1} =g_{2i+2}. The required result is then the following:

Theorem 2.2 There are r.e. sets R, B, C, P, Q, E_{0}, E_{1}, F_{0}, F_{1}, ⟨H_{i} : i ∈ ω⟩ and ⟨G_{i} : i ∈ ω⟩ with R = ⊕G_{i}; H_{i} = ⊕_{k≠i}G_{k}; F_{0} = ⊕G_{2k+1} and F_{1} = ⊕G_{2k+2} such that (for all i and W)

1. G_{i} ≰_{T} H_{i}.

2. R is low.

3. If W ≤_{T} G_{i} and Q ≤_{T} W ⊕ P then G_{i} ≤_{T} W.

4. If W ≤_{T} R and C ≰_{T} W ∨ B then (∃k)W ≤_{T} G_{k}.

5. C ≰_{T} G_{i} ∨ B.

6. Q ≤_{T} G_{i} ∨ P.

7. deg(G_{2i+1}) = deg(G_{2i} ⊕ E_{0}) ∧ deg(F_{0}).

8. deg(G_{2i+2}) = deg(G_{2i+1} ⊕ E_{1}) ∧ deg(F_{1}).

The proof of this theorem is given in the final section.

Note that as the structures required for the undecidability are coded by parameters such that all the infima needed to define σ_{i} exist in R, the structures coded in R(≤, ∨, ∧) include all the ones needed for the undecidability for any (total) extension ∧ of the partial infimum relation on R. Thus the construction of r.e. degrees r, b, c, p, q, e_{0}, e_{1}, f_{0}, f_{1} as described above suffices to prove our main result (Theorem 1.1) that the two quantifier theory of R(≤, ∨, ∧) is undecidable for any total extension ∧ of the infimum relation.

We now turn to establishing the corollaries mentioned in the Introduction.

3 Applications to Other Structures

We first show that our codings provide a new proof of Lempp, Nies and Slaman’s result that the ∀∃∀ theory of R(≤) is undecidable. We need to find a translation of the sentences ∀q⃗[Θ → (P (I)^{∗} → F_{2}^{∗})] of R(≤, ∨, ∧) into ∀∃∀ ones of R(≤) which preserve truth in R. Note first that the definitions Δ_{i} and Π_{m} of the domains D_{i} and predicates P_{m} use ≤ and ∨ but not ∧. Our only use of the infimum operation is in the definitions σ_{i} of the terms representing the successor operations on the D_{i}. In our translation these terms are defined by composition from the successor function s on D ={g_{2i}} = {x : x ∈ G & x ≤ f_{1} ∨ x = g_{0}} given by s(g_{2i}) = (((g_{2i} ∨ e_{0}) ∧ f_{0}) ∨ e_{1}) ∧ f_{1} =g_{2i+2}. Our primary task then is to eliminate the uses of s in our formulas.

We begin with the correctness condition Θ which for s says that ∀x ∈ D(s(x) ∈ D), i.e. (((g_{2i} ∨e_{0})∧f_{0})∨e_{1})∧f_{1} ∈ D. We use the set D̄ ={g_{2i+1}} = {x : x ∈ G & x ≤ f_{0}} as well and break up the condition into the conjunction of two similar assertions: ∀x ∈ D((x ∨ e_{0}) ∧ f_{0} ∈ D̄) and ∀x ∈ D̄((x ∨ e_{1}) ∧ f_{1} ∈ D). The first is replaced by (∀x ∈ D)(∃y ∈ D̄)(y ≤ x ∨ e_{0}, f)_{0}&(∀x ∈ D)(∀y, z ∈ D̄)(y, z ≤ x ∨ e_{0}, f_{0} → y = z) and the second by the analogous statement switching D with D̄ and e_{0}, f_{0} with e_{1}, f_{1}. We can now eliminate ∨ from this sentence at the expense of one additional quantifier in the usual way to get our Π_{2} correctness condition Θ̂ in the language of R(≤). The first one becomes (∀x ∈ D)(∀u)(∃y ∈ D̄)[∀v(v ≥ x, e_{0} → v ≥ u) → y ≤ u, f]&(∀x ∈ D)(∀y, z ∈ D̄)(∀u)[∀v(v ≥ x, e_{0} → v ≥ u) → ((y, z ≤ u, f_{0}) → y = z))] and the second is analogous.

Our typical sentence on the list of ones showing undecidability now looks like ∀q⃗[Θ̂ → (P (I)^{∗} → F_{2}^{∗})]. Our next task is to eliminate the uses of s (and so ∧) in these formulas. We might as well view P (I)^{∗} → F_{2}^{∗} as a single Σ_{1} sentence in ≤, ∨, s. Our correctness condition Θ̂ says that for each r ∈ D there is a unique v ∈ D̄ and w ∈ D such that (v ≤ r ∨ e_{0}, f_{0}) & (w ≤ v ∨ e_{1}, f_{1}). We can use this property to replace each instance of an application of s. We proceed by an induction on the complexity of terms. Suppose our formula is of the form ∃r⃗φ(r⃗, s(r_{0})). (Note that φ necessarily includes a clause r_{0} ∈ D.) We replace this with the sentence ∃r⃗(∃v_{0} ∈ D̄)(∃w_{0} ∈ D)[(v_{0}≤ r ∨ e_{0}, f_{0}) & (w_{0}≤ v_{0}∨e_{1}, f_{1}) & φ(r⃗, w_{0}/s(r_{0}))]. (We use the notation w_{0}/s(r_{0}) to indicate that we have substituted w_{0} for the term s(r_{0}) in the ambient formula.) Assuming the correctness condition Θ̂, this is clearly equivalent to the original ∃r⃗φ(r⃗, s(r_{0})). We can now proceed inductively to eliminate all occurrences of s and produce a Σ_{1} formula in ≤, ∨ equivalent under the assumption Θ̂ to our original ∃r⃗φ(r⃗, s(r_{0})). We can now apply the dual procedure to the one used to eliminate ∨ from Π_{1} formulas in ≤, ∨ to get a Σ_{2} formula Ψ(I) in just ≤ equivalent to (P (I)^{∗} → F_{2}^{∗}). We then have our new family of formulas ∀q⃗[Θ̂ → Ψ(I)] which are ∀∃∀ and whose validity in R is undecidable as required to prove Corollary 3.1.

Corollary 3.1 (Lempp, Nies and Slaman [1998]): The three quantifier (∀∃∀) theory of R(≤) is undecidable.

Next, we consider D and D(≤ 0′). First note that it is straightforward to construct Δ_{2}^{0} lattices with top r, individual elements b, c, p, q, e_{0}, e_{1}, f_{0}, f_{1} and a family of independent (even minimal) elements g_{i} satisfying all the algebraic facts required in Theorem 2.2 and additional elements u and v defining any fixed r.e. subset of the g_{i} as in Lemma 2.1. We can now use the standard embedding theorems from Lerman [1983] to realize these lattices as initial segments of D or D(≤ 0′). Our arguments for undecidability now work just as well in these structures and so we have the analogous results.

Corollary 3.2 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.

Finally, we turn our attention to the lattices I(R) (I_{n}(R), n ≥ 4) of (Σ_{n}) ideals of R with ∨ and ∧. Recall that the operations ∨ and ∧ are defined in the usual way for structures of ideals (I ∨ J is the ideal generated by I ∪ J and I ∧ J is the ideal I ∩ J) and are both total operators on I(R) and I_{n}(R) for n ≥ 4.

Corollary 3.3 The two quantifier (∀∃) theory of I(R) (I_{n}(R), n ≥ 4), the lattice of (Σ_{n}) ideals of R, with ∨ and ∧ is undecidable.

Proof. We claim that the principal ideals generated by the degrees constructed to satisfy Theorem 2.2 and Lemma 2.1 have all the required properties in I(R) that the degrees themselves had in R. The crucial fact is the quantifier free definability of the set {g_{i}} as G(r, b, c, p, q). We denote the principal ideal generated by a degree x by (x) and want to establish the corresponding facts in I(R). Consider any ideal I ⊆ (r) such that (q) ⊆ I ∨ (p) and (c) ⊈ I ∨ (b). The first assumption tells us that there is an e ∈ I such that q ≤ e ∨ p while the second guarantees that c ≰ e ∨ b. Thus e is one of the g_{i} and so (g_{i}) ⊆ I. On the other hand, if h ∈ I then (by our second assumption again) c ≰ h ∨ g_{i}∨b. The HS maximality property of g_{i} then guarantees that h ∨ g_{i} ≤ g_{i} and so I ⊆ (g_{i}) as required.

The other facts needed from Theorem 2.2 are that (g_{2i+1}) = [(g_{2i}) ∨ (e_{0})] ∧ (f_{0}) and the analogous one for (g_{2i+2}). These follow immediately from the trivial general facts about I(R) (I_{n}(R), n ≥ 4) that, for all degrees x, y, (x ∨ y) = (x) ∨ (y) and, if x ∧ y exists, (x ∧ y) = (x) ∧ (y). The only other algebraic fact needed is that the principal ideals given by the degrees constructed for Lemma 2.1 have the analogous property in I(R). This too follows immediately from the first trivial fact.

The same arguments work for I_{n}(R) for n ≥ 4. □

As remarked above, when ∨ and ∧ are total functions the two quantifier theory with ≤, ∨ and ∧ is reducible to the three quantifier theory with just ⊆ and so we also have proven Corollary 3.4.

Corollary 3.4 The three quantifier (∀∃∀) theory of I(R) (I_{n}(R), n ≥ 4), the lattice of (Σ_{n}) ideals of R, with just ⊆ is undecidable.

We now explain how similar considerations characterize the theories of these structures of ideals.

Corollary 3.5 The theory of I(R) is recursively isomorphic to that of true second order arithmetic and that of I_{n}(R) to that of true first order arithmetic for each n ≥ 4.

Proof. Consider the effective successor models {g_{2i} : i ∈ ω} in R with the relevant parameters as constructed here. As remarked above the effective successor models defined by the ideals (g_{2i}) = {a ≤_{T} g_{2i}} generated by the relevant degrees are definable in the same way in I(R) (I_{n}(R), n ≥ 4), using the analogous successor function. We begin by noting that we could add parameters to define additional relations of the form supplied by Lemma 2.1. We want to choose ones that define a structure for arithmetic on one subset of the set D = {(g_{2i})} of ideals. We let D_{k} = {(g_{8i+2k}) : i ∈ ω} for k ≤ 3 and define the required relations for order, addition and multiplication on D_{0}. We begin with parameters that pick out the relations S_{k} = {{(g_{8i}), (g_{8i+2k})} : i ∈ ω} for 1 ≤ k ≤ 3 that identify the corresponding elements of D_{0} and D_{k}. We can then define, for example, the natural ordering on D_{0} by parameters that pick out {{(g_{2i+1}), (g_{2j+2})} : i ≤ j} and similarly plus and times by picking out {{(g_{2i+1}), (g_{2j+2}), (g_{2k+3})} : i + j = k} and {{(g_{2i+1}), (g_{2j+2}), (g_{2k+3})} : i · j = k}. One can then say that the structure so defined is a model of arithmetic in the usual way.

The problem now is to find a nonempty definable class C of structures in I(R) (I_{n}(R)), containing the structure defined above, such that every structure in C is isomorphic to the standard model of arithmetic. C will be defined by saying that there exist parameters I_{e_{i}} and I_{f_{i}} (i = 0, 1), I_{b}, I_{c}, etc. (corresponding to the parameters e_{i}, f_{i}, b, c, … in our construction on degrees), and an ideal J_{0} serving as 0 in the model of arithmetic, satisfying a conjunction of correctness conditions. (Notice that here we cannot assume or require that these parameters be principal ideals.)

We use the effectiveness of the successor function. As is argued in Shore [1981] or Nies, Shore and Slaman [1998], we can generate all representatives of degrees in each element J_{i} = s^{i}(J_{0}) of the structure, uniformly in i, in a way that is effective in ≤ and ∨ on degrees, beginning with representatives of the degrees in the ideals J_{0}, I_{e_{i}}, and I_{f_{i}} (i = 0, 1).

deg(W_{k}) ∈ s(J_{0}) ⟺ deg(W_{k}) ∈ (((J_{0} ∨ I_{e_{0}}) ∧ I_{f_{0}}) ∨ I_{e_{1}}) ∧ I_{f_{1}}
⟺ (∃b, c, d)[deg(W_{b}) ∈ J_{0} & deg(W_{c}) ∈ I_{e_{0}} & deg(W_{d}) ∈ I_{e_{1}} &
deg(W_{b} ⊕ W_{c}) ∈ I_{f_{0}} & W_{k} ≡_{T} W_{b} ⊕ W_{c} ⊕ W_{d} & deg(W_{k}) ∈ I_{f_{1}}].

Now all statements here are Σ_{n} (including the Turing equivalence, since n ≥ 4), because all these ideals are in I_{n}(R). By iterating, we derive a Σ_{n} formulation of “deg(W_{e}) ∈ s^{i}(J_{0})” uniformly in i.

The independence of the defined set G(I_{r}, I_{b}, I_{c}, I_{p}, I_{q}) can also be guaranteed by a correctness condition saying that for each element of the defined set there is something above all the others but not above it. Thus the ideal generated by all the J_{i} will not contain any elements of G(I_{r}, I_{b}, I_{c}, I_{p}, I_{q}) other than the J_{i}. So as usual, if we require of our model that every proper initial segment have a maximal element (all in the ordering defined on the structure) then we have picked out precisely the standard models. Once we have defined this class of standard models of arithmetic, we have guaranteed that each theory is at least as complicated as true first order arithmetic. As each I_{n}(R) is arithmetical, this completely characterizes the complexity of their theories. For I(R) we simply note that the independence of the J_{i} guarantees that every subset is uniquely determined by the ideal it generates and so quantification over I(R) codes full second order quantification over each standard model of arithmetic picked out by our definition. As I(R) is itself defined in second order arithmetic, its theory is equivalent to that of true second order arithmetic as required. □

Corollary 3.6 For m > n ≥ 4, the ideal lattices I_{m}(R) and I_{n}(R) are not elementarily equivalent, nor is any of them elementarily equivalent to I(R).

Proof. Let S ⊆ ω be a Σ_{n+1}-complete set. The sentence ψ which we build to distinguish the lattice I_{m}(R) from I_{n}(R) will say that there exists a standard model of arithmetic encoded in the lattice by parameters I_{e_{0}}, I_{f_{0}}, etc., such that some element of the lattice can use this model to compute S. The existence of a standard model requires only the existence of a set of parameters satisfying the conditions given in the preceding proof. In the rest of the sentence, we say that there exists an element I in the lattice such that for every i,

i ∈ S ⟺ J_{i} ⊆ I,

where J_{i} = s^{i}(J_{0}) is the ideal corresponding to i in the specified standard model. (Thus I codes the set S in this model.) To say “i ∈ S” in the language of lattices, we use the standard model given by the parameters and the Σ_{n+1} definition of S.

In I_{m}(R), by the preceding results, we have a standard model of arithmetic on certain ideals {J_{i} : i ∈ ω}. Let J_{S} be the ideal consisting of finite joins d_{1} ∨ ⋯ ∨ d_{p} with each d_{j} ∈ J_{i_{j}} for some i_{j} ∈ S. We claim that J_{S} lies in I_{m}(R):

{e : (∃p)(∃i_{0}, … i_{p} ∈ S)[deg(W_{e}) ∈ ∨_{j=0}^{p} J_{i_{j}}]} =

{e : (∃p, i_{0}, … i_{p}, k_{0}, … k_{p})(∀l ≤ p)[i_{l} ∈ S & deg(W_{k_{l}}) ∈ s^{i_{l}}(J_{0}) & W_{e} ≤_{T} ⨁_{j=0}^{p} W_{k_{j}}]}.

As noted above, s^{i_{l}}(J_{0}) is a Σ_{m}-ideal uniformly in i. Thus J_{S} is indeed a Σ_{m}-ideal, and I_{m}(R) (and I(R)) satisfy ψ.

Now suppose that we have parameters in I_{n}(R) defining a standard model of arithmetic on ideals {J_{i} : i ∈ ω}, and that I ∈ I_{n}(R) is a (not necessarily principal) ideal with {i : J_{i} ⊆ I} = S. Then there would be a Σ_{n} formula θ defining {e : deg(W_{e}) ∈ I}, so we would have

i ∈ S ⟺ J_{i} ⊆ I ⟺ (∀a ∈ J_{i})[a ∈ I] ⟺ (∀e)[deg(W_{e}) ∈ s^{i}(J_{0}) ⟹ θ(e)].

This is impossible for the Σ_{n+1}-complete set S, since the rightmost formula is Π_{n+1}. Therefore the sentence ψ fails in I_{n}(R), whereas it holds in I_{m}(R) and in I(R).

4 Construction

To prove our required technical result on degrees, Theorem 2.2, it suffices to construct r.e. sets satisfying the requirements of the following Theorem:

Theorem 4.1 There exist sets G_{i} (i ∈ ω), P, Q, B, C, E_{0}, E_{1}, and R = ⊕G_{i} satisfying the following requirements for all e, i, j, k, and x in ω and all computable functionals Ω, Φ, Λ, Υ, and Ψ:

Requirements:

D_{i,Ω} :  G_{i} ≠ Ω^{H_{i}}, where H_{i} = ⊕_{k≠i} G_{k}
L_{Φ,x} :  [(∃^{∞}s) Φ^{R}(x)[s]↓] ⟹ Φ^{R}(x)↓
M_{i,j,Λ,Υ} : W_{j} = Υ^{G_{i}} ⟹ [Λ^{W_{j}⊕P} = Q ⟹ (∃Θ) G_{i} = Θ^{W_{j}}]
N_{e,Φ} :  W_{e} = Φ^{R} ⟹ [(∃Γ) C = Γ^{W_{e}⊕B} or (∃k)(∃Δ) W_{e} = Δ^{G_{k}}]
P_{i,Ψ} :  C ≠ Ψ^{G_{i}⊕B}
R_{k} :  (∃Ξ)Q = Ξ^{G_{k}⊕P} .

Lattice requirements: (Here F_{0} = ⊕_{k} G_{2k+1} and F_{1} = ⊕_{k} G_{2k+2}.)

T_{2i} :  G_{2i+1} ≤_{T} G_{2i} ⊕ E_{0}
T_{2i+1} :  G_{2i+2} ≤_{T} G_{2i+1} ⊕ E_{1}
U_{e,2i} :  Φ_{e}^{G_{2i}⊕E_{0}} = Φ_{e}^{F_{0}} total ⟹ Φ_{e}^{F_{0}} ≤_{T} G_{2i+1}
U_{e,2i+1} : Φ_{e}^{G_{2i+1}⊕E_{1}} = Φ_{e}^{F_{1}} total ⟹ Φ_{e}^{F_{1}} ≤_{T} G_{2i+2}.

(Here and afterwards, the notation “[s]” at the end of a term or equation indicates that we refer to the approximation at stage s of each set, oracle and function used there. Thus, for example, the hypothesis of the requirement L_{Φ,x} is that there are infinitely many stages s at which Φ_{s}^{R_{s}}(x) converges.)

As in Nies, Shore and Slaman [1998], we begin by choosing an effective ordering of all the D-, M-, N-, P-, R-, and U-requirements, in order type ω, such that for all i and j:

• R_{i} precedes every D_{i,Ω} and every U_{e,i} in the ordering (i.e. R_{i} has higher priority than D_{i,Ω} and U_{e,i}); and

• both R_{i} and R_{j} precede every M_{i,j,Λ,Υ}.

(The requirements T_{i} are global requirements and will not be given a priority rank or placed on the tree. The requirements L_{Φ,x} will play a role in priority arguments, as described below, but they also are not placed on the tree.)

This ordering yields a specific priority order on the N-requirements, which we write as N_{0}, N_{1}, …, defining e_{i} and Φ_{i} so that N_{i} denotes N_{e_{i},Φ_{i}}. Next we construct a tree T. Each node on the tree will have a specific requirement assigned to it, will play a particular strategy to attempt to satisfy that requirement, and will have one immediate successor for each possible outcome of the requirement. For brevity, if the requirement D_{i,Ω} is assigned to a node α, we will call α a D_{i,Ω}-node, and also a D-node; similarly with all other requirements. Below, we name the outcomes for each type of node and explain how the construction works to select one of the outcomes and satisfy the node’s requirement.

We view the tree T as growing upwards from a root node. The relation ≺ will represent higher priority: α ≺ β if α is to the left of β on T or α ⊊ β, i.e. exactly when α has higher priority than β. To define T and determine which requirement is assigned to each node ρ ∈ T, we need the following definition.

Definition 4.2 Let ρ ∈ T. Each requirement is either active along ρ (via a single node ⊂ ρ), or satisfied along ρ (again via a single node ⊂ ρ), or neither, according to the following inductive definition. (Notice that a requirement cannot be both active and satisfied along the same node.)

If ρ is the empty string, then no requirement is active or satisfied along ρ. Otherwise, let η = ρ^{−}, the immediate predecessor of ρ.

If a D-, M-, N-, R-, or U-requirement is assigned to η, then every requirement active or satisfied along η via some β is also active or satisfied (respectively) along ρ via β. Also, the requirement assigned to η is active along ρ via η (if it is an N-requirement and ρ = ηˆ ⟨∞⟩) or satisfied along ρ via η (otherwise).

If η is a P_{i,Ψ}-node, then we must consider the successors of η separately.

• If ρ = ηˆ ⟨f⟩ or ρ = ηˆ ⟨w⟩, then every requirement active or satisfied along η via some β is also active or satisfied (respectively) along ρ via β, and P_{i,Ψ} itself is satisfied along ρ via η.

• Otherwise, according to our definition below of the successors of η, ρ = ηˆ ⟨a_{l}⟩ for some l ∈ ω such that N_{l} is active along η via some α. We then define this N_{l} to be satisfied along ρ via α, and every N-requirement active or satisfied along α via some β ⊂ α to be active or satisfied (respectively) along ρ via the same β. All other N-requirements are neither active nor satisfied along ρ. (In particular, Nrequirements which were active or satisfied along η but not along α will be injured by the action we take at node ρ and hence are neither active nor satisfied along ρ.) Requirements of types other than N which were active or satisfied along η via any β remain active or satisfied (respectively) along ρ via β, and P_{i,Ψ} itself is satisfied along ρ via η.

With this definition, we assign to ρ the requirement of highest priority that is neither active nor satisfied along ρ. The immediate successors of ρ depend on the type of requirement assigned. For each possible outcome y of ρ as defined below, we add an immediate successor ρˆ ⟨y⟩ of ρ to T.

The possible outcomes of each node, and their meanings, are as follows:

• If ρ is a D_{i,Ω}-node, then the two possible outcomes for ρ, in order, are f < w. The node ρ finds a witness element w_{ρ}^{i}, as in a Friedberg-Muchnik construction, waits for the witness to be realized, and then attempts to put it into G_{i}. The outcome w holds while we wait for the witness element to be realized. If it is never realized, then it never enters G_{i}, so the requirement is satisfied. If it is realized at some stage, then we preserve the convergence of the computation Ω^{H_{i}}(w_{ρ}^{i}) ↓= 0 by initializing all nodes ≻ ρ, and attempt to enumerate the witness element into G_{i}, by allowing it to enter the pinball machine associated with the satisfaction of the U- and Trequirements, starting at node ρ. Each U- and P-node below ρ periodically allows elements (“balls”) to pass its gate, thereby giving those elements its permission to enter their target sets. Other elements may be assigned to the witness as traces and targeted for sets E_{0}, E_{1}, or G_{i−1}, G_{i−2}, … to satisfy the T-requirements. Assuming that ρ is on the true path, w_{ρ}^{i} will eventually pass every gate below ρ and enter G_{i}, at which point we switch to the outcome f. This represents a “finite win” for the requirement D_{i,Ω}, since we have now satisfied G_{i}(w_{ρ}^{i}) ≠ Ω^{H_{i}}(w_{ρ}^{i}).

D-nodes (and M-nodes, described below) do injure the negative requirements L_{Φ,x} by enumerating elements into R. At certain stages a requirement L_{Φ,x} may initialize cofinitely many nodes on T in order to preserve the computation Φ^{R}(x). Also, each time the node ρ is initialized by another node (as opposed to being initialized by an L-requirement), it loses some priority vis-a-vis the L-requirements. This guarantees that even if ρ is to the right of the true path and enumerates infinitely many elements into R, it will only injure each L-requirement finitely often.

• If ρ is a U_{e,i}-node, then the possible outcomes of ρ are:

p_{0} < p_{1} < p_{2} < ⋯,

ordered as given. The outcome p_{r} represents a restraint of length r placed on G_{i}⊕E_{0} and F_{0} (or on G_{i} ⊕ E_{1} and F_{1}, depending on the parity of i) as in the pinball-style constructions for lattice embeddings in Lerman [1973] and related works. A “ball targeted for G_{i}” is a number which some D- or M-node α would like to put into G_{i}, and will be named w_{α}^{i}. The node ρ acts as a gate in the pinball machine. For every α ⊃ ρ, every ball w_{α}^{i} must wait at gate ρ until the ball can enter G_{i} without injuring the requirement U_{e,i}. Occasionally such an α may also want to put a ball e_{α}^{j} into the set E_{j} (for j = 0 or 1), and again the gate ρ will make that ball wait until the enumeration will not injure U_{e,i}. If the hypothesis of U_{e,i} is satisfied, then the restraints will drop to 0 infinitely often; if not, then they will converge to a finite limit, and every node above that outcome will have the correct guess about the limit, hence will only use witnesses large enough not to injure that restraint.

• If ρ is an R_{k}-node, then the only possible outcome is ∞. At each ρ-stage, we extend the functional Ξ^{G_{k}⊕P} being built by R_{k}. The only possible injury to this construction occurs when some M_{k,j,Λ,Υ}-node wishes to enumerate an element into Q, for reasons described below. Each M-node enumerates at most one element x after its last initialization, and any M-node ⊃ ρ will enumerate its x into Q only after ensuring that some change in G_{k} ⊕ P will allow ρ to redefine Ξ_{ρ}^{G_{k}⊕P} (x) = 1.

• If ρ is an M_{i,j,Λ,Υ}-node, then the possible outcomes are

f < ∞ < w.

We have some control over the enumeration of W_{j} using the hypothesis W_{j} = Υ^{G_{i}}, and this in turn affects the hypothesis Λ^{W_{j}⊕P} = Q. The outcome w denotes a nonexpansionary stage for the latter hypothesis, meaning that the length of agreement between W_{j} and Υ^{G_{i}} is not sufficient for us to guarantee any increase in the length of agreement between Λ^{W_{j}⊕P} and Q. If there are cofinitely many nonexpansionary stages, then M_{i,j,Λ,Υ} will be satisfied.

On the other hand, if the length of agreement between W_{j}[s] and Υ^{G_{i}}[s] has increased sufficiently to enable a longer length of agreement l between Λ^{W_{j}⊕P} [s] and Q[s] to be computed, we call s + 1 a ρ-expansionary stage, and we attempt to extend our functional Θ_{ρ} to compute G_{i} from W_{j} on the domain l, setting the use θ_{ρ}^{W_{j}}(y)[s + 1] = λ^{W_{j}⊕P} (y)[s] and preserving the equality of these uses, as described below. If we succeed, the outcome is ∞. If there are infinitely many ρ-expansionary stages and we succeed in extending Θ_{ρ} at every one, then the true path will contain ρˆ ⟨∞⟩.

If, at some ρ-expansionary stage s + 1, we cannot extend Θ_{ρ} as above, then we will be able to achieve a finite win, denoted by the outcome f. Some number, which we designate as x_{ρ}, must have entered G_{i} since the last ρ-expansionary stage r+1, with no change to W_{j}↾λ^{W_{j}⊕P} (x_{ρ})[r] up until stage s (since such a change would allow us to redefine Θ_{ρ}^{W_{j}}(x_{ρ})[s+1]). We attempt to enumerate x_{ρ} into Q to make Λ^{W_{j}⊕P} ≠ Q, since the absence of any W_{j}-change ensures that Λ^{W_{j}⊕P} (x_{ρ})[s] ↓= 0. (Recall that the use θ_{ρ} matches the use λ.) We will preserve this finite win by initialization, imposing sufficient restraints on P and G_{i} to prevent W_{j} from changing, since W_{j} = Υ^{G_{i}}.

Before enumerating x_{ρ} into Q, however, we must ensure that this enumeration will not injure any higher-priority R_{k}-node β, since such a β builds a functional Ξ_{β} with the intention that Ξ_{β_{k}}^{G_{k}⊕P} = Q. When we enumerate x_{ρ} into Q at a later stage t+1, therefore, we will want to enumerate ξ_{β_{k}}^{G_{k}⊕P} (x_{ρ})[t] into P, allowing β_{k} to redefine its functional at the next β_{k}-stage. On the other hand, if ξ_{β_{k}}^{G_{k}⊕P} (x_{ρ}) < λ^{W_{j}⊕P} (x_{ρ})[t], then this enumeration would allow Λ^{W_{j}}(x_{ρ})[t + 1] to change as well, which would destroy our diagonalization. For k ≠ i, we avoid this problem by first enumerating an element w_{ρ}^{k} = ξ_{β_{k}}^{G_{k}⊕P} (x_{ρ})[s] into the set G_{k}, which allows β_{k} to increase the ξ_{β_{k}}- use without permitting any change in Θ_{ρ}. (Of course, this takes time, since w_{ρ}^{k} must proceed through the pinball machine, starting at ρ, before entering G_{k}.) When we finally enumerate x_{ρ} into Q at a stage t + 1, our P -enumerations at that stage will allow for changes in Ξ_{β_{k}}^{W_{j}}(x_{ρ})[t + 1] while maintaining Λ^{W_{j}⊕P} (x_{ρ})[t + 1]↓= 0.

The requirement R_{i} is also assigned to some β_{i} ⊂ ρ, and the strategy above would not work for it, since any G_{i}-enumeration after stage s could allow a change in W_{j} = Υ^{G_{i}}[s], hence in Λ^{W_{j}⊕P} (x_{ρ})[s], ruining our diagonalization. (P -enumerations, which could also ruin the diagonalization, are discussed below.) Fortunately, we do not need any G_{i}-enumeration, because the ball x_{ρ} was chosen at a stage s + 1 when it had just entered G_{i} itself. β_{i} will have increased the use ξ_{β_{i}}^{G_{i}⊕P} (x_{ρ})[s] to be large, hence > λ^{W_{j}⊕P} (x_{ρ})[s]. (Recall that any change in this λ-use between stages r and s would have allowed us to extend the functional Θ_{ρ} so that Θ_{ρ}^{W_{j}}(x_{ρ}) = G_{i}(x_{ρ})[s+1].) Therefore, we make no further G_{i}-enumerations, but simply enumerate ξ_{β_{i}}^{G_{i}⊕P} (x_{ρ})[s] into P at the stage t + 1 when x_{ρ} enters Q. β_{i} will then be able to redefine Ξ_{β_{i}}^{G_{i}⊕P} (x_{ρ}) = 1 at the next β_{i}-stage, as required.

It is important in the preceding construction that we keep the use θ_{ρ}^{W_{j}}(x) equal to λ^{W_{j}⊕P} (x) at each stage. If the λ-use became larger, then a number > θ_{ρ}^{W_{j}}(x_{ρ})[r] which entered W_{j} between stages r and s might leave λ^{W_{j}⊕P} (x_{ρ}) > ξ_{β_{i}}^{G_{i}⊕P} (x_{ρ})[s] so that the P -enumerations would destroy our diagonalization against Λ^{W_{j}⊕P} = Q, without letting us redefine Θ_{ρ}^{W_{j}}(x_{ρ})[s+1] = 1. So we must ensure that P↾λ^{W_{j}⊕P} (x) is preserved for every x which might eventually play the role of x_{ρ}, i.e. any ball w_{γ}^{i} (with ρˆ ⟨∞⟩ ⊆ γ) targeted for G_{i}.

To make this happen, we refuse to allow any ball w_{α}^{k} to enter the pinball machine (the preliminary step to entering G_{i}) if its entry into G_{i} could create a P - enumeration which might upset the strategy for a higher-priority w_{γ}^{i}. In particular, if ρˆ ⟨∞⟩ ⊆ α, then α thinks that the expansionary outcome of ρ holds, and so α refuses to release any ball w_{α}^{k} into the pinball machine until w_{α}^{k} ∈ dom(Θ_{ρ}^{W_{j}}), that is, until the λ-use on all numbers ≤ w_{α}^{k} has been chosen and guaranteed by agreement between W_{j} and Υ^{G_{i}}. (In particular, the λ-use of all balls from higher-priority nodes γ has been chosen by then.) If w_{α}^{k} does enter G_{k}, then the R_{k}-node β ⊂ α will subsequently choose the use ξ_{β}^{G_{k}⊕P} (w_{α}^{k}) to be large, hence larger than the λ-use of any ball w_{γ}^{i} from any node γ ≺ α. This use ξ_{β}^{G_{k}⊕P} (w_{α}^{k}) may subsequently be enumerated into P by some other M-node, but it will not change P↾λ^{W_{j}⊕P} (w_{γ}^{i}) for any γ ≺ α. Thus, it will not injure the strategy of any M-node of higher priority than α.

(The same is true for any trace for w_{α}^{k}: the corresponding R-node will choose the Ξ-use of the trace to be large after the trace enters its target set, hence after w_{α}^{k} was released, hence after w_{γ}^{i} entered dom(Θ_{ρ}^{W_{j}}). So this Ξ-use will also be greater than λ^{W_{j}⊕P} (w_{γ}^{i}) and can safely be enumerated into P. Therefore, we define every trace to be certified automatically. Only witness balls chosen by D- and M-nodes must wait for certification.)

We will say that w_{α}^{k} is certified when it has entered the domains of all such Θ_{ρ}^{W_{j}}- functionals (for all ρ with ρˆ ⟨∞⟩ ⊆ α), and we require all balls targeted for any G_{k} (whether from D-nodes, from M-nodes, or traces for other balls) to be certified before moving through the pinball machine. If α is on the true path, then the expansionary outcome ρˆ ⟨∞⟩ does hold, and so the domain of Θ_{ρ}^{W_{j}} will eventually grow large enough to include w_{α}^{k}. Thus no ball from a node on the true path will be forced to wait forever before entering the pinball machine.

• If ρ is an N_{e,Φ}-node, then the possible outcomes of ρ are ∞ and w, ordered with ∞ < w. The outcome w denotes a nonexpansionary stage, i.e. a stage at which the length of agreement between W_{e} and Φ^{R} has not increased, so that we wait without taking any action. ∞ represents the outcome of an expansionary stage; if we have infinitely many such stages, then N_{e,Φ} goes about the business of trying to build Γ_{ρ} to compute C from W_{e} ⊕ B. As described below, this process can be injured by lower-priority P-nodes, making this a 0′′′-construction.

• If ρ is a P-node, let K be the finite set of higher-priority N -requirements which ρ may injure:

K = {k : N_{k} is active along ρ via some α_{k}} = {k_{0} < k_{1} < ⋯ k_{n}}.

Then the set of possible outcomes of ρ is the following, ordered as given:

f < a_{k_{0}} < a_{k_{1}} < ⋯ < a_{k_{n}} < w.

For P-nodes ρ, we attempt to achieve a finite win by choosing a witness z_{ρ}, waiting for Ψ^{G_{i}⊕B}(z_{ρ})[s] ↓= 0 at some stage s, and then putting z_{ρ} into C, so as to force C ≠ Ψ^{G_{i}⊕B}. The outcome f denotes our success in doing so, with the construction initializing nodes ≻ ρ at stage s to preserve (G_{i} ⊕ B)↾ ψ^{G_{i}⊕B}(z_{ρ})[s]. The outcome w denotes that we are waiting for this convergence to occur. (If we wait forever, then P_{i,Ψ} will be satisfied.)

However, an N_{e,Φ}-node α ⊂ ρ may object to letting z_{ρ} enter C, since this would disrupt its own computation of C from W_{e} ⊕ B via its functional Γ_{α}. The easiest way around this difficulty is to enumerate the current use γ_{α}^{W_{e}⊕B}(z_{ρ})[s] into B, thereby allowing α to change the value of Γ_{α}^{W_{e}⊕B}(z_{ρ}) to 1. However, we can only do this if γ_{α}^{W_{e}⊕B}(z_{ρ}) > ψ^{G_{i}⊕B}(z_{ρ})[s], since otherwise the change in B would ruin the convergence Ψ^{G_{i}⊕B}(z_{ρ})[s] = 0 and leave P_{i,Ψ} still unsatisfied.

To handle this issue, we check in turn with each requirement N_{k} = N_{e_{k},Φ_{k}} active at ρ via one of the α_{k}, starting with the lowest-priority one N_{k_{n}} and working down to the highest-priority one N_{k_{0}}. If γ_{α_{k}}^{W_{e_{k}} ⊕B}(z_{ρ}) > ψ^{G_{i}⊕B}(z_{ρ})[s], then N_{k} does not object to the entry of z_{ρ} into C, and we continue with the next-higher-priority N - requirement. Otherwise, we wait until the next ρ-stage, offering W_{e_{k}}↾γ_{α_{k}}^{W_{e_{k}} ⊕B}(z_{ρ})[s] the opportunity to change (for technical reasons having to do with Lemma 5.15).

If no such W_{e_{k}}-change occurs, we then enumerate γ_{α_{k}}^{W_{e_{k}} ⊕B}(z_{ρ})[s] into B[s + 1], destroying both of the computations Γ_{α_{k}}^{W_{e_{k}} ⊕B}(z_{ρ})[s] and Ψ^{G_{i}⊕B}(z_{ρ})[s]. In this case we make the outcome a_{k} eligible at stage s. In doing so, we give up our hope of a finite win for ρ with the current realization of z_{ρ}, and also disrupt the computations Γ_{α_{l}}^{W_{e_{l}}⊕B}(z_{ρ})[s] for every l > k. This procedure will result in a win for ρ if we repeat it infinitely often, since in that case Ψ^{G_{i}⊕B}(z_{ρ}) must diverge. For the node α_{k}, each time we make such a B-enumeration, we take a further step in the construction of a functional Δ_{ρ,k}. If ρˆ ⟨a_{k}⟩ lies on the true path, then the functional Δ_{ρ,k} will receive such attention infinitely often and will compute W_{e_{k}} from G_{i}, thereby satisfying N_{k}. Hence we say that N_{k} is satisfied via α along nodes ⊇ ρˆ ⟨a_{k}⟩, meaning that α_{k} does not actively try to protect its functional Γ_{α_{k}} at such nodes, since ρ has constructed Δ_{ρ,k} to satisfy N_{k} instead. This outcome is described in more detail on page 28, in Subcase 3 of the construction for P-nodes.

While the outcome a_{k} does satisfy N_{k}, it also disrupts the functionals Γ_{α_{l}} for all l > k in K, without doing anything to build Δ-functionals for the requirements N_{l}. Those requirements all have lower priority than N_{k}, and are immediately reassigned, in the same order, to ρˆ ⟨a_{k}⟩, its immediate successors, their immediate successors, and so on until each has been assigned to another node σ on each path through ρˆ ⟨a_{k}⟩. Thus, along every path through ρˆ ⟨a_{k}⟩, each such N_{l} now is assigned to a new α ⊃ ρ, with the assurance that the requirement N_{k} will never destroy the functional Γ_{α} the way it destroyed Γ_{α_{l}}. By induction, therefore, each N_{l} will be reassigned to higher nodes only finitely often along any fixed path through the tree.

The N_{j}-requirements which are active along α_{k} emerge with their Γ-functionals unscathed by ρ. These nodes all have higher priority than N_{k} (i.e. have j < k), so will have

γ_{α_{j}}^{W_{e_{j}} ⊕B}(z_{ρ}) < γ_{α_{k}}^{W_{e_{k}} ⊕B}(z_{ρ})[s].

Therefore the numbers enumerated into B by ρ will not injure the functionals Γ_{α_{j}}.

The outcome a_{k} leaves N_{k} satisfied, not active, and, assuming inductively that all higher-priority N-requirements remain either active forever or satisfied forever along the true path, N_{k} will remain satisfied forever there as well.

The P-node also functions as a gate in the pinball machine, temporarily restraining balls targeted for sets G_{j}. When z_{ρ} is realized at a stage s, the restraint will keep balls < ψ^{G_{i}⊕B}(z_{ρ})[s] from entering G_{i}, thereby protecting the convergence of Ψ^{G_{i}⊕B}(z_{ρ})[s]. (In the finite-win situation, of course, the source nodes for all such balls are initialized when z_{ρ} enters C. If the true path passes through ρˆ ⟨a_{k}⟩, then this restraint becomes arbitrarily large, but drops back to 0 each time we destroy the convergence of Ψ^{G_{i}⊕B}(z_{ρ}).) At other stages, for the sake of Lemma 5.15, we wish to ensure that the only balls which enter the set R = ⊕_{j}G_{j} are balls entering G_{i}, so we restrain balls targeted for sets G_{j} with j ≠ i. Since N_{k} assumes that W_{e_{k}} = Φ^{R}, this restraint will ensure that any change in W_{e_{k}} at these stages can be traced to a change in G_{i}, allowing us to redefine the functional Δ_{ρ,k}^{G_{i}} on the element which entered W_{e_{k}}, as N_{k} requires. These retraints are also set to 0 periodically, at stages s when a change in W_{e_{k}} would allow us to increase the use γ_{α_{k}}^{W_{e_{k}} ⊕B}(z_{ρ})[s + 1] to be > ψ^{G_{i}⊕B}(z_{ρ})[s]. Such a change in W_{e_{k}} would let us move closer to the finitewin situation and would lead to initialization of the node ρˆ ⟨a_{k}⟩, so there is no reason to protect W_{e_{k}} at such stages. Thus no ball will be restrained forever by any P-node on the true path.

This completes our description of the outcomes of nodes on T and the meaning attached to each.

Construction. As in Nies, Shore, and Slaman [1998], each stage s + 1 of the construction consists of (at most) s substages, along with two steps which are executed at the end of every stage. At each substage t < s, only one node ρ ∈ T, of length t, will be eligible to act, and that ρ will then designate at most one of its immediate successors in T to be eligible to act at the following substage. (Alternatively, ρ may refuse to make any of its successors eligible.) The empty node is always eligible to act at substage 0 of any stage. The choice of which nodes are eligible to act corresponds to our approximation at stage s of the true path through T, i.e. the path g such that for each ρ ⊂ g, the successor of ρ along g denotes the ultimate outcome of the strategy played by ρ to satisfy the requirement assigned to it. g(n) will be the leftmost node of length n which is eligible to act at infinitely many stages.

To initialize a strategy means to make all its parameters undefined and all functionals which it constructs completely undefined. At stage 0, we initialize every node. At each subsequent substage we initialize every node which lies to the right of any node eligible to act at that substage. Occasionally the construction will instruct us to initialize other nodes as well, but each node on the actual true path will only be initialized finitely often.

A number is large if it is greater than every other number seen thus far in the construction. By convention, our functionals are built so that, for any fixed oracle, the use function is strictly increasing.

At stage s + 1 and substage t < s, let ρ be the node of T eligible to act at this stage and substage. If we have just completed substage s − 1, or if an eligible node refuses to make any of its successors eligible to act at the next substage, then we proceed to the final steps of the stage, which describes which balls are allowed to move on the pinball machine at that stage. We then terminate the stage.

Let s′′ + 1 be the last stage at which ρ was initialized, and let s′ + 1 be the most recent stage > s′′ +1 at which ρ was eligible to act. (If there has been no such stage since s′′ + 1, we take s′ = s′′.) The action of ρ depends on the type of requirement assigned to it.

If ρ is a D_{i,Ω}-node, we proceed in the style of Friedberg and Muchnik.

1. If no witness element w_{ρ}^{i} is currently defined, then pick a large witness element w_{ρ}^{i} and target it for G_{i}. (Thus, for every gate α ⊂ ρ on the pinball machine, this w_{ρ}^{i} will be greater than the restraint currently maintained by that gate. If ρ is on the true path, then w_{ρ}^{i} will be large enough that every such α will eventually allow w_{ρ}^{i} to pass its gate.) We also choose a large number e_{ρ}^{j}, where j is 0 if i is odd and 1 if i is even, and target it for E_{j}. The ball e_{ρ}^{j} serves as a trace for w_{ρ}^{i}, for the sake of requirement T_{i−1}. We then initialize every requirement ⊋ ρ and end this substage, with no node eligible to act at the next substage.

2. If w_{ρ}^{i} is currently defined but either Ω^{H_{i}}(w_{ρ}^{i})↑ [s] or Ω^{H_{i}}(w_{ρ}^{i})↓≠ 0[s], then continue with the next substage, making ρˆ ⟨w⟩ eligible to act at that substage. (Recall that H_{i} = ⊕_{k≠i} G_{k}. In this case we say that w_{ρ}^{i} has not yet been realized.)

3. If w_{ρ}^{i} is currently defined and Ω^{H_{i}}(w_{ρ}^{i}) ↓= 0[s], we check whether w_{ρ}^{i} is certified at stage s. By definition, w_{ρ}^{i} is certified at stage t if for every node σ ⊂ ρ such that a requirement M_{i′,j,Λ,Υ} is assigned to σ and σˆ ⟨∞⟩ ⊆ ρ, we have w_{ρ}^{i} ∈ dom(Θ_{σ}^{W_{j}})[t′], where t′ + 1 is the greatest σ-expansionary stage ≤ t.

(It is important to note that this definition of certified only applies to balls chosen by D- and M-nodes, not to their traces. Every trace, whether targeted for E_{j} or for a set G_{k}, is automatically certified and enters the pinball machine immediately upon being chosen by Instruction 4.4.)

If w_{ρ}^{i} is not certified at stage s, then we initialize all nodes ⊋ ρ (so they will never injure the computation Ω^{H_{i}}(w_{ρ}^{i})[s]) and terminate this substage, with no node eligible to act at the next substage.

4. If w_{ρ}^{i} is currently defined and certified and Ω^{H_{i}}(w_{ρ}^{i})↓= 0[s], we let w_{ρ}^{i} and e_{ρ}^{i} enter the pinball machine, following Instruction 4.3 below. We then initialize all nodes ⊋ ρ and end this substage, with no node eligible to act at the next substage.

5. If w_{ρ}^{i} has entered the pinball machine, but has not yet entered G_{i}, we end this substage, with no node eligible to act at the next substage.

6. If w_{ρ}^{i} has already been enumerated into G_{i} by stage s, then end this substage, making ρˆ ⟨f⟩ eligible to act at the next substage.

Instruction 4.3 (Entering the Pinball Machine) The gates of the pinball machine are precisely the P-nodes and the U-nodes. If a ball entering the pinball machine at stage s + 1 has subscript ρ, we call ρ the source node for that ball. ρ will be either a D-node or an M-node.

• If there is no gate α ⊂ ρ, then we enumerate e_{ρ}^{j} into E_{j}[s+1] and w_{ρ}^{i} into G_{i}[s+1]. (Notice that every ball which enters the pinball machine, either from a D-node or an M-node, is already certified, hence allowed to enter its target set.)

• If there is a gate α ⊂ ρ, then we drop w_{ρ}^{i} to the greatest such α, and drop e_{ρ}^{j} to the greatest gate σ ⊆ α to which a requirement U_{e,2k+j} is assigned. If there is no such σ, then we enumerate e_{ρ}^{j} into E_{j}[s + 1] and appoint a new trace or traces for w_{ρ}^{i}, following Instruction 4.4.

Instruction 4.4 (Assigning Traces) At stage s + 1, if the ball w_{β}^{i} is waiting at a Pgate, we assign a large trace e_{β}^{0} (if i is odd) or e_{β}^{1} (if i is even). If it is waiting at a U_{e,2k}-gate α, we follow these directions:

• If i is even and i > 0, then we assign a new trace e_{β}^{1}, chosen large and targeted for E_{1}. This ball starts at gate α.

• If i is odd and i ≠ 2k+1, then we assign a new trace w_{β}^{i−1}, chosen large and targeted for G_{i−1}, and this trace is assigned its own trace e_{β}^{1} targeted for E_{1}. Each of these two balls starts at gate α. (Since i − 1 ≠ 2k, this will not threaten the restraint imposed by U_{e,2k}.) The trace w_{β}^{i−1} is immediately considered certified.

• If i = 2k + 1, then the ball w_{β}^{i} is not assigned any traces at this gate. Instead, w_{β}^{i} passes gate α immediately and drops to the greatest gate α′ ⊊ α to which either a P-requirement or a requirement U_{e′,k′} with k′ + 1 ≠ i is assigned. We then follow these same instructions with α′ in place of α. If there is no such node α′, then w_{β}^{i} enters G_{i}[s + 1]. In this case we check whether w_{β}^{i} was a trace for another ball. If so, then we follow these same instructions for that ball at the gate at which it is currently waiting.

• If i = 0, then the ball w_{β}^{i} waits at gate α but is not assigned any traces.

To create traces for a ball w_{β}^{i} waiting at a U_{e,2k+1}-gate α, we follow the analogous directions, with the special case occurring when i = 2k + 2. The ball w_{β}^{i} and the one or two traces defined above together constitute a block, with lead ball w_{β}^{i}. Any previously existing blocks which contained w_{β}^{i} become undefined.

The point of this process is that (barring initialization of α), at any subsequent αstage at which the restraint r at gate α is less than w_{β}^{i}, all the balls in the block will be able to pass gate α simultaneously. For instance, in the case where α is a U_{e,2k+1}-gate, either no ball in the block is targeted for F_{1} (if i is odd) or none of them is targeted for G_{2k+1} ⊕ E_{1} (if i is even and j ≠ 2k + 2). As noted above, the case i = 2k + 2 is an exception, but then the ball w_{β}^{i} is targeted for G_{2k+2}, allowing G_{2k+2} to compute Φ_{e}^{F_{1}}, so U_{e,2k+1} will still be satisfied. Finally, if i = 0 then no T-requirement applies to G_{i}, so no trace is required. Therefore the entire block will be able to drop down to the next gate of the pinball machine simultaneously without violating requirement U_{e,2k+1}. If more than one block of balls is waiting at a gate, we allow the block with highest-priority subscript to pass first; if several blocks have the same subscript, then the one with the largest lead ball goes first, since the larger lead ball will be a trace for the smaller lead ball.

If ρ is an R_{k}-node, we extend the functional Ξ_{ρ} it builds. If s′ = s′′, then Ξ_{ρ}^{G_{k}⊕P} [s′ +1] is empty, and we let y = −1; otherwise we let y = max(dom(Ξ_{ρ}^{G_{k}⊕P}))[s′ + 1]. We check whether there is any x ≤ y such that Ξ_{ρ}^{G_{k}⊕P} (x)[s] does not converge to Q(x)[s]. If there is no such x, we define Ξ_{ρ}^{G_{k}⊕P} (y + 1)[s + 1] = Q(y + 1)[s] with large use. If there is, then for each such x we act as follows:

• If x has entered Q[s] since s′, then it must have done so on behalf of an M-node above ρ, and this node will have enumerated an element into P, allowing us to redefine Ξ_{ρ}^{G_{k}⊕P} (x)[s + 1] = 1. We do so, since now Q(x)[s] = 1, and we leave the use of the computation unchanged.

• If Q(x)[s] = Q(x)[s′], then there must have been a change in G_{k} ⊕ P since stage s′ +1 on the use of the computation Ξ_{ρ}^{G_{k}⊕P} (x)[s′ +1]. Therefore, we simply redefine Ξ_{ρ}^{G_{k}⊕P} (x)[s + 1] = Q(x)[s]. If either x ∈ G_{k}[s] − G_{k}[s′] or x = x_{α} for some M_{i,j,Λ,Υ}- node α ⊃ ρ such that w_{α}^{k} ∈ G_{k}[s] − G_{k}[s′] (as defined below), then we choose the use of this computation to be large. Otherwise, we retain the previous use.

R_{k} has only one outcome, namely ∞, and we end this substage, making ρˆ ⟨∞⟩ eligible to act at the next substage.

If ρ is an M_{i,j,Λ,Υ}-node, then there may be a witness element x_{ρ} already defined, which we will use to try to make Λ^{W_{j}⊕P} ≠ Q. We will also ask whether the stage s + 1 is ρ-expansionary, defined as follows. Let

m(ρ, s) = max{y ≤ s : (∀x < y) Υ_{ρ}^{G_{i}}(x)↓= W_{j}(x)[s]}

l(ρ, s) = max{z ≤ s : (∀x < z) Λ^{W_{j}⊕P} (x)↓= Q(x)[s] with use < m(ρ, s)}.

The stage s + 1 is ρ-expansionary if ρ is eligible to act at s + 1 and l(ρ, s) > l(ρ, t) for every t with s′′ < t < s at which ρ was eligible to act. Thus, we are considering not the actual length of agreement between Λ^{W_{j}⊕P} [s] and Q[s], but rather that portion of the length of agreement which we can guarantee by putting sufficient restraint on W_{j} ⊕P. Of course, we cannot restrain W_{j} directly, but we achieve this purpose by putting restraint on G_{i} and noting that the use of Λ^{W_{j}⊕P} [s] is less than the length of agreement between Υ_{ρ}^{G_{i}}[s] and W_{j}[s]. We define r + 1 to be the greatest ρ-expansionary stage such that s′′ < r < s. (If there has been no such stage, then s′ = s′′, and we set r = s′′.)

1. If x_{ρ} ∈ Q[s], then we end this substage, making ρˆ ⟨f⟩ eligible to act at the next substage. (This preserves any finite win we may have achieved through Substep 6 at a previous stage since s′′.)

2. If s + 1 is not ρ-expansionary and x_{ρ} is not defined, then we end this substage, making ρˆ ⟨w⟩ eligible to act at the next substage.

3. If s + 1 is ρ-expansionary but no witness element x_{ρ} existed at stage r + 1, then we check whether there exists x ∈ dom(Θ_{ρ}^{W_{j}})[r + 1] such that x ∈ G_{i}[s] − G_{i}[r] and W_{j}[s] has not changed on the use θ_{ρ}^{W_{j}}(x)[r] since stage r.

(a) If there is no such x, then we extend dom(Θ_{ρ}^{W_{j}})[s + 1] up to l(ρ, s) − 1 by defining Θ_{ρ}^{W_{j}}(x)[s + 1] = G_{i}(x)[s], with use θ_{ρ}^{W_{j}}(x)[s + 1] = λ^{W_{j}⊕P} (x)[s], for each x for which Θ_{ρ}^{W_{j}}(x)[s] is not already defined. (Possibly this defines Θ_{ρ}^{W_{j}}(x)[s + 1] ≠ Θ_{ρ}^{W_{j}}(x)[r + 1] for certain x, but only if W_{j}[s] has changed on the use of the computation at r.) We make ρˆ ⟨∞⟩ eligible to act at the next substage, and end this substage.

(b) If some x ∈ dom(Θ_{ρ}^{W_{j}})[r + 1] has entered G_{i}[s] since stage r, without any corresponding W_{j}-change as above, we choose x_{ρ} be the least such x. For each k ≠ i such that some β_{k} ⊂ ρ is an R_{k}-node, we set w_{ρ}^{k} = ξ_{β_{k}}^{G_{k}⊕P} (x_{ρ})[s] and assign to it a large trace e_{ρ}^{l} targeted for the set E_{l}, where l = 0 if k is odd and l = 1 if k is even. In order to preserve (W_{j} ⊕ P)↾ λ^{W_{j}⊕P} (x_{ρ})[s], we initialize all nodes above ρ and end this substage, with no successor eligible to act at the next substage.

4. If x_{ρ} is defined and no balls with subscript ρ are currently on the pinball machine, but some ball w_{ρ}^{k} is defined and has not yet entered the machine, then for the least such k, we check whether w_{ρ}^{k} is certified at stage s (using the same definition as for D-nodes, from page 23). If so, then we allow w_{ρ}^{k} and its trace to enter the machine at node ρ, in accordance with Instruction 4.3; if not, we do nothing. In either case we end this substage, with no successor eligible to act at the next substage.

5. If x_{ρ} is defined and some ball w_{ρ}^{k} has entered the pinball machine but is not yet in G_{k}, then we end this substage, with no successor eligible to act at the next substage.

6. If x_{ρ} is defined but not in Q[s], and every ball w_{ρ}^{k} currently defined has entered G_{k}[s], then we enumerate x_{ρ} into Q[s + 1]. For every k such that some β_{k} ⊂ ρ is an R_{k}-node, we enumerate ξ_{β_{k}}^{G_{k}⊕P} (x_{ρ})[s] into P [s + 1]. We initialize every node ⊃ ρ and terminate this substage, with no node eligible to act at the next substage.

(The initializations when x_{ρ} was defined guarantee that either Λ^{W_{j}⊕P} (x_{ρ}) ↓= 0 ≠ Q(x_{ρ})[s] or W_{j} has changed in such a way that W_{j} ≠ Υ^{G_{i}}. Each possibility yields a finite win on requirement M_{i,j,Λ,Υ}. For each k ≠ i, the enumerations of w_{ρ}^{k} into G_{k} guarantee that ξ_{β_{k}}^{G_{k}⊕P} (x_{ρ})[s] has been chosen large since x_{ρ} was defined. Also, before x_{ρ} was chosen as x_{ρ}, it entered G_{i}, and at the next β_{i}-stage t + 1, ξ_{β_{i}}^{G_{i}⊕P} (x_{ρ})[t + 1] was chosen large. Since λ^{W_{j}⊕P} (x_{ρ}) has not changed since before x_{ρ} entered G_{i}, our P -enumerations at this stage do not affect the convergence Λ^{W_{j}⊕P} (x_{ρ})↓= 0[s]. Moreover, now each β_{k} (including k = i) will be allowed to redefine Ξ_{β_{k}}^{G_{i}⊕P} (x_{ρ}) = 1 at the next β_{k}-stage, since now Q(x_{ρ})[s + 1] = 1.)

If ρ is an N_{e,Φ}-node, we define the length of agreement for ρ at this stage by:

l(ρ, s) = max{x : (∀y < x)Φ^{R}(y)↓= W_{e}(y)[s]}.

The stage s + 1 is ρ-expansionary if ρ is eligible to act at s and l(ρ, s) > l(ρ, t) for every t with s′′ < t < s at which ρ is eligible to act.

If s + 1 is not ρ-expansionary, we end this substage, with ρˆ ⟨w⟩ eligible to act at the next substage. Otherwise, for each y < l(ρ, s) for which Γ_{ρ}^{W_{e}⊕B}(y)[s] is undefined, let Γ_{ρ}^{W_{e}⊕B}(y)[s + 1] = C(y)[s]. To define the use γ_{ρ}^{W_{e}⊕B}(y)[s + 1], we ask if any of the following apply:

• γ_{ρ}^{W_{e}⊕B}(y)[s′ + 1] was not defined; or

• γ_{ρ}^{W_{e}⊕B}(z)[s′ + 1] ∈ B[s] for some z ≤ y (which happens if some P-node ⊇ ρˆ ⟨∞⟩ has enumerated it into B in order to allow γ_{ρ}^{W_{e}⊕B}(z)[s′ + 1] to increase); or

• for some z ≤ y, some node ⊇ ρˆ ⟨∞⟩ in T has requested that γ_{ρ}^{W_{e}⊕B}(z)[s′ + 1] be increased.

If so, we choose γ_{ρ}^{W_{e}⊕B}(y)[s + 1] to be large. If none of the conditions applies, then apparently no node above ρ has tried to destroy the functional Γ_{ρ}, so we set γ_{ρ}^{W_{e}⊕B}(y)[s+ 1] = γ_{ρ}^{W_{e}⊕B}(y)[s′ + 1], in order to keep γ_{ρ}^{W_{e}⊕B}(y) from approaching ∞. We then make ρˆ ⟨∞⟩ eligible to act at the next substage, and end this substage.

If ρ is a P_{i,Ψ}-node, we first check if any balls with subscripts ⊃ ρ are presently waiting at any gate below gate ρ. If so, then we end this substage, with no successor eligible to act at the next substage. Otherwise ρ continues to try to satisfy P_{i,Ψ}, and any N-requirement active along ρ may be injured by the action of ρ. Let

K = {k : N_{k} is active along ρ via some α_{k}}.

Define e_{k} and Φ_{k} such that N_{k} = N_{e_{k},Φ_{k}}, and for brevity write Γ_{k} for the function Γ_{α_{k}}^{W_{e_{k}} ⊕B}[s], the current version of the functional being built by α_{k} (k ∈ K), with associated use function γ_{k} = γ_{α_{k}}^{W_{e_{k}} ⊕B}[s]. We will also define a restraint r(ρ, j, k, s + 1) associated to each k ∈ K, denoting the restriction which ρ places on elements targeted for G_{j}. (Restraining G_{j}, coupled with the expansionary outcome of α_{k}, will help ensure that W_{e_{k}} does not change, or else will ensure that if it does change, we can trace the source of the change to some set other than G_{j}.) The restraint finally enforced by ρ on such elements will be

r(ρ, j, s + 1) = max_{k∈K} r(ρ, j, k, s + 1).

(Any restraint r(ρ, j, k, s + 1) which is not mentioned is assumed to retain its value from stage s′ + 1, or is reset to 0 if ρˆ ⟨a_{k}⟩ was initialized at or since stage s′ + 1.)

Subcase 1: If no witness z_{ρ} is presently defined for P_{i,Ψ}, then pick a large number z and designate it as the witness element z_{ρ} for P_{i,Ψ}. Let ρˆ ⟨w⟩ be eligible to act at the next substage, and end this substage.

Subcase 2: If z_{ρ} ∈ C[s], then let ρˆ ⟨f⟩ be eligible to act at the next substage, and end this substage.

Subcase 3: If z_{ρ} ∉ C[s] and ρ enumerated any elements into B at stage s′ + 1 (using Subcase 6(b)), then we set k̃_{s+1} = k̃_{s′+1}, w_{s+1} = w_{s′+1}, and e = ek̃_{s+1} and redefine the same functional Δ_{ρ,k̃_{s+1}} which we extended at that stage (using the notation from Subcase 6(b) below):

Δ_{ρ,k̃_{s+1}}^{G_{i}}↾w_{s+1}[s + 1] = W_{e}↾w_{s+1}[s].

If this involves adding any axioms to Δ_{ρ,k̃_{s+1}}, we choose the use to be large. (Sublemma 5.17 will ensure that our redefinition of Δ_{ρ,k̃_{s+1}} is allowed.) We also set r(ρ, i, k̃_{s+1}, s+1) = φ^{R}(γk̃_{s+1}(z_{ρ}))[s], which (along with the restraints set at stage s′+1) guarantees that αk̃_{s+1} will preserve W_{e}↾ γW_{e}⊕B ; k̃_{s+1}(z_{ρ})[s] until the next ρ-stage. We then end this substage, with ρˆ ⟨ak̃_{s+1}⟩ eligible to act at the next substage. (This is the stage where we complete the business begun in Subcase 6(b) at stage s′ +1. Between s′ +1 and s, any ball targeted for G_{i} can pass gate ρ without injuring the outcome ak̃_{s+1}, since our B-enumeration at stage s′ + 1 already destroyed the convergence of Ψ^{G_{i}⊕B}(z_{ρ})[s′]. Also, this is the only subcase in which ρˆ ⟨ak̃_{s+1}⟩ is made eligible. If ρˆ ⟨a_{k}⟩ is on the true path, then after stage s′′ we will cycle forever from Subcase 4 to 5 to 6 to 3 and back to 4, with k̃_{s+1} = k infinitely often and k̃_{s+1} < k only finitely often, and in Subcases 6(b) and 3 we will build a total function Δ_{ρ,k}^{G_{i}} = W_{e_{k}} to satisfy N_{k}.)

Subcase 4: If z_{ρ} ∉ C[s] and ρ made no B-enumeration at stage s′ + 1 and z_{ρ} is not yet realized (i.e. either Ψ^{G_{i}⊕B}(z_{ρ})[s]↑ or Ψ^{G_{i}⊕B}(z_{ρ})[s]↓≠ 0), then we let ρˆ ⟨w⟩ be eligible to act at the next substage, and end this substage.

Subcase 5: If z_{ρ} ∉ C[s] and Ψ^{G_{i}⊕B}(z_{ρ})[s]↓= 0 and ρ made no B-enumeration at stage s′, then consider each N_{e,Φ}-node β ⊂ ρ (for each e and Φ) such that N_{e,Φ} is not active along ρ via β. Let τ_{β} be the greatest node ⊂ ρ such that N_{e,Φ} is active along τ_{β} via β; there must be such a node τ_{β}, and it must be a P-node. If for some such β we have γ_{β}^{W_{e}⊕B}(z_{τ_{β}})↓≤ ψ^{G_{i}⊕B}(z_{ρ})[s] then we let ρˆ ⟨w⟩ be eligible to act at the next substage, and end this substage.

(If ρ is on the true path, then for each such β the requirement N_{e,Φ} is either satisfied or destroyed at τ_{β}. Hence γ_{β}^{W_{e}⊕B}(z_{τ_{β}}) will eventually be redefined to be > ψ^{G_{i}⊕B}(z_{ρ})[s]. We wait for this to take place, because we do not want to enter Subcase 6 until we are certain that the convergence Ψ^{G_{i}⊕B}(z_{ρ}) ↓= 0 will not be disrupted even if τ_{β} decides to enumerate γ_{β}^{W_{e}⊕B}(z_{τ_{β}}) into B.)

Subcase 6: Otherwise z_{ρ} ∉ C[s] and Ψ^{G_{i}⊕B}(z_{ρ})[s]↓= 0 and ρ made no B-enumeration at stage s′ + 1 and there is no node β as described in Subcase 5. We choose k̃_{s+1} to be the greatest k ∈ K such that

γ_{k}(z_{ρ}) ≤ ψ^{G_{i}⊕B}(z_{ρ})[s].  (1)

If no k satisfies this condition, then let k̃_{s+1} = −1.

If k̃_{s+1} = −1, we enumerate z_{ρ} ∈ C[s+1] (to satisfy P_{i,Ψ}). We enumerate into B[s+1] every number in the set

{γ_{β}^{W_{e}⊕B}(z_{ρ})[s] : β ⊂ ρ & β is an N -node},

in order to allow the corresponding functionals Γ_{β} to change their value on the argument z_{ρ}. To preserve the computation Ψ^{G_{i}⊕B}(z_{ρ}) ↓= 0[s], we initialize every node ≻ ρ. We set all restraints r(ρ, j, k, s + 1) to 0, since no further restraint is necessary after these initializations. Then we end this substage, with no successor eligible to act at the next substage. (Now that we have enumerated z_{ρ} into C, each such β will wait until the next stage at which it is eligible and then adjust Γ_{β} to compute C correctly. Our Benumeration ensures that these changes will be possible.)

If −1 < k̃_{s+1} < k̃_{s′+1} (or if −1 < k̃_{s+1} and k̃_{s′+1} was not defined), we request that the node αk̃_{s+1} increase the use γk̃_{s+1}(z_{ρ}) at the next opportunity, and revoke any corresponding request for αk̃_{s′+1}, since that request must have been fulfilled in order for k̃ to have decreased. We also set

r(ρ, i, k̃_{s+1}, s + 1) = max(ψ^{G_{i}⊕B}(z_{ρ})[s], φ^{R}(γk̃_{s+1}(z_{ρ}))[s]),

and for all j ≠ i we set r(ρ, j, k̃_{s+1}, s + 1) = 0 (since at this stage, balls targeted for G_{j} with j ≠ i may pass node ρ without injuring our strategy for satisfying P_{i,Ψ}). We then end this substage, with no successor eligible to act at the next substage.

Finally, if k̃_{s+1} = k̃_{s′+1} > −1, we write k̃ = k̃_{s+1}, e = ek̃, Φ = Φk̃, σ = ρˆ ⟨ak̃⟩, and γ = γk̃(= γ_{αk̃}^{W_{e}⊕B}) for simplicity, and let t + 1 be the greater of s′′ + 1 and the last stage at which Δ_{ρ,k̃} was extended. We select the appropriate step among the following.

a. If some G_{j} with j ≠ i changed on φ^{R}(γ(z_{ρ}))[s′] between stage s′ and stage s, then we initialize all nodes to the right of σ and end this substage, with no successor eligible to act at the next substage.

b. Otherwise, we let

w_{s+1} = min(γ(z_{ρ}), 1 + dom(Δ_{ρ,k̃}^{G_{i}}))[t + 1]

(here regarding dom(Δ_{ρ,k̃}^{G_{i}})[t + 1], a finite initial segment of ω, as an integer). We define

Δ_{ρ,k̃}^{G_{i}}↾w_{s+1}[s + 1] = W_{e}↾w_{s+1}[s].

If this involves adding any axioms to Δ_{ρ,k̃}, we choose the use to be large. Sublemma 5.17 will ensure that these redefinitions are allowed.

We enumerate γ(z_{ρ})[s′ + 1] into B[s + 1], making Γ_{αk̃}^{W_{e}⊕B}(z_{ρ})[s + 1] undefined, so that αk̃ will increase the use γ(z_{ρ}) at the next αk̃-stage. (Notice that γ(z_{ρ})[s′ + 1] did not already lie in B[s]. Only numbers in the ranges of the γ-functions are ever enumerated into B, and such numbers are always chosen large.) By (1), Ψ^{G_{i}⊕B}(z_{ρ})[s+1] also becomes undefined. We set r(ρ, i, k̃, s+1) = 0 and r(ρ, j, k̃, s+ 1) = φ^{R}(γ(z_{ρ}))[s] for all j ≠ i, to ensure that until the next stage at which z_{ρ} is realized, W_{e}↾w_{s+1} can only change on account of a G_{i}-change, which will allow us to redefine Δ_{ρ,k̃}^{G_{i}} wherever needed. We also revoke our request for αk̃ to increase the use γ_{αk̃}(z_{ρ}). We initialize all nodes to the right of σ and end this substage, with no successor eligible to act at the next substage.

This completes the instruction for P-nodes.

If ρ is a U_{e,i}-node, let m = 0 if i is even and m = 1 if i is odd, and set:

l(ρ, s) = max{x : (∀y < x)Φ_{e}^{G_{i}⊕E_{m}}(y)↓= Φ_{e}^{F_{m}}(y)↓ [s]}.

The stage s + 1 is ρ-expansionary if s = 0 or l(ρ, s) > l(ρ, t) for all stages t + 1 with s′′ < t < s at which ρ was eligible to act. We define r(ρ, s) = 0 if s + 1 is ρ-expansionary, while otherwise r(ρ, s) is the greatest number used in the construction up until the last ρ-expansionary stage. If no ball with a subscript ⊇ ρˆ ⟨p_{r(ρ,s)}⟩ is waiting at any gate ⊊ ρ at stage s, then we make ρˆ ⟨p_{r(ρ,s)}⟩ eligible to act at the next substage, and end this substage. If any such ball is waiting at any gate below ρ, then we initialize all nodes to the right of ρˆ ⟨p_{r(ρ,s)}⟩, but end this substage without making any nodes eligible to act at the next substage.

This completes the instructions for the substages of the stage s + 1. Once we have completed all s substages, or reached a substage at which no new node is made eligible to act at the next substage, we proceed to the final two steps of the stage: satisfying the L-requirements and allowing balls on the pinball machine to drop to lower gates.

First we consider the L-requirements. If L_{k} = L_{Φ,x}, then k is the priority of that requirement. For each α ∈ T, define n(α, s) to be the number of times that α has been initialized (up to stage s) by other nodes on T. (We do not count any initializations by L-requirements themselves in this total.) For the least k ≤ s such that Φ^{R}(x)[s] ↓ and Φ^{R}(x)[s − 1] either diverges or converges with a different use, the requirement L_{k} initializes every α ∈ T satisfying:

⌜α⌝ + n(α, s) > k.

(Here ⌜α⌝ ∈ ω is a code for the node α, with T viewed as a subtree of ω^{<ω}.) This guarantees that none of the α initialized will later injure L_{k}.

Finally, we use a pinball-style approach to determine which ball(s) currently on the pinball machine can pass the gate at which they are currently waiting. Choose the highest-priority α such that there is a gate ρ which was eligible at the current stage s + 1 such that:

• there is a block of balls waiting at ρ, with lead ball w_{α}^{j} or e_{α}^{j}; and

• if ρ is a U-gate, then the lead ball of the block is > r(ρ, s); and

• if ρ is a P-gate, then the lead ball of the block either is of the form e_{α}^{j} or is > r(ρ, j, s + 1); and

• no ball which passed gate ρ at any earlier stage is currently waiting at any gate below ρ.

If there is no such α, then end the stage. If α exists, then the corresponding ρ is unique (by the last condition), and we choose the greatest lead ball with subscript α currently waiting at gate ρ. We allow all balls in its block to pass gate ρ, initialize all nodes ≻ α, and follow Instruction 4.5 below for the balls in the block. Once the balls pass gate ρ, they are no longer in the same block. (For convenience, we usually think of the node α as having performed the initialization of the nodes ≻ α, even though α itself may not have been eligible at this stage.)

Instruction 4.5 (Dropping to a new gate) 1. For each ball e_{α}^{k} which passed gate ρ, we drop e_{α}^{k} to the highest U_{e,2l+k}-gate τ ⊊ ρ (for any l), if such a τ exists. Its block at gate τ consists only of itself.

2. For each ball w_{α}^{k} which passed gate ρ, we drop w_{α}^{k} to the highest gate τ ⊊ ρ, if such a τ exists. For the time being, its block at gate τ consists only of itself, but traces may be added later.

3. If there is no such τ, then we enumerate the ball into its target set (w_{α}^{k} into G_{k}[s+1] or e_{α}^{k} into E_{k}[s + 1]). If this ball was a trace for another ball w_{α}^{j} which does not enter G_{j} at this same stage, then we add new traces for w_{α}^{j} in accordance with Instruction 4.4, to form a new block at the gate at which w_{α}^{j} is currently waiting. (If w_{α}^{j} is waiting at a U_{e,j−1}-gate, this process will involve dropping it to a lower gate or into G_{j}.)

If the ball was not a trace, then it was of the form w_{α}^{k}. Either it was enumerated into G_{k} for the sake of some M_{i,j,Λ,Υ}-node α with i ≠ k, so as to allow an R_{k}- node β ⊂ α to redefine its functional Ξ_{β}^{G_{k}⊕P}, helping α achieve a finite win; or it was a witness element for a D-requirement assigned to α, in which case that D-requirement is now satisfied.

Notice that under these instructions, no ball w_{α}^{j} can end up at a lower gate than its trace.

This completes the construction.

5 Verification of the Construction

To prove that the structure of our tree allows every node to be satisfied, we first need a sublemma.

Sublemma 5.1 At every node ρ on T, if N_{j} is active or satisfied along ρ and i < j, then N_{i} is active or satisfied along ρ also.

Proof. We use induction on the level of the node ρ. Suppose N_{j} is active or satisfied along ρ, and let i < j. Write η = ρ^{−}.

Case 1. Suppose N_{j} was active or satisfied along η. Then by induction so was N_{i}. The only way for N_{i} not to be active or satisfied along ρ is if a P-requirement was assigned to η and ρ = ηˆ ⟨a_{l}⟩, for some l such that N_{l} is active along η via some α along which N_{i} is neither active nor satisfied. Since α ⊊ ρ, the inductive hypothesis ensures that N_{j} was neither active nor satisfied along α either. But then N_{j} cannot be active or satisfied along ρ, contradicting the assumption of the sublemma.

Case 2. Otherwise N_{j} was neither active nor satisfied along η, so in order to become active or satisfied at ρ it must have been assigned to η. Since N_{i} has higher priority than N_{j}, this implies that N_{i} was already active or satisfied at η. But with an N-requirement assigned to η, every requirement active or satisfied at η will still be active or satisfied at ρ, including N_{i}.

Lemma 5.2 For every path h through T and every requirement N_{l}, there exists an N_{l}- node α ⊂ h such that either:

• N_{l} is active via α along every β with α ⊆ β ⊂ h; or

• there exists σ ⊂ h such that N_{l} is active via α along every β with α ⊆ β ⊆ σ, and satisfied via α along every β with σ ⊊ β ⊂ h.

Proof. Fix h, and assume by induction that the lemma holds for every N-requirement of higher priority than N_{l}. This yields a node α_{i} ⊂ h for each i < l, as well as nodes σ_{i} ⊂ h for certain i < l, and we take ξ to be the largest of all these nodes (both α_{i}’s and σ_{i}’s). Then no N_{i} with i < l is assigned to any node on h extending ξ.

Case 1. Suppose first that there exists an N_{l}-node α ⊂ h above ξ. N_{l} must be active or satisfied along the immediate successor of α on h. We argue inductively that N_{l} must be active or satisfied via α along every β ⊃ α on h. Let ρ = β^{−}. Then the only way N_{l} could possibly fail to be active or satisfied at β via α is if a P-requirement is assigned to ρ, and β = ρˆ ⟨a_{m}⟩ for some m such that N_{m} is active along ρ via some η. According to the construction, N_{m} is then satisfied along β, so by the inductive hypothesis on l, we have m > l. But then, in order for N_{m} to have been assigned to η, N_{l} must have been active or satisfied along η. Hence N_{l} remains active or satisfied along β via α, by Definition 4.2.

Case 2. Otherwise N_{l} is not assigned to any node on h above ξ. Then N_{l} must have been assigned to some node below ξ (since otherwise it would eventually be assigned to some node above ξ, as no higher-priority requirement can be assigned to more than one node on h above ξ). So let α be the greatest N_{l}-node ⊆ ξ. If N_{l} were neither active nor satisfied via α along any node on h above α, then a new node on h above α would be chosen as an N_{l}-node, contrary to hypothesis. Thus in both of these two cases, N_{l} is either active or satisfied via the chosen α along every node β with α ⊂ β ⊂ h.

Finally, we note that N_{l} cannot switch from satisfied via α at a node ρ to active at any of its immediate successors β. According to Definition 4.2, if N_{l} is satisfied via α at ρ, then either N_{l} is satisfied via α at β, or β = ρˆ ⟨a_{m}⟩ for some m and N_{l} is neither active nor satisfied at β. Since this does not happen at any β with α ⊂ β ⊂ h, we see that either N_{l} is active via α along every such β, or it is satisfied via α along every such β, or it is active via α along αˆ ⟨∞⟩, switches to satisfied via α along some higher σ ⊂ h, and then stays satisfied via α along all extensions of σ on h. In each of these cases, the lemma holds for N_{l}.

The true path g through T is defined inductively. It begins at the root of T, and for each ρ ⊂ g, we extend g to include the leftmost immediate successor τ of ρ such that τ is eligible to act at infinitely many stages. The existence of such a τ will be shown by induction in Lemma 5.9. To begin this induction, however, we need some sublemmas first.

D- and M-nodes are the only nodes that ever try to enumerate balls into the sets G_{k}. To see that these enumerations do occur, we need the following sublemmas.

Sublemma 5.3 If the ball w_{α}^{i} is ever chosen as x_{σ} by an M-node σ, then σˆ ⟨∞⟩ ⊆ α.

Proof. The node σ has three immediate successors, corresponding to its outcomes f, ∞, and w. To be chosen as x_{σ} at a stage s + 1, w_{α}^{i} must have been enumerated into G_{i} since the last σˆ ⟨∞⟩ stage r + 1. If α ≺ σ, this enumeration would have initialized σ, in which case σ would not have chosen any x_{σ} at s + 1. If σˆ ⟨f⟩ ⊆ α, then α was never eligible until after x_{σ} was selected. If α lies to the right of σˆ ⟨∞⟩, then w_{α}^{i} must have been chosen after the last σˆ ⟨∞⟩-stage, hence could not lie in dom(Θ_{σ}^{W_{j}})[s] and would not have been chosen as x_{σ}. Finally, α ≠ σ, since σ does not target balls for any set G_{k} until it chooses x_{σ}. Hence σˆ ⟨∞⟩ ⊆ α.

The next sublemma will be used extensively throughout the rest of our proofs. It guarantees that balls entering the pinball machine are sufficiently large not to injure any higher-priority requirements.

Sublemma 5.4 Let s′′ + 1 be the greatest stage < s + 1 at which α was initialized, and let t + 1 be the least α-stage > s′′ + 1. If a ball w_{α}^{k} enters the pinball machine at stage s + 1, then w_{α}^{k} is greater than any number used in the construction up to stage t.

Proof. If α is a D-node, then its current witness was chosen at stage t + 1, so w_{α}^{k} was chosen large at some stage ≥ t + 1. If α is an M_{i,j,Λ,Υ}-node, then w_{α}^{k} = ξ_{β}^{G_{k}⊕P} (x_{α})[s′] for some R_{k}-node β ⊂ α and some α-stage s′ + 1 < s + 1, and x_{α} = w_{α′}^{i} for some α′ ⊇ αˆ ⟨∞⟩ (by Sublemma 5.3). If α′ is a D-node, then we are done, since w_{α}^{k} > x_{α} and α′ is initialized every time α is. If not, then we continue by induction. Eventually we must reach a witness or trace for a D-node, since only finitely many nodes have been eligible up to stage s.

Sublemma 5.5 For a D-node α ⊂ g, if w_{α}^{i} is realized at a stage after which α is never again initialized, then eventually w_{α}^{i} will enter G_{i}. For an M-node α ⊂ g, if w_{α}^{i} is a ball targeted for G_{i} by α at a stage after which α is never again initialized, then eventually w_{α}^{i} will enter G_{i}.

Proof. Every M_{i′,j′,Λ,Υ}-node σ with σˆ ⟨∞⟩ ⊂ α has σˆ ⟨∞⟩ ⊂ g. At each σˆ ⟨∞⟩-stage s + 1, the domain of Θ^{W_{j′}} is extended to the new length of agreement l(ρ, s). Hence for each ball w_{α}^{j} (j ≤ i) there exists a stage s + 1 such that w_{α}^{j} is certified at all stages t + 1 ≥ s + 1. So w_{α}^{j} will eventually enter the pinball machine and drop to the highest gate below α, as dictated by Instruction 4.3. (For M-nodes α, this involves an easy induction on j ≤ i. For D-nodes, it only applies with j = i.)

Leaving α and i fixed, we argue by induction, first on gates ρ ⊂ α and then on j ≤ i, that every ball w_{α}^{j} (including traces for other balls) which reaches a gate ρ ⊂ α must eventually pass that gate. This will prove the sublemma.

Suppose w_{α}^{j} is currently waiting at a U-gate ρ and let ρˆ ⟨p_{r}⟩ be the immediate successor of ρ on g. Since α is never again initialized, no ball with subscript ≺ α will ever move again. By induction on ρ, every current trace for w_{α}^{j} at any gate below ρ will eventually enter its target set. (If j = 0, no trace is ever assigned, and similarly for traces targeted for E_{0} or E_{1}.) By Sublemma 5.4, w_{α}^{j} and all its traces must be > r, since ρˆ ⟨p_{r}⟩ ⊂ α. There may be a trace w_{α}^{j−1} for w_{α}^{j} which is also waiting at gate ρ but in a different block from w_{α}^{j}. However, by induction w_{α}^{j−1} eventually passes gate ρ and enters G_{j−1}, with Instruction 4.4 assigning a new trace (or two) to w_{α}^{j}. The new trace(s) lie in the same block as w_{α}^{j}, so after that, the next time ρˆ ⟨p_{r}⟩ is eligible, w_{α}^{j} and its new trace(s) will pass ρ and drop to lower gates, in accordance with Instruction 4.5. Thus, by induction on ρ, w_{α}^{j} will eventually enter G_{j}.

Now suppose w_{α}^{j} has been waiting at a P_{i′,Ψ}-gate ρ since the last σ-stage, where σ ⊆ α is the immediate successor of ρ below α. If σ = ρˆ ⟨f⟩, then there is a stage s_{0} + 1 after which ρ sets all its restraints to 0. We also note that each time a restraint r(ρ, j, k′, s) is changed, all nodes to the right of ρˆ ⟨a_{k′}⟩ are initialized. Hence if σ = ρˆ ⟨w⟩, then no restraint is redefined after the last initialization of σ, so by Sublemma 5.4, w_{α}^{j} is larger than all such restraints and is allowed to pass gate ρ. Finally, if σ = ρˆ ⟨a_{k}⟩, then w_{α}^{j} > r(ρ, j, k′, s + 1) for all s and all k′ < k by Sublemma 5.4, and all restraints r(ρ, j, k′, s + 1) with k′ > k are reset to 0 whenever k̃_{s+1} = k. We know that σ is eligible infinitely often. If i′ = j, then r(ρ, j, k, s + 1) is set to 0 infinitely often in Subcase 6(b) with k̃_{s+1} = k; if not, it is set to 0 each time k̃_{s+1} = k ≠ k̃_{s′+1} in Subcase 6. Thus lim inf_{s} r(ρ, j, s) < w_{α}^{j}. This completes the induction.

Lemma 5.6 Let ρ ⊂ g be an M_{i,j,Λ,Υ}-node such that Υ^{G_{i}} = W_{j} and Λ^{W_{j}⊕P} = Q, and let ρˆ ⟨∞⟩ ⊂ γ. Fix a ball w_{γ}^{i}, chosen by γ at a stage after which ρ is never again initialized. Let s_{0} + 1 be the least ρ-expansionary stage with w_{γ}^{i} ∈ dom(Θ_{ρ}^{W_{j}})[s_{0} + 1], and let s_{1} + 1 be the greatest ρ-expansionary stage before which w_{γ}^{i} has not yet entered the pinball machine. Let s_{2} + 1 be the greatest ρ-expansionary stage < the stage at which w_{γ}^{i} either enters G_{i} or is cancelled, and let s_{3} + 1 be the least ρ-expansionary stage > s_{2} + 1. Then:

1. For every ρ-expansionary stage t + 1 with s_{0} ≤ t < s_{1}, let t′ + 1 be the least ρ-expansionary stage > t + 1. Then we have

P↾l [t] = P↾l [t′],

where l = θ^{W_{j}}(w_{γ}^{i})[t + 1].

2. For every ρ-expansionary stage t + 1 with s_{1} ≤ t < s_{2}, we have

(W_{j} ⊕ P)↾l_{1} [t] = (W_{j} ⊕ P)↾l_{1} [t′],

with t′ as above, and where l_{k} = λ^{W_{j}⊕P} (w_{γ}^{i})[s_{k}] (for k = 1, 2). Hence l_{1} = l_{2}.

3. If w_{γ}^{i} is chosen as x_{ρ} at stage s_{3} + 1, then for every ρ-expansionary stage t + 1 ≥

s_{3} + 1, we have

(W_{j} ⊕ P)↾l_{1} [t] = (W_{j} ⊕ P)↾l_{1} [s_{1}]

with l_{1} as above. Hence Λ^{W_{j}⊕P} (w_{γ}^{i}) = 0.

If w_{γ}^{i} is never cancelled nor ever enters G_{i}, then the items above hold with s_{2} = s_{3} = ∞. If w_{γ}^{i} never enters the pinball machine, they hold with s_{1} = ∞.

In fact we will use this lemma to show that w_{γ}^{i} cannot be chosen as x_{ρ}, so that (assuming Υ^{G_{i}} = W_{j} and Λ^{W_{j}⊕P} = Q) the third item never actually applies.

Proof. For the first item, let t + 1 be a ρ-expansionary stage with s_{0} ≤ t < s_{1}. We will proceed by induction on such t. Only M-nodes enumerate elements into P, so suppose an M_{k,j′,Λ′,Υ′}-node σ enumerates some x into P at a stage s + 1 such that t + 1 is the greatest ρ-expansionary stage ≤ s+1. For this s, the node σ must be unique, since every node ≻ σ is initialized at s + 1. (This also forces γ ⪯ σ, since γ is not initialized before s_{1} + 1.) We wish to show that x > l.

Now the least number enumerated into P by σ at s + 1 is of the form ξ_{β}^{G_{k}⊕P} (x_{σ})[s], for the R_{k}-node β ⊂ σ, and σ also enumerates x_{σ} into Q at stage s + 1. If σ lay to the right of ρˆ ⟨∞⟩, then x_{σ} and its use ξ_{β}^{G_{k}⊕P} (x_{σ})[s] would both have been chosen after stage t+1 (since the ball x_{σ} would have been cancelled at stage t+1, by Sublemma 5.3), hence could not be < l.

So assume ρˆ ⟨∞⟩ ⊆ σ. Now x_{σ} = w_{α}^{k′} for some α ⊃ σ, by Sublemma 5.3, so γ ≺ α. Let w_{α}^{k} be the original ball released by α (so either w_{α}^{k′} = w_{α}^{k}, or w_{α}^{k′} is a trace for w_{α}^{k}, or a trace for a trace for w_{α}^{k}, etc.) Sublemma 5.4 shows that w_{γ}^{i} < w_{α}^{k}. By the construction for Dand M-nodes, w_{α}^{k} did not enter the pinball machine until after the first ρ-expansionary stage t_{0} + 1 ≤ t + 1 with w_{α}^{k} ∈ dom(Θ_{ρ}^{W_{j}})[t_{0}], by which stage w_{γ}^{i} ∈ dom(Θ_{ρ}^{W_{j}})[t_{0}] as well, since at every ρˆ ⟨∞⟩-stage this domain is an initial segment of ω. Thus s_{0} < t_{0}. Let l_{0} = λ^{W_{j}⊕P} (w_{γ}^{i})[t_{0}], and let u_{0} be the use of the computation Υ^{G_{i}}(l_{0})[t_{0}]. Then ξ_{β}^{G_{k}⊕P} (x_{σ})[s] must be > l_{0}, having been chosen large after w_{α}^{k} entered G_{k}, hence after t_{0}.

Now if W_{j}↾ l_{0} has changed between t_{0} + 1 and t, then there must have been a corresponding change in G_{i}↾ u_{0} between those same stages, since t_{0} + 1 and t + 1 are both ρ-expansionary. So some ball w_{α′}^{i} < u_{0} entered G_{i} between t_{0} + 1 and t. Now w_{α′}^{i} must have been chosen by stage t_{0}, by Sublemma 5.4, and so α′ ≺ α, since w_{α′}^{i} was not cancelled at t_{0} + 1. But the entry of w_{α′}^{i} into G_{i} took place after t_{0} + 1, hence after w_{α}^{k} entered G_{k}, since otherwise it would have cancelled w_{α}^{k}.

Now we apply the same argument to w_{α′}^{i} as to w_{α}^{k}. If t′_{0} is the greatest ρ-expansionary stage before w_{α′}^{i} (or the ball for which it was a trace) entered the machine, with corresponding uses l′_{0} and u′_{0}, then w_{γ}^{i} ∈ dom(Θ_{ρ}^{W_{j}})[t′_{0}], and s_{0} < t′_{0} < t_{0}. and so ξ_{β}^{G_{k}⊕P} (x_{σ})[s] > l′_{0}. But any change to W_{j}↾ l′_{0} between t′_{0} and t would require a corresponding change in G_{i}↾ u′_{0} between those same stages, by a ball w_{α′′}^{i} entering G_{i}, and so forth. Since G_{i}[t] is finite, this process must terminate. Thus eventually we find a stage t_{0}^{(n)}, with corresponding l_{0}^{(n)} and u_{0}^{(n)}, for which ξ_{β}^{G_{k}⊕P} (x_{σ})[s] > l_{0}^{(n)} and no change occurred in W_{j}↾ l_{0}^{(n)} between t_{0}^{(n)} + 1 and t. But by the inductive hypothesis on t, P↾ l_{0}^{(n)}[t_{0}^{(n)}] = P↾ l_{0}^{(n)}[t] as well, and so in fact l_{0}^{(n)} = l. Hence ξ_{β}^{G_{k}⊕P} (x_{σ})[s] > l, completing our induction on t.

For the second item, let t + 1 be a ρ-expansionary stage with s_{1} ≤ t < s_{2}. Now all nodes α ≻ γ are initialized at stage s_{1} + 1 when w_{γ}^{i} enters the pinball machine. Hence no such α ever again enumerates any element < l_{1} into P, nor any ball < u_{1} into G_{i}, where u_{1} is the use of the computation Υ^{G_{i}}(l_{1})[s_{1}]. Also, no node ≺ γ could enumerate any ball into G_{i} or any element into P without cancelling w_{γ}^{i}, which would contradict t′ ≤ s_{2}. Finally, γ itself never has two distinct balls on the pinball machine which are both targeted for the same set G_{i}, and γ cannot make any P -enumerations until w_{γ}^{i} has entered G_{i}. For P, this shows that P ↾ l_{1} [t] = P ↾ l_{1} [s_{1}]. For G_{i}, it shows that G_{i}↾u_{1} [t] = G_{i}↾u_{1} [s_{1}], and since t + 1 is ρ-expansionary,

W_{j}↾l_{1} [t] = Υ^{G_{i}}↾l_{1} [t] = Υ^{G_{i}}↾l_{1} [s_{1}] = W_{j}↾l_{1} [s_{1}].

The conclusion that l_{2} = l_{1} is immediate, by induction on t, so this completes the proof of the second item.

For the third item, assuming s_{2} < ∞, we know w_{γ}^{i} ∈ G_{i}[s_{3}]. First we show that P ↾ l_{1} [s_{2}] = P ↾ l_{1} [s_{3}]. Nodes ≻ γ were initialized after s_{1} + 1, hence cannot enumerate elements ≤ l_{1} into P. Among nodes ≺ γ, those ≺ ρ could not enumerate elements into P without initializing ρ, and those ≻ ρ do not enumerate into P at s_{2} + 1 (since this would initialize γ when w_{γ}^{i} has yet to enter G_{i}) and are not eligible after that until s_{3} +1, hence cannot enumerate any elements into P.

Now we induct on ρ-expansionary stages t + 1 ≥ s_{3} + 1. Since w_{γ}^{i} is chosen as x_{ρ} at stage s_{3} + 1, all nodes ⊇ ρˆ ⟨∞⟩ are initialized at s_{3} + 1, and the only nodes above ρ that are ever again eligible are those ⊇ ρˆ ⟨f⟩. These nodes have not been eligible since the last initialization of ρ, so they will never enumerate any elements ≤ l_{3} into P, nor any elements ≤ u_{3} into G_{i}. Since W_{j} = Υ^{G_{i}}, this yields our result for (W_{j} ⊕ P) in the third item.

It is now clear that the final value Λ^{W_{j}⊕P} (w_{γ}^{i}) will be the value Λ^{W_{j}⊕P} (w_{γ}^{i})[s_{2}]. Since w_{γ}^{i} ∉ G_{i}[s_{2}], we must have w_{γ}^{i} ∉ Q[s_{2}]. Since s_{2} + 1 is ρ-expansionary, this forces Λ^{W_{j}⊕P} (w_{γ}^{i})[s_{2}] = 0.

Lemma 5.7 The requirements T_{j} are all satisfied by our construction.

Proof. We show that G_{2i+1} ≤_{T} G_{2i} ⊕ E_{0}, as required by T_{2i}. (The proof for T_{2i+1} is analogous.) To compute whether n ∈ G_{2i+1}, we run the following steps:

1. Check whether n is targeted for G_{2i+1} at or before stage n, either as a witness for some D- or M-requirement or as a trace. If not, halt and conclude that n ∉ G_{2i+1}.

2. If n is targeted for G_{2i+1} by stage n, then when it was so targeted, it must have had a trace appointed. Use the oracle to check whether this trace ever entered G_{2i} ⊕E_{0}. If it never entered them, conclude that n ∉ G_{2i+1}.

3. If the trace did enter G_{2i} ⊕ E_{0}, find the stage s + 1 at which it did so, and check if n ∈ G_{2i+1}[s + 1]. If so, conclude that n ∈ G_{2i+1}. If not, then another trace must have been appointed at stage s. Repeat Step 2 with this new trace.

We claim that this process must eventually terminate with the correct answer. The conclusion in Step 1 is justified by Sublemma 5.4, and the conclusion in Step 3 is abundantly clear. For Step 2, we note that the construction does appoint a trace when n is targeted for G_{2i+1}, and each time such a trace enters its target set, either n itself simultaneously enters G_{2i+1} or another trace is appointed. Furthermore, this new trace becomes part of the same block as n, so they will pass the current gate simultaneously. Hence n must advance by at least one gate down the tree before that trace can enter its target set, which implies that only finitely many traces for n will ever be appointed. (In particular, if n = w_{ρ}^{2i+1}, then after its first trace, it can only have as many traces appointed as there are gates below ρ on T.) Thus the process does eventually terminate.

Finally, notice that at each gate α on the tree, the blocks waiting at gate α are prioritized so that if n and a trace for n lie in different blocks waiting at gate α, then each is the lead ball of its block, and the trace will get to pass the gate first. Hence at every stage until a trace enters its target set, the trace will be waiting at a gate ⊆ the gate at which the ball itself is waiting. Therefore n cannot enter its target set G_{2i+1} unless all its traces have entered their target sets by the same stage. This proves the correctness of our conclusion in Step 2 of the above procedure.

Lemma 5.8 Each requirement L_{Φ,x} is satisfied by our construction, and initializes other nodes at only finitely many stages.

Proof. Let s′′ + 1 be a stage after which no L_{j} with j < k ever initializes any node, and write L_{k} = L_{Φ,x}. If Φ^{R}(x)[s] ↓ with the same use at every s ≥ s′′, or if Φ^{R}(x)[s] ↑ for all such s, then L_{k} is satisfied and never again initializes any nodes. Otherwise, L_{k} initializes cofinitely many nodes at some stage s + 1 ≥ s′′ + 1. Thereafter, none of those nodes will put any number < φ^{R}(x)[s] into R. Among the finitely many remaining nodes α, D- and M-nodes may injure N_{k}, but each of them can put only finitely many numbers into R without being initialized itself. (A witness ball for α drops by at least one gate every time a new trace targeted for R is assigned.) Such an α will not be initialized by any other L-requirement after s′′ + 1, and if other nodes initialize α infinitely often, then eventually n(α, s) becomes so large that L_{k} will initialize α along with everything else. Hence we will reach a stage at which L_{k} initializes every node except those which will never again injure it, and thereafter L_{k} is satisfied and never needs to initialize any more nodes.

Lemma 5.9 The true path g is infinite, and every node on it is initialized only finitely often.

Proof. Suppose the node ρ lies on g. Now ρ may have infinitely many immediate successors, so we must show that one of them will be eligible infinitely often. Since the immediate successors of ρ are well-ordered, there will be a leftmost one τ eligible infinitely often, and that τ will then lie on g.

By induction we assume that ρ is initialized only finitely often by nodes ≺ ρ (and never by nodes ⪰ ρ). Hence n(ρ) = lim_{s} n(ρ, s) exists, and only requirements L_{k} with k < ⌜ρ⌝ + n(ρ) will ever initialize ρ. By Lemma 5.8, therefore, ρ will only be initialized finitely often. Let s′′ + 1 be the last stage at which ρ is initialized. Now we argue that ρ itself initializes its successors only finitely often, and that one of its immediate successors will be eligible infinitely often (so g does not terminate at ρ).

If ρ is an N- or R-node, then ρ has only finitely many immediate successors. Every time ρ acts, one of its successors will be eligible, and such a ρ never initializes any of its successors, so the lemma is clear.

A P_{i,Ψ}-node ρ also has only finitely many immediate successors, but may initialize its successors. We claim that this only happens once after stage s′′ + 1, however. It occurs at only a stage s + 1 such that z_{ρ} has been realized and k̃_{s+1} = −1, and the initialization preserves the computation Ψ^{G_{i}⊕B}(z_{ρ})[s] = 0. Thereafter ρˆ ⟨f⟩ will be eligible whenever ρ is, and no further initialization occurs.

Even if no initializations occur after s′′ + 1, however, there may be infinitely many stages after s′′ + 1 at which ρ is eligible but no immediate successor of ρ is eligible. Such stages occur in Subcase 6 of the construction for ρ. To complete the induction for P-nodes, therefore, we need the following sublemma.

Sublemma 5.10 In this situation, let k be the least number such that N_{k} = N_{e,Φ} is active along ρ via some α and k̃_{s+1} = k at infinitely many ρ-stages s + 1. Then σ = ρˆ ⟨a_{k}⟩ is eligible at infinitely many stages.

Proof. ρˆ ⟨f⟩ can never be eligible after s′′ + 1, or k̃ would never again be defined. By minimality of k, there is a stage s_{0} +1 after which no node to the left of σ is ever eligible. Hence at stages s + 1 > s_{0} + 1, α must never have been able to obey the request from Subcase 6 and increase γ_{α}^{W_{e_{k}} ⊕B}(z_{ρ})[s] on its own. Therefore, the only increases come at stages s + 1 when Subcase 6(b) applies with k̃_{s+1} = k and γ_{α}^{W_{e_{k}} ⊕B}(z_{ρ})[s] is enumerated into B. After each such B-enumeration, σ will be eligible at the next ρ-stage. Hence if σ were eligible only finitely often, then γ_{α}^{W_{e_{k}} ⊕B}(z_{ρ}) would only be redefined finitely often, so would converge to some c. However, since αˆ ⟨∞⟩ ⊂ g, Lemma 5.8 ensures that Φ^{R} is total, so there will exist ρ-stages s + 1 with k̃_{s+1} = k at which R↾ φ^{R}(c)[s] ↓. At such stages we have no G_{j}-change on φ^{R}(c)[s], so we enter Subcase 6(b), and at the next ρ-stage we will be in Subcase 3 and σ will be eligible again, yielding a contradiction.

If ρ is a D_{i,Ω}-node, then ρ initializes all its successors when the witness element w_{ρ}^{i} is defined, again if w_{ρ}^{i} is realized, again at every ρ-stage until w_{ρ}^{i} enters the pinball machine, and again each time any ball with subscript ρ moves down the pinball machine. Once we reach a stage after which ρ is never initialized again, the next witness w_{ρ}^{i} will never be cancelled, and by Sublemma 5.5, if it is realized, then it will eventually enter its target set, after which ρ will never again initialize any of its successors.

Among the immediate successors of ρ, ρˆ ⟨f⟩ will be eligible infinitely often if w_{ρ}^{i} enters G_{i} after the last initialization of ρ. If this w_{ρ}^{i} never enters G_{i}, then by Sublemma 5.5 it must never have been realized, so ρˆ ⟨w⟩ is eligible infinitely often.

An M-node ρ has only finitely many immediate successors, and the only stages > s′′ + 1 at which ρ either fails to make one of them eligible or initializes its successors are those stages s + 1 (if any) at which Substeps 3(b), 4, 5, or 6 of the construction for M-nodes apply. To reach any of these substeps after s′′ + 1, ρ must enter Substep 3(b) first. After that, x_{ρ} is permanently defined. By Sublemma 5.5, ρ can only stay in Substep 4 for finitely many steps for each of the finitely many balls w_{ρ}^{k}, and then can only stay in Substep 5 for finitely many steps for each such ball. Finally ρ spends exactly one ρ-stage in Substep 6, at which x_{ρ} enters Q. Thereafter ρˆ ⟨f⟩ will be eligible (via Substep 1) at every ρ-stage, and ρ will make no further initializations after its one stage in Substep 6. Thus the lemma holds at M-nodes.

Finally, if ρ is a U_{e,i}-node, we let r = lim inf_{s} r(ρ, s) and σ = ρˆ ⟨p_{r}⟩. The existence of this r follows from the definition of r(ρ, s) in the construction: if there are infinitely many ρ-expansionary stages, then r = 0; otherwise r equals the greatest number appearing in the construction at or before the greatest ρ-expansionary stage. Clearly, once we reach a stage s′′ + 1 after which r(ρ, s) ≥ r, ρ will never again initialize any node above σ. We claim that σ ⊂ g.

Now the proof of Sublemma 5.5 actually showed slightly more than was stated:

Sublemma 5.11 Let ρ ⊂ g be a U_{e,2i}-gate, and choose r as above. Any ball w_{α}^{j} > r waiting at gate ρ at a stage s + 1 after which α is never again initialized must eventually enter G_{j}.

From this it follows that there will be infinitely many σ-stages. If not, then eventually all of the (finitely many) balls emanating from above σ which had passed gate ρ would either enter their target sets or be cancelled by initialization of their source nodes. (All such balls are > r by Sublemma 5.4.) At the next stage at which r(ρ, s) = r, σ would then be eligible again. By induction, then, we have established Lemma 5.9.

Lemma 5.12 Every D-, M-, P-, R-, and U-requirement is satisfied by our construction.

Proof. Every one of these requirements is assigned to some unique node on the true path g. (N-requirements, which may be assigned to several nodes, are handled in Lemma 5.16.) We argue by induction along g, proving that the requirement assigned to each ρ ⊂ g is satisfied by the sets we construct. Assume this holds for every σ ⊊ ρ, and let s′′ + 1 be the last stage at which ρ is initialized.

• Suppose ρ is a D_{i,Ω}-node. Once we reach the first ρ-stage > s′′ +1, the construction selects a witness element w_{ρ}^{i} which will remain fixed through all subsequent stages. If this witness element is ever realized, then by Sublemma 5.5 we see that w_{ρ}^{i} ∈ G_{i}, so that D_{i,Ω} is satisfied. If it is never realized, then Ω^{H_{i}}(w_{ρ}^{i}) either diverges or converges to a value ≠ 0. However, in this case w_{ρ}^{i} never enters the pinball machine on behalf of ρ, and it cannot simultaneously be a witness or trace for any other node, since such witnesses are always chosen large (including balls from M-nodes, whose values were originally chosen as the uses of Ξ-functionals). Hence w_{ρ}^{i} ∉ G_{i}, satisfying D_{i,Ω}.

• Suppose ρ is an R_{k}-node. Then at each ρ-stage we either extend the functional Ξ_{ρ} to a larger domain, or add new axioms so as to redefine it on some value x in its current domain. However, the use of Ξ_{ρ}^{G_{k}⊕P} (x) is only changed when x enters G_{k} or when x = x_{α} for some α ⊃ ρ and w_{α}^{k} enters G_{k}. Since each of these can happen only once after Ξ_{ρ}^{G_{k}⊕P} (x − 1) has converged, the function Ξ_{ρ}^{G_{k}⊕P} must be total.

If s′ + 1 < s + 1 are consecutive ρ-stages and a number x enters Q at a stage t with s′ + 1 ≤ t < s + 1, we have x = x_{α} for some M_{i,j,Λ,Υ}-node α ≻ ρ (since if α ≺ ρ, ρ would be initialized). If α lies to the right of ρ, then x_{α} must have been chosen by a node to the right of ρ at a stage > s′ + 1, so x_{α} cannot be in the domain of Ξ_{ρ}^{G_{k}⊕P} [s′ + 1]. Otherwise ρ ⊂ α, and by the construction for M-nodes, α will have enumerated the use ξ_{ρ}^{G_{k}⊕P} (x)[s′ + 1] into P at the same stage that x entered Q. Since s+1 is the first ρ-stage since then, ρ is allowed to redefine Ξ_{ρ}^{G_{k}⊕P} (x)[s+1] = 1. Thus Ξ_{ρ}^{G_{k}⊕P} = Q, satisfying R_{k}.

• Suppose ρ is an M_{i,j,Λ,Υ}-node, and suppose W_{j} = Υ^{G_{i}} and Λ^{W_{j}⊕P} = Q. Then there must be infinitely many ρ-expansionary stages. Now if a witness element x_{ρ} becomes defined at any stage s + 1 > s′′ + 1, then as noted in the construction we have x_{ρ} = w_{γ}^{i} for some γ ⊃ ρˆ ⟨∞⟩ (by Sublemma 5.3), and x_{ρ} must have entered G_{i} by stage s but since the previous ρ-expansionary stage r + 1. At stage s + 1 we enter Substep 3(b) of the construction for ρ, and at the next ρ-stage we enter Substep 4. By Sublemma 5.5, the balls chosen by ρ in Substep 3(b) all eventually enter their target sets, so we eventually enumerate x_{ρ} into Q[t + 1] via Substep 6 at some stage t + 1. However, applying Lemma 5.6 to the ball w_{γ}^{i}, we see that Λ^{W_{j}⊕P} (x_{ρ}) = 0, contradicting the assumption that Λ^{W_{j}⊕P} = Q.

Hence x_{ρ} is never defined. But this means that Θ_{ρ}^{W_{j}} = G_{i} on all elements of ω, since in Step 3(a) of the construction for ρ we define it thus, with the same use as Λ^{W_{j}⊕P}, for all x < l(ρ, s) (and lim_{s} l(ρ, s) = ∞). Moreover, we made sure in that step that any redefinition of Θ was allowed by some W_{j}-change, so Θ is indeed a computable functional. (Had there been no W_{j}-change, we would have defined an element to be x_{ρ} instead.) Thus M_{i,j,Λ,Υ} is satisfied.

• Suppose ρ is a U_{e,2i}-node, and that Φ_{e}^{G_{2i}⊕E_{0}} = Φ_{e}^{F_{0}} with domain ω. (The argument for U_{e,2i+1} is analogous.) Then the node σ = ρˆ ⟨p_{0}⟩ will lie on g.

We make the standard argument for a pinball construction. In the construction, we only allow a block to pass gate ρ if its lead ball is targeted for the infimum (as discussed below) or for E_{1}, or is > r(ρ, s). (A ball is always smaller than its trace. Hence if the lead ball is > r(ρ, s), then the entire block consists of balls > r(ρ, s).) A single block can injure both Φ_{e}^{G_{2i}⊕E_{0}} and Φ_{e}^{F_{0}} only if it contains a ball targeted for the infimum G_{2i+1}. Otherwise, we protect the uninjured side by initializing all nodes of lower priority than the source node of the balls in the block and refusing to allow any other ball to pass the gate until all the balls of the first block have either entered their target sets or disappeared due to initialization of their source nodes, and until the injured computation has recovered and achieved a longer length of agreement with the uninjured computation. (Notice that ρ has the correct guesses about lim inf_{s} r(α, s) for every U-gate α ⊊ ρ and about lim inf_{s} r(α, i, s) for every P-gate α ⊊ ρ and every i, so any ball emanating from a node above ρ is large enough that such an α will eventually allow that ball to pass. Thus no ball which passed gate ρ will have to wait permanently at any gate below ρ, so we know that eventually each block waiting at gate ρ will be allowed to pass.)

In Instruction 4.4, however, we allowed a ball w_{α}^{2i+1} targeted for G_{2i+1} to pass gate ρ at stage s + 1 even if it was ≤ r(ρ, s). (No other instruction allows balls ≤ r(ρ, s) to pass gate ρ, except balls targeted for E_{1}, which will not injure either side of the computation. Also, Instruction 4.4 applies when w_{α}^{2i+1} needs a new trace, so w_{α}^{2i+1} passes gate ρ by itself; its block at stage s + 1 contained no other balls.) Therefore, when we attempt to compute Φ_{e}^{F_{0}}(x), we use a G_{2i+1}-oracle to look for the least σ-stage s_{0} + 1 > s′′ + 1 by which the length of agreement between Φ_{e}^{F_{0}}[s_{0}] and Φ_{e}^{G_{2i}⊕E_{0}}[s_{0}] exceeds x and such that both computations on input x are G_{2i+1}-correct, i.e.

G_{2i+1}↾(u_{0} + 1)[s_{0}] = G_{2i+1}↾(u_{0} + 1),

where u_{0} is the greater of the uses of the two computations Φ_{e}^{G_{2i}⊕E_{0}}(x)[s_{0}] and Φ_{e}^{F_{0}}(x)[s_{0}]. Set h(x) = Φ_{e}^{G_{2i}⊕E_{0}}(x)[s_{0}].

(Such a stage s_{0} must exist. Φ_{e}^{F_{0}}(x) and Φ_{e}^{G_{2i}⊕E_{0}}(x) both converge by some stage s with some use u, and there must be infinitely many σ-stages > s by which G_{2i+1} stabilizes on u. Pick any D_{j,Ω}-node α ⊃ ρ such that α ⊂ g, j ∈ ω, the functional Ω evaluates to 0 on every input and every oracle, and α is never eligible until after G_{2i+1} ↾ u has stabilized. Then α must subsequently enumerate an element into G_{j}. We claim that the least σ-stage s_{0} + 1 > s + 1 by which α has completed its enumerations into all sets G_{j} will satisfy the above conditions. Clearly the length of agreement exceeds x, so we must show that s_{0} is G_{2i+1}-correct. Now α is never initialized again, since otherwise it would have to enumerate another element into G_{j} to get back to the outcome αˆ ⟨f⟩, so no ball from any node ≺ α ever moves after stage s_{0} + 1. Since s_{0} + 1 is a σ-stage, every node to the right of σ = ρˆ ⟨p_{0}⟩ is initialized at stage s_{0} + 1. Nodes ≻ α above σ were initialized when the witness w_{α}^{j} entered G_{j}, and cannot have been eligible since then, because σ has not been eligible since then. Also, no ball from any node ⪯ α can have been below ρ when w_{α}^{j} passed ρ, or can have moved since then. Hence no ball at all is at any gate ⊊ ρ at stage s_{0} + 1, except those which wait there permanently.)

We note that no balls below ρ at stage s_{0} + 1 ever move again. Balls from nodes ≺ ρ cannot move without initializing ρ, which is impossible since s_{0} + 1 > s′′ + 1. Balls from nodes to the right of σ are all cancelled at the σ-stage s_{0} + 1, and in order for s_{0} + 1 also to be a σ-stage, no ball from any node ⊇ σ can be waiting at any node below ρ at stage s_{0} + 1, since otherwise σ would not be eligible at s_{0} + 1.

We argue by induction that at every σ-stage s + 1 > s_{0} + 1, at least one side of the computation is G_{2i+1}-correct – that is, either Φ_{e}^{F_{0}}(x)[s] = h(x) with use u_{s} such that G_{2i+1}↾(u_{s} + 1)[s] = G_{2i+1}↾(u_{s} + 1), or Φ_{e}^{G_{2i}⊕E_{0}}(x)[s] = h(x) with use satisfying the same condition. Assume this holds for all σ-stages t + 1 with s_{0} ≤ t ≤ s′, where s′ + 1 is the last σ-stage before s + 1.

Suppose that Φ_{e}^{F_{0}}(x)[s′] = h(x) is G_{2i+1}-correct with use u_{s′}. (The analogous argument will hold if the other side was G_{2i+1}-correct, as shown below.) The induction is trivial unless some ball ≤ u_{s′} enters F_{0} before stage s + 1, so suppose w = w_{α}^{2k+1} is the first such ball to do so, entering G_{2k+1} at a stage t + 1 with s′ < t ≤ s. Since no ball from any node ≺ ρ ever moves after s′′ + 1, we must have α ⪰ σ. With w ≤ u_{s′}, Sublemma 5.4 ensures that w must have been chosen before stage s′ + 1, and hence σ ⊆ α, since all nodes to the right of σ were initialized at stage s′ +1. Thus w cannot have been below ρ at the σ-stage s′ +1, so w must have passed ρ at a stage t′ + 1 ≥ s′ + 1. By G_{2i+1}-correctness, w was not targeted for the infimum G_{2i+1}, so we must have r(ρ, t′) < w ≤ u_{s′} ≤ s′, and thus r(ρ, t′) = 0. This forces t′ + 1 to be a σ-stage < s + 1, so in fact t′ + 1 = s′ + 1. Notice that due to the instructions for gate ρ, no other ball from above ρ can have been below ρ at stage s′ + 1, or can have passed ρ between stages s′ + 1 and t. Traces may have been chosen for w after it passed ρ, but they would all be chosen > u_{s′}, and will all enter their target sets before w enters G_{2k+1}. After stage t + 1, the restraint r(ρ, ·) will be set to prevent any other ball from above σ from passing gate ρ, until the next time the length of agreement recovers and exceeds l(ρ, s′) – which must be the next σ-stage, namely s + 1. Thus w was the only ball chosen before s′ + 1 to pass gate ρ between stages s′ + 1 and s.

Now we claim that if Φ_{e}^{F_{0}}(x)[s] is no longer G_{2i+1}-correct, then the computation Φ_{e}^{G_{2i}⊕E_{0}}(x)[s] = h(x) is G_{2i+1}-correct. The preceding paragraph shows that no ball entered G_{2i} ⊕ E_{0} between stages s′ + 1 and s, except balls which were chosen large after s′ + 1, so that

Φ_{e}^{G_{2i}⊕E_{0}}(x)[s] = Φ_{e}^{G_{2i}⊕E_{0}}(x)[s′] = Φ_{e}^{F_{0}}(x)[s′] = h(x).

The first two of these computations have the same use u, and we claim that both are G_{2i+1}-correct. Suppose that some ball w_{β}^{2i+1} was chosen before stage s′ + 1 (since any ball chosen after s′ + 1 would be > u) and eventually enters G_{2i+1}. Then w_{β}^{2i+1} was waiting either at gate ρ or at a gate ⊇ σ at stage s′ + 1 (since no ball was waiting below ρ at s′ + 1, balls from the right of σ were initialized then, and balls from nodes ≺ ρ never move again). Also, we have β ⪯ α, since w_{β}^{2i+1} was not cancelled when w_{α}^{2k+1} moved. Hence w_{β}^{2i+1} was chosen before w_{α}^{2k+1} was chosen, and so w_{β}^{2i+1} < w_{α}^{2k+1}. (If β = α, then k < i, since w_{α}^{2k+1} passed gate ρ first. Then w_{α}^{2k+1} would be a trace for w_{β}^{2i+1}, hence larger.) But w_{α}^{2k+1} < u_{s′}, so this would contradict the G_{2i+1}-correctness of the computation Φ_{e}^{F_{0}}(x)[s′], which was the inductive hypothesis.

The analogous argument, assuming Φ_{e}^{G_{2i}⊕E_{0}}(x)[s′] = h(x) to be G_{2i+1}-correct with use u_{s′}, is similar. However, in the second paragraph, when we claim that no ball chosen before s′ + 1 entered F_{0} between s′ + 1 and s, we must worry about balls w_{β}^{2i+1} targeted for the infimum, since such balls could pass ρ at a stage t between s′ + 1 and s despite a large restraint r(ρ, t). The only way for this to happen is under Instruction 4.4, if the trace for w_{β}^{2i+1} entered its target set at stage t+1. This is possible only if that trace was the ball w_{α}^{2i} or e_{α}^{0} which passed ρ at stage s′ + 1, which forces both β = α and w_{β}^{2i+1} < u_{s′}. This contradicts the G_{2i+1}-correctness of the computation Φ_{e}^{G_{2i}⊕E_{0}}(x)[s′], so in fact no such ball w_{β}^{2i+1} can have passed ρ between s′ +1 and s. The rest of the argument goes through essentially unchanged, showing that Φ_{e}^{F_{0}}(x)[s] = h(x) must be G_{2i+1}-correct.

• Suppose ρ is a P_{i,Ψ}-node. Then at the first ρ-stage after s′′ + 1, a witness element z_{ρ} will be chosen and will remain fixed at all subsequent stages. We will need the following two sublemmas for our argument. The first one guarantees that if ρ is in Subcase 5 at infinitely many stages but only reaches Subcase 6 at finitely many stages, then the use ψ^{G_{i}⊕B}(z_{ρ}) → ∞.

Sublemma 5.13 Suppose some α ⊂ g is an N_{k}-node, with N_{k} = N_{e,Φ}, but there is a node σ with α ⊂ σ ⊂ g such that N_{e,Φ} is not active along σ via α. Then for all sufficiently large z, γ_{α}^{W_{e}⊕B}(z)[s] → ∞ as s → ∞. (More specifically, let τ be the immediate predecessor of the least such σ. Then α ⊂ τ, τ is a P-node, and for each z ≥ z_{τ} and each n ∈ ω there exists a stage s_{0} such that at all stages s ≥ s_{0} we have either γ_{α}^{W_{e}⊕B}(z)[s] > n or Γ_{α}^{W_{e}⊕B}(z)[s]↑.)

Proof. N_{k} is active via α along every immediate successor of α, so the τ described must lie above α. The node τ must be a P_{i,Ψ}-node for some i and Ψ, since only at successors of P-nodes can N_{k} change from active via α to inactive via α. If σ ⊇ τˆ ⟨a_{k}⟩, then Subcase 6(b) must apply infinitely often with k̃_{s+1} = k in the construction for τ. Hence γ_{α}^{W_{e}⊕B}(z_{τ})[s + 1] is chosen large at infinitely many stages s + 1, so the sublemma is satisfied for z = z_{τ}. Otherwise σ ⊇ τˆ ⟨a_{l}⟩ for some l < k with N_{l} assigned to some β ⊂ α. In order for this σ to be eligible infinitely often, k must fail Condition (1) from page 29 infinitely often. But γ_{β}^{W_{e_{l}}⊕B}(z_{τ})[s + 1] is chosen large at infinitely many stages s + 1 since τˆ ⟨a_{l}⟩ ⊂ g, and we must have ψ^{G_{i}⊕B}(z_{τ})[s] → ∞ as s → ∞ to allow k̃ = l infinitely often. By Condition (1), therefore, γ_{α}^{W_{e}⊕B}(z_{τ})[s] → ∞ as well.

By convention the use function γ_{α}^{W_{e}⊕B} is increasing, so the result holds for all z ≥ z_{τ}.

Sublemma 5.14 Let s + 1 > s′′ + 1 be a ρ-stage at which the construction for ρ is in Subcase 6. Then (G_{i}⊕B)↾ψ^{G_{i}⊕B}(z_{ρ})[s] will be preserved (and Ψ^{G_{i}⊕B}(z_{ρ})[s]↓= 0) until we enter either Subcase 6(b) or Subcase 2 of the construction for ρ.

Proof. Let t + 1 > s + 1 be a ρ-stage such that ρ has not entered Subcase 2 or 6(b) since stage s + 1. By induction on t, ρ has not entered any of Subcases 1, 3, 4, or 5 since stage s + 1 either. (For Subcase 5, this follows because γ-uses never decrease from one stage to the next.)

For preservation of G_{i}, notice that no ball targeted for G_{i} was below gate ρ at stage s + 1 (except possibly balls from nodes to the left of ρ, and such balls never move again). The construction set r(ρ, i, k̃_{s}, s + 1) ≥ ψ^{G_{i}⊕B}(z_{ρ})[s], ensuring that no ball ≤ ψ^{G_{i}⊕B}(z_{ρ})[s] from above ρ has passed ρ since stage s+1, and all balls from nodes to the right of ρ are cancelled by initialization at s+1. (Balls from nodes ≺ ρ never move again, since ρ is never initialized again.)

Now a node must be eligible in order to enumerate an element into B. Hence no node to the left of ρ nor any node above ρ will violate our B-preservation, since nodes above ρ are never eligible when ρ is in Subcase 6. Each node σ to the right of ρ is initialized at s + 1, so any element which σ enumerates into B at stage t + 1 will be of the form γ_{α}^{W_{e}⊕B}(z_{σ})[t], hence > z_{σ}[t] > ψ^{G_{i}⊕B}(z_{ρ})[s]. A node τ ⊂ ρ never again enumerates anything into C (since doing so would initialize ρ), so its only B-enumeration can come when τ is in Subcase 6(b). Assume τˆ ⟨a_{k}⟩ ⊂ ρ, and suppose that at stage t + 1, τ enumerates some element γ_{α}^{W_{e}⊕B}(z_{τ})[t] into B, with N_{l} = N_{e,Φ} assigned to α ⊂ τ. Then k ≤ l, since otherwise ρ would be initialized at this stage, so N_{l} is not active via α along ρ, and τ is precisely the node τ_{α} described in Subcase 5. But then γ_{α}^{W_{e}⊕B}(z_{τ}) > ψ^{G_{i}⊕B}(z_{ρ})[t], since we are not in Subcase 5. Thus the B-enumeration by τ at stage t + 1 does not violate the sublemma.

If ρˆ ⟨f⟩ ever becomes eligible at some stage s + 1 > s′′ + 1, then our initializations when z_{ρ} entered C will preserve the convergence Ψ^{G_{i}⊕B}(z_{ρ})[s]↓= 0 ≠ C(z_{ρ}) forever after, satisfying P_{i,Ψ}. (The same argument as in Sublemma 5.14 shows that no τ ≺ ρ will injure this computation by any subsequent B-enumeration.)

If ρˆ ⟨w⟩ ⊂ g, then either Subcase 4 holds infinitely often (so Ψ^{G_{i}⊕B}(z_{ρ}) ↓≠ 0 or diverges) or Subcase 5 holds infinitely often (so Ψ^{G_{i}⊕B}(z_{ρ}) ↑, by Sublemma 5.13 and the conditions of Subcase 5). Sublemma 5.13 excludes the possibility of our remaining in Subcase 5 without eventually entering Subcases 2 or 3, both of which give outcomes to the left of ρˆ ⟨w⟩ ⊂ g.) Moreover, z_{ρ} never enters C, so P_{i,Ψ} holds.

Otherwise, z_{ρ} is realized infinitely often, and Sublemma 5.13 guarantees that each time it is realized, we will eventually enter Subcase 6 of the construction for ρ. If k̃ = −1 at any subsequent ρ-stage, ρ will enumerate z_{ρ} into C, and ρˆ ⟨f⟩ becomes eligible, as described above. Otherwise there is some k such that N_{k} = N_{e,Φ} is active along ρ via some α and σ = ρˆ ⟨a_{k}⟩ ⊂ g. Let s_{0} + 1 < s_{1} + 1 < ⋯ be all the σ-stages occurring after the last initialization of ρ. We claim that P_{i,Ψ} holds because in this case Ψ^{G_{i}⊕B}(z_{ρ}) must diverge. At each stage s_{n}+1, we are in Subcase 3 of the construction for the node ρ, so we have been in Subcase 6(b) at some stage t + 1 > s_{n−1} + 1. At that stage t + 1, we enumerated γ_{k}^{W_{e}⊕B}(z_{ρ})[t] into B, and at the next α-stage s+1, γ_{k}^{W_{e}⊕B}(z_{ρ})[s+1] was chosen large. Since k̃_{s_{n}+1} = k, we know γ_{k}^{W_{e}⊕B}(z_{ρ}) ≤ ψ^{G_{i}⊕B}(z_{ρ})[s_{n}], so ψ^{G_{i}⊕B}(z_{ρ})[s_{n}] → ∞ as n → ∞, satisfying P_{i,Ψ}.

This completes the proof of Lemma 5.12.

The following lemma ensures that the functionals Δ_{ρ,k} built at P-nodes ρ with ρˆ ⟨a_{k}⟩ ⊂ g are indeed computable.

Lemma 5.15 (Δ-Correction Lemma) Let ρ be a P_{i,Ψ}-node, and let σ = ρˆ ⟨a_{k}⟩ lie on the true path g through T, with N_{k} = N_{e,Φ}. Then there is an s_{0} such that for every w ∈ ω and every σ-stage s + 1 ≥ s_{0} + 1 such that w ∈ dom(Δ_{ρ,k}^{G_{i}})[s + 1], no ball w_{β}^{i} with δ_{ρ,k}^{G_{i}}(w)[s + 1] < w_{β}^{i} < φ^{R}(w)[s] enters G_{i} from stage s + 1 until the next σ-stage.

Proof. Since a_{k} is an outcome of the node ρ, the requirement N_{k} must be active along ρ via some node τ ⊊ ρ. Now dom(Δ_{ρ,k}^{G_{i}}) ⊆ dom(Φ^{R})[t] at every stage t, since Δ_{ρ,k} is extended only at ρ-stages, all of which are τ-expansionary. Let s_{0} + 1 be the last stage at which σ is initialized, so that no ball with subscript ≺ σ ever moves after stage s_{0} + 1. Let s_{1} + 1 be the first σ-stage > s_{0} + 1 at which Δ_{ρ,k}^{G_{i}}(w)[s_{1} + 1] is defined. Then the use δ_{ρ,k}^{G_{i}}(w)[s_{1} + 1] is chosen large, hence is greater than φ^{R}(w)[s_{1}].

We argue by induction on σ-stages s+1 that no ball w_{α}^{i} with δ_{ρ,k}^{G_{i}}(w) < w_{α}^{i} < φ^{R}(w)[s] and σ ⪯ α even exists at any σ-stage ≥ s_{1} +1. (By the above remarks, this holds at stage s_{1} + 1.) Since no ball with subscript ≺ σ moves after stage s_{0} + 1 and no ball defined after a σ-stage s + 1 can be < φ^{R}(w)[s], this will prove the lemma.

For the inductive step, let s + 1 > s′ + 1 be consecutive σ-stages ≥ s_{1} + 1, and fix α ⪰ σ. Now any new witness or trace chosen at an intervening stage must be greater than φ^{R}(w)[s′], so the induction will be trivial unless φ^{R}(w)[s] > φ^{R}(w)[s′]. This implies that some element y < φ^{R}(w)[s′] entered R after stage s′. (Recall that R = ⊕_{k}G_{k}.) Then y must have been appointed as a witness or trace before stage s′ + 1, by some node β ⊇ σ.

If y entered G_{i}, then by our induction on s′ + 1, we have y ≤ δ_{ρ,k}^{G_{i}}(w)[s′ + 1] as well, so at stage s + 1 we redefine Δ_{ρ,k}^{G_{i}}(w) and set δ_{ρ,k}^{G_{i}}(w)[s + 1] > φ^{R}(w)[s], completing the induction for s + 1.

Otherwise y = w_{β}^{j} entered G_{j} for some j ≠ i. If α ≻ β on T, then α was initialized when y entered G_{j} and is not eligible again before stage s + 1, so any new ball with subscript α at stage s + 1 will be greater than φ^{R}(w)[s], by Sublemma 5.4.

If α ≺ β, then no ball y′ with subscript α has moved or been chosen since w_{β}^{j} was chosen (since otherwise β would have been initialized). Sublemma 5.4 then ensures that such a y′ is < w_{β}^{j}, hence < φ^{R}(w)[s′], and the inductive hypothesis guarantees that either y′ < δ_{ρ,k}^{G_{i}}(w)[s′ + 1] or y′ is targeted for a set other than G_{i}.

Finally we consider the case α = β. Since w_{β}^{j} entered G_{j} after stage s′, it must have passed gate ρ at a stage > s′, since otherwise σ could not have been eligible at s′ + 1. When w_{β}^{j} passed gate ρ, all its traces either had already entered their target sets or were targeted for E_{0} or E_{1}. Moreover, if w_{β}^{j} was a trace for another ball w_{β}^{j+1}, then w_{β}^{j+1} must have been waiting at a gate ⊇ σ at stage s′ + 1. (Two balls targeted for R cannot pass a P-gate simultaneously.) The ball w_{β}^{j+1} may have dropped as far as gate ρ when w_{β}^{j} entered G_{j}, but the construction does not allow it to pass ρ until the next σ-stage s + 1. When w_{β}^{j} entered G_{j}, a new trace (or traces) was appointed for w_{β}^{j+1}, but these new traces will each be targeted for either E_{0}, E_{1}, or G_{j}, not for G_{i}, and will begin at the same gate at which w_{β}^{j+1} is currently waiting. Hence none of these traces will move until stage s + 1, so no new trace will be targeted for G_{i} until at least stage s + 1. This proves our claim, and the lemma follows.

Lemma 5.16 Every requirement N_{k} = N_{e,Φ} is satisfied by our construction.

Proof. Let g be the true path, and let α be the node described by Lemma 5.2 for N_{k}. If αˆ ⟨w⟩ ⊂ g, then W_{e} ≠ Φ^{R}, so N_{k} holds. Otherwise we have two cases.

Case 1: There exists a P_{i,Ψ}-node ρ ⊃ α, for some i and Ψ such that σ = ρˆ ⟨a_{k}⟩ ⊂ g. By the construction and our choice of α, N_{k} must be satisfied via α along every node ⊇ σ on g. Once we have reached a stage s′′ + 1 after which σ is never again initialized, Subcase 6(b) guarantees that the domain of the function Δ_{ρ,k}^{G_{i}} built by ρ will be extended by at least one element between every pair of σ-stages, subject only to the restriction that every element in the domain at stage s + 1 must be < γ_{k}^{W_{e}⊕B}(z_{ρ})[s + 1]. As noted in the proof of satisfaction of P_{i,Ψ} above, γ_{k}^{W_{e}⊕B}(z_{ρ})[s] → ∞ as s → ∞, so for each n ∈ ω, Δ_{ρ,k}^{G_{i}}(n)[s + 1] is defined at infinitely many stages s + 1. The L-requirements will then ensure that Δ_{ρ,k}^{G_{i}} is total, so that W_{e} ≤_{T} G_{i}, given the following.

Sublemma 5.17 In the situation above, Δ_{ρ,k} is a computable functional, with Δ_{ρ,k}^{G_{i}} = W_{e}.

Proof. In Subcases 3 and 6(b) we always redefine Δ_{ρ,k}^{G_{i}} to equal W_{e} on its domain. We must prove that Δ_{ρ,k} is computable, i.e. that these redefinitions are allowed.

If the construction is in Subcase 3 at the ρ-stage s + 1, let s′ + 1 be the most recent ρ-stage (at which we must have been in Subcase 6(b)). If any y < w_{s′+1} has entered W_{e} since stage s′+1, then some change in φ^{R}(y) must have taken place since s′+1 to allow it, where Φ is the functional assigned to N_{k}. With the restraints r(ρ, j, k, s′ + 1) ≥ φ^{R}(y)[s′] for all j ≠ i, this means that G_{i}↾φ^{R}(y)[s′] has changed since s′. Indeed, by Lemma 5.15, G_{i}↾δ_{ρ,k}^{G_{i}}(y)[s′] must have changed, so our redefinition of Δ_{ρ,k}^{G_{i}}(y)[s + 1] is allowed.

In Subcase 6(b) at stage s + 1, if some y < w_{s+1} ≤ γ_{k}^{W_{e}⊕B}(z_{ρ})[t + 1] has entered W_{e} since the last stage t + 1 at which we were in Subcase 3 with k̃_{t+1} = k, then y must have been allowed to enter W_{e} by some change in R↾ φ^{R}(y)[t]. Now we set r(ρ, i, k, t + 1) = φ^{R}(γ_{k}(z_{ρ}))[t], and this restraint has stayed at least that large at all subsequent stages up through s + 1. Hence some G_{j} ↾ φ^{R}(z_{ρ})[t] with j ≠ i must have changed after z_{ρ} was realized. However, the change would have happened before the previous ρ-stage s′ + 1 (since otherwise we would be in Subcase 6(a) at stage s + 1) and after the stage t′+1 > t+1 at which we re-entered Subcase 6 with k̃_{t′+1} = k and reset r(ρ, j, k, t′+1) = 0. However, at stage t′ + 1 we also requested that α = α_{k} increase γ_{α}^{W_{e}⊕B}(z_{ρ})[t′]. Hence by stage s + 1, α would have recognized the W_{e}-change and obeyed our request, setting γ_{α}^{W_{e}⊕B}(z_{ρ})[s+1] > ψ^{G_{i}⊕B}(z_{ρ})[s]. This would contradict Condition (1), since our restraints have preserved ψ^{G_{i}⊕B}(z_{ρ})[t′] since we entered Subcase 6. Thus no such G_{j}-changes can have taken place, so W_{e} has not changed, and Subcase 6(b) only extends the domain of the functional Δ_{ρ,k} without redefining it on any arguments.

Case 2: By Lemma 5.2, if Case 1 does not hold, then N_{k} is active via α along every node on g above α. Then at every α-expansionary stage we extend the domain of Γ_{α}^{W_{e}⊕B} by another element. Once the use γ_{α}^{W_{e}⊕B}(x−1) stabilizes, γ_{α}^{W_{e}⊕B}(x) increases only when:

• x enters C; or

• x = z_{ρ} for some eligible ρ ⊃ α at which N_{k} is satisfied; or

• x = z_{ρ} for some eligible ρ ⊃ α at a stage at which k̃ = k in the construction at ρ.

In the second case, ρ cannot lie on g, so either ρ is eligible only finitely often or z_{ρ} is eventually cancelled by initialization and redefined to be > x. In the third case, if ρ ⊂ g, then there are only finitely many such stages. Hence the use will increase only finitely often, and Γ_{α}^{W_{e}⊕B} is total.

It only remains to show that this function computes C correctly – which is clear for any argument x ∉ C. Now no node ≺ α ever enumerates any element into C without initializing α, and after each initialization we start building a new Γ_{α}, so the version of Γ_{α} constructed after the last initialization of α will never be injured by those nodes. Among nodes ρ ≻ α, only P-nodes ever enumerate any elements into C. When such a ρ does so, the element is the witness z_{ρ}, and it enters C at a stage s + 1 with k̃_{s+1} = −1 in the construction for that ρ.

If ρ lies to the right of α, then z_{ρ} is cancelled each time α is eligible. If such a z_{ρ} is enumerated into C, therefore, then there were no α-stages between the definition of z_{ρ} at some stage s + 1 and its entry into C. Since z_{ρ} was chosen large, it cannot have been in the domain of Γ_{α}^{W_{e}⊕B}[s], nor can it have entered that domain since stage s + 1. When Γ_{α}^{W_{e}⊕B}(z_{ρ}) is finally defined, therefore, it will be correct.

So suppose α lies below the P_{i,Ψ}-node ρ, and ρ enumerates z_{ρ} into C at stage s + 1 (using Subcase 6 of the construction for ρ). Since k̃_{s+1} = −1 and Subcase 5 did not apply, either γ_{α}^{W_{e}⊕B}(z_{ρ})[s]↑ or γ_{α}^{W_{e}⊕B}(z_{ρ}) > ψ^{G_{i}⊕B}(z_{ρ})[s]. In the latter case ρ enumerates γ_{α}^{W_{e}⊕B}(z_{ρ})[s] into B[s+1]. In either case, therefore, α will be able to define Γ_{α}^{W_{e}⊕B}(z_{ρ})[t+1] correctly at the next α-stage t + 1. Hence Γ_{α}^{W_{e}⊕B} = C, satisfying N_{k}.

6 References

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.

Calhoun, W. C. [1993], Incomparable prime ideals of recursively enumerable degrees., 9th International Congress of Logic, Methodology and Philosophy of Science (Uppsala, 1991). Ann. Pure Appl. Logic 63, 39–56.

Calhoun, W. C. and Lerman, M. [2001], Embedding finite lattices into the ideals of computably enumerable Turing degrees. J. Symbolic Logic 66, 1791–1802.

Dreben, B. and Goldfarb, W. [1979], The decision problem, Solvable Classes of Quantificational Formulas, Addison-Wesley, Reading MA.

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.

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

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

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

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

Lachlan, A. H. [1975], A recursively enumerable degree which will not split over all lesser ones, Ann. Math. Logic 9, 307-365.

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. of Math. (2) 93, 365-389.

Lerman, M. [1973], Admissible ordinals and priority arguments, in Cambridge Summer School in Mathematical Logic, LNM 337, A. R. D. Mathias and H. Rogers jr. eds., Springer-Verlag, Berlin, 311-344.

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

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, Advances in Mathematics 53, 301-320.

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.

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.

Nies, A. [2003], Parameter definability in the recursively enumerable degrees, to appear in Journal of Mathematical Logic.

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.

Ramsey, F. P. [1930], On a problem of formal logic, Proc. Lond. 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. of 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′, Journal of the London Mathematical Society 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.

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, Annals of Mathematics, 153, 1-43.

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. Yates, C. E. M. [1966], On the degrees of index sets, Trans. Am. Math. Soc. 121,

309-328.