Biinterpretability up to double jump in the degrees below 0′

Richard A. Shore^{∗} Department of Mathematics Cornell University Ithaca NY 14853

July 29, 2013

Abstract

We prove that, for every z ≤ 0′ with z′′ > 0′′ (i.e. z ∈ L̄_{2}), the structure D(≤ z) of the Turing degrees below x is biinterpretable with first order arithmetic up to double jump. As a corollary, every relation on D(≤ z) which is invariant under double jump is definable in D(≤ z) if and only if it is definable in arithmetic.

1 Introduction

A major issue in the analysis of relative complexity of computation over the past few decades has been the determination of the complexity of various structures that capture some reducibility, i.e. a notion of relative computability, and a class of sets (A ⊆ ℕ) (or equivalently functions f : ℕ → ℕ) whose relative complexities are to be compared. The basic notion of relative complexity is that of Turing. We say that A ≤_{T} B if there is a Turing machine Φ_{e}, equipped with an oracle for B, i.e. access to membership information about B, which can compute membership in A. The trend has been to show that such structures are as complicated as possible: first, in the sense that their theories are as complicated as possible given the definability of the structure itself in some (often second order) version of arithmetic; second, in the sense that the class of relations on the structures definable in them is as rich as possible.

Considering only Turing reducibility, the class of sets to consider first is that of all subsets of ℕ. As usual, we move to the equivalence classes under ≤_{T}, i.e. the (Turing) degrees), to define the basic structure D of these degrees under the induced relation ≤_{T}. Then one considers important or natural substructures of D. The most prominent of these are the recursively enumerable degrees (those of sets with effective enumerations), R, the degrees of sets recursive in the halting problem, D(≤ 0′) and the degrees of sets definable in (first order) arithmetic, A. These last degrees are closed under relativizations of the halting problem, i.e. the (Turing) jump sending A to A′ (the halting problem for machines with oracle A). From basic facts connecting definability in arithmetic to the jump operator, it follows that A is the least ideal in D closed under the jump. (D is an uppersemilattice, so an ideal in D is a downward closed subset closed under join.) Also of interest, then, are the other ideals closed under the jump.

∗Partially supported by NSF Grants DMS-0852811 and DMS-1161175 and as a Visiting Professor in the Department of Mathematics and the Institute for Mathematical Sciences at the National University of Singapore with partial funding from the John Templeton Foundation.

The complexity of the theories of all of these structures are known to be as high as possible. They are each easily seen to be (recursively) interpretable in the version of second order arithmetic with quantification over sets with degrees in the specified structures. Thus their theories are reducible (even by a one-one function) to those of the corresponding structure for arithmetic. One then proves a converse that each such structure of arithmetic is interpretable in the associated degree structure. Thus the theory of each degree structure is recursively equivalent to that of the corresponding structure of arithmetic. (These results are due to Simpson [1977] for D, Harrington and Slaman and Slaman and Woodin (see Nies, Shore and Slaman [1998]) for R, Shore [1981] for D(≤ 0′) and Nerode and Shore [1980] for all ideals closed under jump.) By their interpretability in (some version of) arithmetic, the most one could hope for in terms of definability in these degree structures would be that all relations invariant under Turing degree and definable in the corresponding structure for arithmetic are definable in the degree structure. To date, the best general results have been that relations invariant under double jump definable in each structure of arithmetic are definable in the associated degree structure. The known results are due to Slaman and Woodin (see Slaman [1991] and [2008]) for D, Nies, Shore and Slaman [1998] for R and Shore [2007] for ideals closed under jump which also contain 0^{(ω)}, the effective join of the 0^{(n)}, the finite iterations of the jump. Possible routes to this result for D(≤ 0′) are outlined in Shore [1988] and more concretely in Nies, Shore and Slaman [1998] but a crucial ingredient is missing from these sketches (comparison maps between models as explained below). We supply this missing ingredient and so prove the result for D(≤ 0′). Indeed by making use of some more recent general results on constructing 1-generics for various notions of forcing below degrees z in \overline{GL}_{2} (z′′ > (z ∨ 0′)′) from Cai and Shore [2012] applied to the analysis of 1-genericity for two specific such types of forcing in Greenberg and Montalbán [2004], we simultaneously prove the same results for D(≤ z) for any z ≤ 0′ with z′′ > 0′′. The corresponding question for A is an important open problem whose solution should lead to other interesting theorems.

Such results on definability are now generally approached through the stronger notions of biinterpretability and biinterpretability up to double jump due to Harrington for the r.e. degrees and Slaman and Woodin for other structures (see Slaman [1991] and [2008]). We define these notions in §2. There also supply statements of, and references for, the somewhat scattered results we need about coding arithmetic into degree structures and forcing in arithmetic. More details and some proofs can be found in our lecture notes Shore [2013]. Our main theorem on biinterpretability up to double jump (Theorem 3.4) is proven in §3. The major consequence is Theorem 3.5 that, for z ≤ 0′ with z′′ > 0′′, a relation on D(≤z) which is invariant under the double jump is definable in D(≤z) if and only if it is definable in true first order arithmetic.

2 Background Information

We begin our path to coding arithmetic into D(≤ z) (or any degree structure S) with a specific highly effective form of coding orderings of type ω called nice effective successor structures introduced in Shore [1981]. They have been used as well in Nies, Shore and Slaman [1998] and Shore [2007] which contains (in §3) a good presentation. For our purposes all we need to know is that the scheme provides a way of coding a sequence ⟨d_{n}⟩ of independent degrees (i.e. no d_{n} is below the join of the rest of the degrees d_{m}) by finitely many parameters q̄ which generate a partial lattice including the d_{n}. We assume that the first element q̄_{0} of q̄ is a bound on all the other elements needed to determine this partial lattice. The crucial property of this coding is the following:

Proposition 2.1. Given a q̄ determining a nice effective successor structure, the set of indices, relative to Q_{0} ∈ q̄_{0}, for the degrees in the ideal generated by the d_{n} is Σ_{3}^{Q_{0}} and any set S such that S = {n|d_{n} ≤ g_{0}, g_{1}} for any g_{0}, g_{1} ≤ q_{0} is also Σ_{3}^{Q_{0}}. We say that the set S is coded (with respect to the structure determined by q̄) by the degrees g_{0} and g_{1}. Moreover, for every S ∈ Σ_{3}^{X} with Q_{0} ≤_{T} X, the set of indices relative to X, for the ideal generated by {d_{n}|n ∈ S} is Σ_{3}^{X}.

We next want to extend the sequence of parameters q̄ to one p̄ such that there are formulas with parameters p̄ providing an interpretation of arithmetic on the domain consisting of the d_{n} given by q̄ that identifies d_{n} with the nth element of this model, M(p̄). (See Hodges [1993] for a general explanation of interpretations of one structure in another.) For our purposes, we just need formulas φ_{D}(x), φ_{+}(x, y, z), φ_{×}(x, y, z), φ_{<}(x, y) all with parameters p̄ and an additional one φ_{c}(p̄) called a correctness condition that asserts at least that, for any p̄, the structure M(p̄) with domain D(p̄) = {x ∈ S|S ⊨ φ_{D}(x)} and relations +, × and < defined by φ_{+}(x, y, z), φ_{×}(x, y, z), φ_{<}(x, y), respectively, is a model of some standard finite axiomatization of arithmetic and that the d_{n} form an initial segment of its domain. Providing the translation of the axioms of arithmetic is a general fact about interpretations as is saying that d_{0} is the 0 of the structure. Saying that the d_{n} form an initial segment is phrased by using the definition of the way d_{n+1} is generated (in terms of ∨ and ∧) from the degrees in q̄. We also want to add a condition to φ_{c} that, in the degree structures we study, will guarantee that the models M(p̄) for which p̄ satisfies it are all standard. As we code sets S in such models by exact pairs g_{0}, g_{1} for the ideal generated by {d_{n}|n ∈ S}, we can translate the sentence x ∈ S into arithmetic in M(p̄) by φ_{D}(x) & x ≤ g_{0}, g_{1}. (Degrees g_{0} and g_{1} are an exact pair for an ideal I if I = {x|x ≤ g_{0}, g_{1}}. Note also that by the independence of the d_{n} the ideal generated by {d_{n}|n ∈ S} contains no d_{m} for m ∉ S.) We write this as φ_{S}(x, ḡ, p̄). To say that M(p̄) is standard, it suffices to say that every nonempty bounded subset of its domain as coded by a pair g_{0}, g_{1} has a greatest element as long as the set {d_{n}|n ∈ ℕ} is so coded. To this end, we want a theorem that guarantees the existence of exact pairs for the ideals generated by Σ_{3}^{Q_{0}} sets of indices. We give one which follows from Shore [1981] where it is proved for a r.e. in b and Ambos-Spies et al. [2009] or Cai and Shore [2012] where it is proven that, even for a ∈ \overline{GL}_{2}(b), there is an â ∈ [b, a) with a r.e. in â.

Theorem 2.2. If b <_{T} a and a ∈ L̄_{2}(b) and I is a Σ_{3}^{B} ideal in D(≤ b) then there is an exact pair for I below a.

To see that this suffices for our added correctness condition to define a class of standard models requires a further condition that restricts q̄_{0} to L_{2}. The point then is that if q̄_{0} < z and q̄_{0} ∈ L_{2} then z ∈ L̄_{2}(q̄_{0}) and so we have enough exact pairs below z to define the standard part of any M(p̄) with p̄ ∈D(≤ z). Once we argue that this is possible (Theorem 3.1), Theorem 2.2 and our calculation that the ideal generated by the d_{n} is Σ_{3}^{Q_{0}} shows that our correctness condition picks out only standard models as long as q̄_{0} ∈ L_{2}. In the other direction, it also shows that (with these expanded correctness conditions) the sets coded in M(p̄) by pairs below any x ≥ q̄_{0} not in L_{2} are precisely those Σ_{3}^{X}. This suggests a route to the characterization of x′′ via the following standard fact.

Proposition 2.3. For any sets A and B and n ∈ ℕ, A^{(n)} ≡_{T} B^{(n)} if and only if Σ_{n+1}^{A} = Σ_{n+1}^{B}.

Proof. By the hierarchy theorem Σ_{n+1}^{X} = Σ_{1}^{X^{(n)}}, so if A^{(n)} ≡_{T} B^{(n)}, then Σ_{n}^{A} = Σ_{n}^{B}. On the other hand, for any Z and W, Σ_{1}^{Z} = Σ_{1}^{W} iff Z ≡_{T} W, since the equality implies that both Z and Z̄ (W and W̄) are Σ_{1}, i.e. r.e., in W (Z) and so each is recursive in the other. Thus if Σ_{n+1}^{A} = Σ_{n+1}^{B} then Σ_{1}^{A^{(n)}} = Σ_{1}^{B^{(n)}} and so A^{(n)} ≡_{T} B^{(n)} as required.

We now turn to the notions of invariance under, and biinterpretability up to, the double jump.

Definition 2.4. A relation R(x_{1}, … x_{n}) on degrees is invariant under the double jump if, for all degrees x_{1}, … x_{n} and y_{1}, … y_{n} such that x′′_{i} = y′′_{i} for all i ≤ n, R(x_{1}, … x_{n}) ⇔ R(y_{1}, …, y_{n}).

Definition 2.5. A degree structure S is biinterpretable with arithmetic if it is interpretable in arithmetic and we have formulas in parameters p̄ (including a correctness condition) and a formula φ_{S}(x, ȳ) which defines sets (coded) in the model given by p̄ as described above which provide an interpretation of true arithmetic in S (i.e. the models M(p̄) satisfying the correctness condition are all standard). Moreover, there is an additional formula φ_{R}(x, ȳ, p̄) such that S ⊨ ∀x∃ȳφ_{R}(x, ȳ, p̄) and for every a, ḡ ∈ S, S ⊨φ_{R}(a, ḡ, p̄) if and only if the set {n|φ_{S}(d_{n}, ḡ, p̄)} (where d_{n} is the nth element of the model M(p̄) coded by the parameters p̄) is of degree a. These last conditions then say that the set coded in M(p̄) by ḡ is of degree a and that all degrees a in S have codes ḡ for a set of degree a. If we weaken the second condition on φ_{R} so that for every a, b̄ ∈ S, S ⊨φ_{R}(a, b̄, p̄) if and only if the set {n|φ_{S}(d_{n}, b̄, p̄)} has the same double jump as a, we say that S is biinterpretable with arithmetic up to double jump

It is not hard to see that, if a degree structure S is biinterpretable with arithmetic up to double jump, then we know all there is to know about the definability in S of relations invariant under the double jump.

Theorem 2.6. If a degree structure S is biinterpretable with arithmetic up to double jump, then a relation on S which is invariant under double jump is definable in S if and only if it is definable in arithmetic.

Proof. Consider any definable relation Q(x̄) on S. By the assumption that S is interpretable in arithmetic, we know that Q is definable in arithmetic. For the other direction, suppose Q is definable by a formula Θ(X̄) of arithmetic with additional set variables X̄ and relation ∈ between numbers and elements of X̄, i.e. Θ defines the property that the sequence of the degrees of X̄ satisfies Q. Q is then defined in S by the formula

Ψ(z̄) ≡ ∃p̄, ḡ_{0} … ∃ḡ_{n−1}(φ_{c}(p̄) & ⋀_{i<n} φ_{R}(z_{i}, ḡ_{i}, p̄) → Θ^{T} (ḡ_{i}, p̄)) where T is the translation

of formulas of second order arithmetic given after Proposition 2.1. Here our correctness condition φ_{c} guarantees that the model M(p̄) is standard and we also assume that the requirements of the definition of biinterpretability are satisfied. So the translation of Θ asserts (because of the properties of φ_{R}) that a sequence of sets of degree z_{i} satisfy Θ (in ℕ), i.e. Q holds of z̄.

We also need some facts about forcing in arithmetic. The setting is standard. We consider only recursive notions of forcing, i.e. recursive partial orders P for which forcing sentences of the form Φ_{e}^{G⊕A}(x) ↓= y is recursive in A for any set A. Hence forcing existential sentences (in A) is Σ_{1} (Σ_{1}^{A}) and for universal ones it is Π_{1} (Π_{1}^{A}). For a class C of dense sets, C-generic filters G and C-generic sequences ⟨p_{k}⟩ are defined as usual: they meet all the dense sets in C. If C is the collection of all sets D_{e} = {p|p ⊩ Φ_{e}^{G}(e) ↓ or (∀q ≤_{P} p)(q ⊮ Φ_{e}^{G)}(e) ↓} (D_{e} = {p|p ⊩ Φ_{e}^{A⊕G}(e) ↓ or (∀q ≤_{P} p)(q ⊮ Φ_{e}^{A⊕G}(e) ↓}) then the associated generic filters, sequences and objects G are called 1-generic (over A). We use the following results (and various relativizations):

Theorem 2.7 (Cai and Shore [2012]). If A ∉ GL_{2} then for any recursive notion of forcing P and any collection C of dense sets uniformly recursive in A ⊕ 0′ (such as those for 1-genericity) there is C-generic sequence ⟨p_{s}⟩ ≤_{T} A and so the associated C-generic G is also recursive in A.

The next two theorems reduce constructions of Shore [1982] and Slaman and Woodin [1986], respectively, to constructing 1-generics for recursive notions of forcing. The last Proposition is a standard argument.

Theorem 2.8 (Greenberg and Montalbán [2004]). Given a recursive partial lattice L, there is a recursive notion of forcing for which any 1-generic G computes an embedding of L into the degrees below G which is uniformly recursive in G. So, in particular, one for which any 1-generic G computes degrees q̄ determining a nice effective successor structure in which the d_{n}, and indeed all the elements of the embedded lattice, are uniformly recursive in G.

Theorem 2.9 (Greenberg and Montalbán [2004]). Given any c which uniformly bounds sets C_{i} and relations R_{j} on {deg(C_{i})} there is a recursive notion of forcing for which any 1-generic over C computes degrees p̄_{j} which code the relations R_{j} on the degrees of the C_{i} in the sense that there are fixed formulas φ_{n} independent of C, C_{i} and R_{j}) such that, if R_{j} is of parity n, R_{j}(x̄) ⇔ φ_{n}(x̄, p̄_{j}) and, moreover, φ_{n}(x̄, p̄_{j}) holds if and only if it holds in any (equivalently all) ideals containing the degrees in p̄_{j}.

Proposition 2.10. For any recursive notion of forcing P, set A and 1-generic over A sequence ⟨p_{k}⟩ with an associated set G, (A ⊕ G)′ ≤_{T} A′ ⊕ ⟨p_{k}⟩.

Proof. To decide if e ∈ (A ⊕ G)′, find a k such that p_{k} ∈ D_{e} (as in the definition of 1-genericity over A). This can clearly be done recursively in A′ ⊕ ⟨p_{k}⟩. Then A′ can decide which clause of the definition of D_{e} holds and so if e ∈ (A ⊕ G)′.

3 Biinterpretability up to double jump

We fix a degree z ≤ 0′ which is in \overline{L}_{2}, work in D(≤ z) and plan to show that D(≤ z) is biinterpretable with arithmetic up to double jump. We want to show that there are degrees p̄ < z which define a standard model of arithmetic and a correctness condition as described in §2 that guarantees that M(p̄) is standard for any p̄ satisfying it.

We begin by defining the set {x ≤ z|x ∈ L_{2}}. Of course, that it is definable would be an immediate corollary of biinterpretability up to double jump by Theorem 2.6. Now the proof of this specific result uses and illustrates several of the ingredients needed for the full result. They would suffice to define all the double jump classes in D(≤ z) and, with some additional effort, all the subsets of D(≤ z) invariant under double jump. More is needed for the full result but, most importantly, we actually need this special case to prove the full result.

The crucial point for both this special case and the full result is that the sets we can code below a \overline{GL}_{2} degree x are precisely the ones Σ_{3}^{X} and the class of sets Σ_{3}^{X} uniquely determines x′′ by Proposition 2.3.

Theorem 3.1. The set L_{2} = {x ≤ z|x′′ = 0′′} is definable in D(≤ z).

Proof. Our analysis of coding in models of arithmetic in §2 shows that we have a way to, definably in D(≤z), pick out, via correctness conditions, parameters p̄ that define structures M(p̄) which are models of our finite axiomatization of arithmetic. We have a correctness condition in §2 which would pick out p̄ such that M(p̄) is standard if we also knew that p̄_{0} ∈ L_{2}. Now consider then the formula ψ(x) which says of an x < z that for any p̄ satisfying this correctness condition with p̄_{0} < x any set S coded in M(p̄) by a pair g_{0}, g_{1} < x satisfies the (translation of) the formula of arithmetic saying that S ∈ Σ_{3}. We claim that x ∈ L_{2} if and only this formula holds of x.

First suppose that x ∈ L_{2} and consider any p̄ as described by ψ(x). As p̄_{0} < x, there is a pair g_{0}, g_{1} < z (not necessarily below x) defining the standard part of the model by Proposition 2.1 and Theorem 2.2 as z ∈ L̄_{2}(p̄_{0}) and so the model must be standard. In this case, only Σ_{3}^{P_{0}} = Σ_{3} sets can be defined in the model by codes below x by Proposition 2.1 and so x satisfies ψ

Next, if x ∉ L_{2}, then by Theorems 2.8 and 2.7 and Proposition 2.10, there are parameters q̄ defining a nice effective successor model with q̄_{0}< x and q̄′_{0} = 0′. By Theorems 2.9 and 2.7, we can extend these parameters to ones p̄ defining a standard model of arithmetic which, of course, satisfies the correctness condition for being standard and, as p̄′_{0} = q̄′_{0} = 0′, ψ(p̄_{0}) holds as well. Thus x ∈ L̄_{2}(p̄_{0}) and so every set S ∈ Σ_{3}^{X} is coded in M(p̄) by some g_{0}, g_{1} ≤_{T} x by Proposition 2.1 and Theorem 2.2. Since x′′ > 0′′ there is an S ∈ Σ_{3}^{X} − Σ_{3} by Proposition 2.3 and so a code for such an S below x as required to show that x does not satisfy ψ(x).

Corollary 3.2. The theory of D(≤ z) is recursively equivalent to that of true arithmetic, T h(ℕ).

Proof. By the arguments in the proof of the theorem we can pick out the standard models by our correctness conditions. Thus we can interpret arithmetic in D(≤ z) and so T h(ℕ) ≤_{1−1}T h(D(≤ z)). The other directions follows as we have pointed out from the interpretability of D(≤ z) in arithmetic.

To discuss even the binary relation of two degrees having the same double jump given by biinterpretability up to double jump, we must have a way to analyze, for any a and b the sets coded below them in a single common model. This is the crux of biinterpretability to which we now turn.

Our plan for being able to talk about the sets coded in one model M(p̄) in another M(p̄′) is similar in outline to that used in Nies, Shore and Slaman [1998] for R. We provide a scheme defining isomorphisms between two arbitrary standard models satisfying the standard correctness condition plus the requirement that p̄_{0} (and p̄′_{0}) are in L_{2} which is definable in D(≤ z) by Theorem 3.1. We call this the strong correctness condition and assume from now on that any parameters p̄ used to define a model M(p̄) satisfy it.

Such isomorphisms would allow us to definably transfer assertions about (codes for) sets in different models to ones expressing the same facts about the same sets in a single model and so define the required relation φ_{R}. More precisely, our procedure provides a formula θ(x, y, z̄, z̄′) such that for any p̄ and p̄′ satisfying the strong correctness condition θ(n, m, p̄, p̄′) holds if and only if n and m represent the same natural number in M(p̄) and M(p̄′), respectively. Using this formula, we can talk about a set S coded in M(p̄′) by parameters ḡ inside M(p̄) by, in our translation of arithmetic, replacing φ_{S}(x, ḡ, p̄′) (which says the number represented by x in M(p̄′) is in S) by ∃y[φ_{S}(y, ḡ, p̄′) & θ(x, y, p̄, p̄′)] which then says that the number represented in M(p̄) by x is in S. Thus we can talk about the set S defined in M(p̄′) in M(p̄) as desired.

Arguments similar to those in the proof of 3.1 then allow us to identify degrees up to double jump with the sets coded below them in appropriate models. The transfer procedure we have just suggested then allows us to make the identification in any model and so define the formula φ_{R} required for biinterpretability up to double jump.

We begin with a lemma used to build such isomorphisms by interpolating a sequence of additional models between the two given ones and isomorphisms between each successive pair of such models.

Lemma 3.3. If d ≤ 0′, d ∈ \overline{L}_{2} , a_{0}, a_{1} ∈ L_{1} and P is a recursive notion of forcing, then there is a G ≤_{T} D which is 1-generic for P and such that (A_{0} ⊕ G)′ ≡_{T} 0′ ≡_{T} (A_{1} ⊕ G)′.

Proof. Let C consist of the dense sets for 1-genericity over A_{0} and over A_{1} (each separately). As A′_{0} ≡_{T} A′_{1} ≡_{T} 0′, these sets are uniformly recursive in 0′ and so there is a C-generic sequence recursive in d by Theorem 2.7. Proposition 2.10 then says that (A_{0} ⊕ G)′ ≡_{T} 0′ ≡_{T} (A_{1} ⊕ G)′.

We now turn to our main result.

Theorem 3.4. D(≤ z) is biinterpretable with arithmetic up to double jump.

Proof. Given two models M(p̄_{0}) and M(p̄_{4}) we want to show that there are additional models M(p̄_{k}) for k ∈ {1, 2, 3} and uniformly definable isomorphisms between the domain of these models taking d_{i,n} to d_{i+1,n} for i < 4. (Given parameters p̄_{k} defining a model M(p̄_{k}) we write d_{k,n} for the degree representing the nth element of this model. Similarly, we write p̄_{k,0} for the first element of p̄_{k} and q̄_{k} for the parameters in p̄_{k} determining the effective successor structure which provides the domain of M(p̄_{k}).) Thus (as we explain below) we produce a single formula θ(x, y, z̄, z̄′) which uniformly defines isomorphisms between any two of our models M(p̄_{0}) and M(p̄_{4}) as described above (with z̄ and z̄′ replaced by p̄_{0} and p̄_{4}).

We begin by choosing q̄_{1} < z as given by a 1-generic over p_{0,0} sequence for the recursive notion of forcing of Theorem 2.8. As p_{0,0} ∈ L_{2}, z is L̄_{2}(p_{0,0}) and so such q̄_{1} exists by Theorem 2.7 (relativized to p_{0,0}). Note that q̄_{1} (and so q̄_{1,0}) is in L_{1} by Proposition 2.10 as it is associated with a 1-generic sequence recursive in z. We may now extend q̄_{1} to p̄_{1} defining a standard model M(p̄_{1}) by Theorem 2.9 and Theorem 2.7 as z is \overline{GL}_{2}(q̄_{1}). Similarly, we see that there are q̄_{3} and p̄_{3} bearing the same relation to M(p_{4}) as q̄_{1} and p̄_{1} do to M(p_{0}). Now as q̄_{1,0} and q̄_{3,0} are both low we may apply Lemma 3.3 to the forcing of Theorem 2.8 to get q̄_{2} < z (again as z ∈ L̄_{2}(q̄_{1,0}), L̄_{2}(q̄_{3,0})) such that both q̄_{1,0} ⊕ q̄_{2,0} and q̄_{2,0} ⊕ q̄_{3,0} are in L_{1} and then extend q̄_{2} to p̄_{2} defining M(p̄_{2}) as we did for q̄_{1}.

We now apply Theorem 2.9 and Theorem 2.7 again (many times) to get the desired schemes defining our desired isomorphisms: Given any n ∈ ℕ and i < 4, consider the finite sequences of degrees ⟨d_{i,0}, …, d_{i,n}⟩ and ⟨d_{i+1,0}, …, d_{i+1,n}⟩. We want to show that there are parameters r̄_{i} < z such that the formula φ_{2}(x, y, r̄_{i}) (where φ_{2}(x, y, z̄) ranges over binary relations as z̄ varies as in Theorem 2.9) defines an isomorphism taking d_{i,k} to d_{i+1,k} for each k ≤ n. By the results just cited it suffices to show that the ⨁_{k<n} d_{i,k}⊕ ⨁_{k<n} d_{i+1,k} are

in L_{2} for each i < 4. For i = 0, note that q̄_{1} is associated with a 1-generic/p_{0.0} sequence which is recursive in z. Thus by Proposition 2.10 (suitably relativized) (q̄_{1}⊕p_{0,0})′ = p′_{0,0} and so (q̄_{1,0} ⊕ p̄_{0,0})′ = p′_{0,0}. As p_{0,0} ∈ L_{2}, 0′′ = p̄′′_{0,0} = (q̄_{1,0} ⊕ p̄_{0,0})′′ as required. The argument for i = 3 is similar. For the other pairs, we have already guaranteed that q̄_{1,0} ⊕ q̄_{2,0} and q̄_{2,0} ⊕ q̄_{3,0} are in L_{1}. (Note that we could not directly define the isomorphisms between M(p̄_{1}) and M(p̄_{3}) as the sequences of degrees required in the argument above would be recursive only in p̄_{1,0} ⊕ p̄_{3,0} which could be z and so not in L_{2}. It is by the use of Proposition 2.10 and the model M(p̄_{3}) that we can make all the required joins be in L_{2} as required to apply Theorem 2.7.)

We can now define the desired isomorphism θ(n, m, p̄_{0}, p̄_{4}) between M(p̄_{0}) and M(p̄_{4}). We say that an n in the domain of M(p̄_{0}) (i.e. φ_{D}(n, p̄_{0})) is taken to m in the domain of M(p̄_{4}) (with p̄_{0,0}, p̄_{4,0} ∈ L_{2}) if and only if there are degrees p̄_{k} for k ∈ {1, 2, 3} defining models of arithmetic M(p̄_{k}) and ones r̄_{i} for i < 4 as above such that each φ_{2}(x, y, r̄_{i}) defines an isomorphism between initial segments of (the domains of) M(p̄_{i}) and M(p̄_{i+1}) where the initial segment in M(p̄_{0}) is the one with largest element n and that in M(p̄_{4}) has largest element m. Clearly this can all be expressed using the formulas φ_{D}(x, p̄_{k}) and φ_{<}(x, y, p̄_{k}) defining the domains of M(p̄_{k}) and the orderings on them. Note that the definition of this isomorphism is uniform in p̄_{0} and p̄_{4} and that we have shown that, for any p̄_{0} and p̄_{4} defining standard models as guaranteed by our strong correctness condition, there are parameters below z defining all these isomorphisms. In other words, we have described the desired formula θ(x, ȳ, z̄, z̄′).

We now wish to define the formula φ_{R}(x, ȳ, p̄_{0}) required in the definition of biinterpretability up to double jump. (We have replaced p̄ in Definition 2.5 by p̄_{0} to match our current notation.) First, φ_{R} says that, if x ∈ L_{2} (as defined by Theorem 3.1), then ȳ codes (via our standard φ_{S}) the empty set in M(p̄_{0}). In addition, φ_{R} says that, if x ∉ L_{2} and S is the set coded in M(p̄_{0}) by ȳ, then for every set Ŝ ∈ Σ_{3}^{S} (as given by a definition in arithmetic in M(p̄_{0}) using the definition of S via φ_{S}(x, ȳ, p_{0})), there are ḡ<x and p̄_{4} with p̄_{4,0} < x such that ḡ codes a set Ŝ_{4} in M(p̄_{4}) and θ(n,m, p̄_{0}, p̄_{4}); then, n satisfies the definition of Ŝ in M(p̄_{0}) if and only if φ_{S}(m,ḡ, p̄_{4}), i.e. Ŝ = Ŝ_{4}. By all that we have done already, this guarantees that every Ŝ ∈ Σ_{3}^{S} is Σ_{3}^{X}. For the other direction, φ_{R} also says that if ḡ<x and p̄_{4} with p̄_{4,0} < x are such that ḡ codes a set Ŝ_{4} in M(p̄_{4}) then there is a set Ŝ (coded in M(p̄_{0}) by some h̄) which is Σ_{3}^{S} (as defined in arithmetic in M(p̄_{0})) such that Ŝ = Ŝ_{4} as expressed as above using θ. So again by what we have already done, this guarantees that every Ŝ_{4} ∈ Σ_{3}^{X} is Σ_{3}^{S}. Thus, by Proposition 2.3, S has the same double jump as X as required.

Theorem 2.6 now gives us our desired result on definability in D(≤ z).

Theorem 3.5. A relation on D(≤ z) which is invariant under the double jump is definable in D(≤ z) if and only if it is definable in true first order arithmetic. In particular the jump classes L_{n} (x^{(n)} = 0^{(n)}) and H_{n} (x^{(n)} = 0^{(n+1)}) are definable in D(≤ z) for n ≥ 2.

We can draw one more conclusion about definability of one of the two jump classes not invariant under double jump (H_{1} and L_{1}).

Corollary 3.6. H_{1} is definable in D(≤ z).

Proof. This follows from the fact that x < 0′ is in H_{1} if and only if ∀w ≤ 0′∃y ≤ x(w′′ = y′′) (Nies, Shore and Slaman [1998, Theorem 2.21 and the remarks there on p. 257]). We can now capture this characterization in D(≤ z) using our results. An x ≤ z is in H_{1} if and only if there is a p̄ such that in M(p̄) for every set W ≤_{T} 0′ (with W coded by any h̄ and its being recursive in 0′ expressed in arithmetic in M(p̄)) there is a y ≤ x such that the sets coded by ḡ < y in models M(p̄′) with p̄′ satisfying the strong correctness condition and with p̄′_{0} < y are precisely the sets Σ_{3}^{W} (and so y′′ = w′′). Our isomorphisms between any two models M(p̄) and M(p̄′) allows us to express this formula in D(≤ z) and our results on what sets can be coded below any y show that we get precisely those which are Σ_{3}^{Y} and so the formula says that y′′ = w′′ as required.

The definability of L_{1} in D(≤ z) (or even D(≤ 0′)) and, more generally, full biinterpretability, even up to single jump, are major open questions.

4 Bibliography

Ambos-Spies, K., Ding, D., Wang, W. and Yu, L. [2009], Bounding non-GL_{2} and R.E.A., J. Symb. Logic 74, 989–1000.

Cai, M. and Shore, R. A. [2012], Domination, forcing, array nonrecursiveness and relative recursive enumerability, J. Symb. Logic 77 33-48.

Greenberg, N. and Montalbán, A. [2004], Embedding and coding below a 1-generic degree, Notre Dame J. Formal Logic 44, 200-216.

Hodges, W. [1993], Model Theory, Cambridge University Press, Cambridge UK.

Nerode, A. and Shore, R. A. [1980], Reducibility orderings: theories, definability and automorphisms, Ann. of Math. Logic 18, 61-89.

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.

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

Shore, R. A. [1982], Finitely generated codings and the degrees r.e. in a degree d, Proc. Am. Math. Soc. 84, 256-263.

Shore, R. A. [1988], Defining jump classes in the degrees below 0′, Proc. Am. Math. Soc. 104, 287-292.

Shore, R. A. [2007], Direct and local definitions of the Turing jump, J. Math. Logic 7, 229-262.

Shore, R. A. [2013], Lecture notes on the Turing degrees, AII Graduate Summer School in Logic, Singapore, 28 June - 23 July 2010, World Sci. Publ., to appear.

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

Slaman, T. A. [1991], Degree structures, in Proc. Int. Cong. Math., Kyoto 1990, Springer-Verlag, Tokyo, 303-316.

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

Slaman, T. A. and Woodin, H. W. [1986], Definability in the Turing degrees, Illinois J. Math. 30, 320-334.