The Σ 2 theory of D h ( ⩽ h O ) as an uppersemilattice with least and greatest element is decidable

Abstract

The decidability of the two quantifier theory of the hyperarithmetic degrees below Kleene’s $O$ in the language of uppersemilattices with least and greatest element is established. This requires a new kind of initial segment result and a new extension of embeddings result both in the hyperarithmetic setting.

Keywords

Recursion theory hyperarithmetic theory

1. Introduction

1.1. The hyperarithmetic degrees

Hyperarithmetic reducibility is a notion of reduction with connections to Turing reducibility, recursive well-orderings, and definability in second-order arithmetic. A subset X of ω is hyperarithmetic in a subset Y of ω, written $X ⩽_{h} Y$ , if there is an ordinal δ with a Y-recursive representation such that X is Turing reducible to the δth jump of Y. (Some care must be taken in defining $Y^{(δ)}$ : $Y^{(0)} = Y$ , $Y^{(δ + 1)} = {(Y^{δ})}^{'}$ , and if ${δ_{n}}_{n = 0}^{\infty}$ is a Y-recursive sequence of Y-recursive ordinals, then $Y^{(lim δ_{n})} = ⨁_{n} Y^{(δ_{n})}$ . It must be shown that, up to Turing degree, the definition of $Y^{(δ)}$ for limit δ does not depend on the choice of Y-recursive cofinal sequence.) Kleene showed that X is hyperarithmetic in Y iff X is $Δ_{1}^{1}$ definable in second-order arithmetic with a predicate for membership in Y.

The hyperarithmetic degrees (or hyperdegrees), $D_{h}$ , is the quotient of $2^{ω}$ under hyperarithmetical equivalence: $X \equiv_{h} Y$ iff $X ⩽_{h} Y$ and $Y ⩽_{h} X$ . This degree structure shares many similarities with the Turing degrees, for instance, it is an uppersemilattice with least element: The join operator can be defined (on representatives for degrees) as $\begin{matrix} X \oplus Y = {2 n : n \in X} \cup {2 n + 1 : n \in Y}, \end{matrix}$ and the least element is the degree of the empty set. There is also a notion of jump: the hyperjump of X, written $O^{X}$ , is the $Π_{1}^{1} (X)$ complete set of notations for X-recursive ordinals. This operator bears some similarity to the Turing jump operator, which takes a set X and returns a complete $Σ_{1}^{0} (X)$ set. The tempting analogy between being recursively enumerable in X (which is equivalent to being $Σ_{1}^{0} (X)$ ) and being $Π_{1}^{1} (X)$ is a false one: The only hyperdegrees with a $Π_{1}^{1}$ member are the trivial hyperdegree and the hyperdegree of $O$ , the hyperjump of the empty set.

Despite this, $D_{h} (⩽_{h} O)$ , the hyperdegrees hyperarithmetic in $O$ , is still an interesting substructure of $D_{h}$ in its own right and may be considered analogous to $D_{T} (⩽_{T} 0^{'})$ , the Turing degrees below $0^{'}$ . It is natural to ask questions about what kind of structures embed into $D_{h} (⩽_{h} O)$ ? What its initial segments look like? How complex is its theory? And so on. This paper concerns embeddings of finite lattices into $D_{h} (⩽_{h} O)$ that takes the top element to $O$ and everything else to an initial segment, extensions of embeddings of finite uppersemilattices, and an application of these facts to the complexity of the theory of $D_{h} (⩽_{h} O)$ .

Note that, in the definition of $⩽_{h}$ and $D_{h}$ , very little is changed by working with functions from ω to itself rather than subsets of ω: A function from ω to ω can be identified with its graph, and so with a subset of ω by some fixed recursive pairing function, and a subset of ω can be identified with its characteristic function. In the following, a distinction between these two perspectives is not observed.

1.2. An overview of the proof

The goal is to establish the decidability of the $Σ_{2}$ theory of $D_{h} (⩽_{h} O)$ in the language of uppersemilattices. Toward this goal, a decision procedure must be provided and proved correct. It will be shown that deciding the correctness of such a sentence can be reduced to deciding questions of the following kind:

Given a finite bounded uppersemilattice $U$ and a collection $V_{1}, \dots, V_{n}$ of finite bounded uppersemilattice extensions of $U$ , does every embedding of $U$ into $D_{h} (⩽_{h} O)$ extend to an embedding of one of the $V_{i}$ ?

The answer to this question is yes if one of the $V_{i}$ does not put any new elements below any of the elements of $U$ other than its greatest element. In this case $V_{i}$ is called an almost-end-extension of $U$ , and $U$ is called an almost-initial-segment of $V_{i}$ . If no such $V_{i}$ exists, then the answer is no.

The proof of the correctness of this answer is in two parts: the first part establishes that any bounded uppersemilattice $U$ can be realized as an almost-initial-segment of $D_{h} (⩽_{h} O)$ . Consequently, if $V$ is a superstructure of $U$ that is not itself an almost-end-extension, then the provided embedding of $U$ into $D_{h} (⩽_{h} O)$ cannot be extended to $V$ , as there is no space in $D_{h} (⩽_{h} O)$ below the image of $U$ ; the second part establishes that if $V$ is an almost-end-extension of $U$ , then any embedding of $U$ can be extended.

Producing initial segments of degree structures has a long history. It begins with Spector [8] producing a minimal Turing degree, which is a very simple initial segment. Spector’s proof uses perfect trees to approximate a set of minimal degree. The approximation is improved by successively pruning the tree. The strategy of using perfect trees to construct minimal degrees has provided fruitful in other degree settings and in producing more complicated minimal structures.

As the degree structures we consider are uppersemilattices with a least element, and a finite uppersemilattice is a lattice, the finite initial segments of the degree structures must be lattices. To try to find an initial segment that is isomorphic to a particular lattice a representation of the lattice by a combinatorial object called a table is used. These easily allow a computability theorist to translate algebraic facts about the lattice into computations. For instance if the lattice has objects x and y and $x ⊑ y$ , then the computability theorist would like to produce sets X and Y, corresponding to x and y, such that X can be computed from Y. The lattice table lets one ‘look up’ what the value of X should be on a particular input if one already knows the value of Y.

To marry lattice tables to perfect trees, the trees are built out of sequences of elements of lattice tables. A branch on the tree then naturally corresponds to a collection of sets corresponding to the lattice. Some of the algebraic facts about the lattice are given for free by the structure of the lattice table, e.g. ⊑ and ⊔. Showing that ⊓ and ⋢ are preserved and that the sets form an initial segment requires delicately pruning the trees.

In the forthcoming, there is also the concern of mapping the greatest element of the lattice to a particular set. To do this, the set $O$ is coded into the set corresponding to the greatest element. This produces a new issue: can the various requirements for the rest of the lattice be met without interfering with the coding procedure?

Towards the second part of the answer, embeddings must also be extended. This is independent of the initial segments work mentioned previously. Using algebraic arguments the problem is simplified by considering two special cases: the first where the extension is free and the second where the extension is generated by a single new element. The free extensions result is a straightforward application of Cohen forcing, but the other requires Kumabe-Slaman forcing to produce a set with the correct computational properties.

2. Decidability

Definition 2.1 (Lattice and uppersemilattice).

A lattice $\begin{matrix} L = (L, ⊑_{L}, ⊓_{L}, ⊔_{L}, ⊤_{L}, ⊥_{L}) \end{matrix}$ is a structure such that $⊑_{L}$ is a partial order on the set L satisfying the following:

$⊤_{L}$ is the greatest element of $L$ .

$⊥_{L}$ is the least element of $L$ .

Each pair $x, y \in L$ have a greatest lower bound $x ⊓_{L} y$ .

Each pair $x, y \in L$ have a least upper bound $x ⊔_{L} y$ in $L$ .

An uppersemilattice

U = (U, ⊑_{U}, ⊔_{U}, ⊥_{U})

is like a lattice, but there need not be a greatest element, nor need greatest lower bounds exist.

An uppersemilattice with ⊤ is an uppersemilattice with a greatest element $⊤_{U}$ . Such a structure is also called a bounded uppersemilattice.

Notation.
Lattices and uppersemilattices are denoted by calligraphic roman letters $L$ , $U$ , $V$ and the like. Elements of lattices (and uppersemilattices) are denoted with lowercase roman letters from the end of the alphabet: x, y, z, w.

Whenever confusion will not arise, the subscripts on the various parts of the structure are dropped, e.g. ⊑ instead of $⊑_{L}$ . Additionally, uppersemilattice is abbreviated by USL, and uppersemilattice with ⊤ is abbreviated by ${USL}^{⊤}$ .

Note that a finite USL $U$ is a lattice: its greatest element and meet are given by $\begin{matrix} ⊤ : = ⨆_{x \in U} x and x ⊓ y : = ⨆_{z ⊑ x, y} z, respectively . \end{matrix}$ As $U$ is finite and has least element ⊥, each of these joins are defined over nonempty, finite sets; therefore, they are well defined.

The satisfiability of a $Π_{2}$ sentence in the language of USL^⊤s over $D_{h} (⩽_{h} O)$ (or any ${USL}^{⊤}$ ) can be effectively reduced (in a manner entirely analogous to that of Lerman Theorem VII.4.4 [5]) to deciding questions of the following form:
Question.
Let $U$ be a finite USL^⊤ and let $V_{1}, \dots, V_{n}$ be finite USL^⊤s each a superstructure of $U$ . Then is it the case that every embedding of $U$ into $D_{h} (⩽_{h} O)$ extends to an embedding of one of the $V_{i}$ s?

Note that the embedding must preserve ⊔, and must map ⊥ to the degree of the empty set and ⊤ to the degree of $O$ .

To answer the question, we introduce some terminology and state our results.
Definition 2.2 (Almost-initial-segment).

If $U$ and $V$ are USL^⊤s and $U$ is a substructure of $V$ , then $U$ is an almost-initial-segment of $V$ (alternatively, $V$ is an almost-end-extension of $U$ ) if whenever $u \in U$ and $v \in V ∖ U$ satisfy $v ⊑ u$ , then $u = ⊤$ , i.e., the only way an element of $U$ is above something strictly in $V$ is if it is the greatest element (in both $U$ and $V$ ).

Theorem 2.3.
Let $L$ be a finite lattice. Then there is a lattice embedding $f : L \to D_{h} (⩽_{h} O)$ such that the image of $L$ under f is an almost-initial-segment of $D_{h} (⩽_{h} O)$ .
Theorem 2.4.
Let $U$ and $V$ be finite USL ^⊤ s such that $U$ is an almost-initial-segment of $V$ . Then every embedding of $U$ into $D_{h} (⩽_{h} O)$ extends to one of $V$ .

Given these results, the aforementioned question can be answered by determining whether any of the $V_{i}$ s are almost-end-extensions of $U$ , which can be answered in a uniform and recursive manner: If $V_{i}$ is an almost-end-extension of $U$ , then Theorem 2.4 provides an extension of any embedding of $U$ into $D_{h} (⩽_{h} O)$ to one of $V_{i}$ . On the other hand, if no $V_{j}$ is an almost-end-extension of $U$ , then Theorem 2.3 provides an embedding of $U$ into $D_{h} (⩽_{h} O)$ as an almost-initial-segment, which can not extend to any of the $V_{j}$ s.

The major project for the rest of this paper is to establish Theorems 2.3 and 2.4.
3. Almost-initial-segments of $D_{h} (⩽_{h} O)$

Recall that a finite USL^⊤ is a lattice. An arbitrary embedding of a USL^⊤ into $D_{h} (⩽_{h} O)$ need not preserve the meet structure; however, if the image of an embedding is an almost-initial-segment, then the meet structure will be preserved. Consequently, while the question to be answered concerns almost-initial-segments of $D_{h} (⩽_{h} O)$ , there is no loss of generality in considering lattices.

Kjos-Hanssen and Shore [4] have produced initial segment embeddings of every sublattice of every hyperarithmetic lattice; a class which contains all finite lattices. We combine their forcing construction with ideas from Lerman and Shore [6] to code $O$ into the top real we construct, while preserving the lattice structure, in such a way that everything except ⊤ is mapped into some initial segment.

Let $L$ be a finite lattice, and let A be the set of coatoms of $L$ , i.e., $\begin{matrix} A = {x \in L : x ⊏ ⊤ and there is no y \in L s.t. x ⊏ y ⊏ 1} . \end{matrix}$ Let f be an embedding of $L$ into $D_{h}$ as an initial-segment, as provided by Kjos-Hanssen and Shore [4]. As $L$ is finite, it is recursive; therefore, there is such an f which takes ⊤ to a degree below that of $O$ . Define a map $\tilde{f} : L \to D_{h} (⩽_{h} O)$ by $\begin{matrix} \tilde{f} (x) = \{\begin{matrix} f (x) & if x \neq ⊤, \\ degree (O) & if x = ⊤ . \end{matrix} \end{matrix}$ This map will not, in general, be a lattice embedding of $L$ , as the join structure may not be preserved. However, if $| A | < 2$ , then there are no $x, y \in L$ such that $x, y < ⊤$ , yet $x ⊔ y = ⊤$ . In this case, $\tilde{f}$ will be a lattice embedding and, by choice of f, will be an almost-initial-segment embedding of $L$ into $D_{h} (⩽_{h} O)$ . Henceforth, it is assumed that $| A | ⩾ 2$ .

The rest of this section approximately follows the structure of Kjos-Hanssen and Shore [4] with the additional concern of coding $O$ into the image of the top element of a lattice. The notion of forcing employed is rather simpler than theirs (because the lattices are finite), but whenever a dense set must be met, it must be shown it can be met without interfering with the coding procedure (which is yet to be defined).

3.1. Lattice representations

To define the notion of forcing for almost-initial-segments a strong kind of representation of $L$ is required.

Definition 3.1 (USL table).

A set Θ of maps from $L$ to ω is an USL table for $L$ if it has the following properties:

(Nontriviality of Θ) The zero map $x \mapsto 0$ is in Θ (This map is denoted 0 as well).

(⊥ is trivial) For every $α \in Θ$ , $α (⊥) = 0$ .

And for every choice $x, y, z \in L$ :

(Order) If $x ⊑ y$ , and $α, β \in Θ$ satisfy $α (y) = β (y)$ , then $α (x) = β (x)$ .

(Differentiation) If $x ⋢ y$ , then there are $α, β \in Θ$ such that $α (y) = β (y)$ , yet $α (x) \neq β (x)$ .

(Join) If $x ⊔ y = z$ , and if $α, β \in Θ$ satisfy $α (x) = β (x)$ and $α (y) = β (y)$ , then $α (z) = β (z)$ .

Notation.
Lattice tables are denoted by Θ, $Θ_{1}$ , $Θ_{2}$ and so on, and their elements are denoted by lowercase Greek letters α, β and γ.

For $x \in L$ and $α, β \in Θ$ members of an USL table for $L$ , $α \equiv_{x} β$ means $α (x) = β (x)$ . This is an equivalence relation on Θ. Furthermore, $α \equiv_{x, y} β$ means that $α \equiv_{x} β$ and $α \equiv_{y} β$ .

This notation is extended to partial functions (and so, in particular, to strings) by declaring $f \equiv_{x} g$ if wherever f, g are both defined their values agree modulo x.
Definition 3.2 (Sequential lattice representation).

A nested sequence ${Θ_{i} : i \in ω}$ of finite USL tables for $L$ is a sequential (lattice) representation for $L$ if for every $i \in ω$ :

There are meet interpolants for $Θ_{i}$ in $Θ_{i + 1}$ , i.e., if $x, y, z \in L$ satisfy $x ⊓ y = z$ , and if $α, β \in Θ_{i}$ satisfy $α \equiv_{z} β$ , then there are $γ_{0}, γ_{1}, γ_{2} \in Θ_{i + 1}$ such that $\begin{matrix} α \equiv_{x} γ_{0} \equiv_{y} γ_{1} \equiv_{x} γ_{2} \equiv_{y} β . \end{matrix}$

There are homogeneity interpolants for $Θ_{i}$ in $Θ_{i + 1}$ , i.e., for all $α_{0}, α_{1}, β_{0}, β_{1} \in Θ_{i}$ such that $\begin{matrix} (\forall x \in L) [α_{0} \equiv_{x} α_{1} \to β_{0} \equiv_{x} β_{1}] \end{matrix}$ there are $γ_{0}, γ_{1} \in Θ_{i + 1}$ and $L$ -homomorphisms $f, g, h : Θ_{i} \to Θ_{i + 1}$ such that $\begin{matrix} f : α_{0}, α_{1} \mapsto β_{0}, γ_{1}, g : α_{0}, α_{1} \mapsto γ_{0}, γ_{1}, h : α_{0}, α_{1} \mapsto γ_{0}, β_{1} . \end{matrix}$ (f is an $L$ -homomorphism from $Θ_{i}$ to $Θ_{i + 1}$ if for each $α, β \in Θ_{i}$ and each $x \in L$ if $α \equiv_{x} β$ , then $f (α) \equiv_{x} f (β)$ .)

The above definition is a simplification of the representation given in Theorem 5.1 of Kjos-Hanssen and Shore [4]. It is simpler because the lattices are finite, and so no sequence of approximations of the lattice are needed. Using such a representation, $L$ could be embedded as an initial segment of $D_{h}$ , or even $D_{h} (⩽_{h} O)$ ; however, there is insufficient control over the image of ⊤ for this purpose of this paper. Apparatus that allows coding of $O$ into the image of ⊤ is required:

Definition 3.3 (Coding-ready representation).

A sequential representation ${Θ_{i} : i \in ω}$ has $C \subseteq Θ_{0}$ as a coding set if there is a bijective map g from $\begin{matrix} {⟨ x, y, k ⟩ : k \in {0, 1}, x ⊔ y = ⊤, and x, y \neq ⊤} \end{matrix}$ to C such that:

For every $x, y \in L ∖ {⊤}$ if $x ⊔ y = ⊤$ , then $\begin{matrix} g (x, y, 0) \equiv_{x} g (x, y, 1) and g (x, y, 0) ≢_{y} g (x, y, 1) . \end{matrix}$

For all $α \in C$ and all $x \in L ∖ {⊤}$ , there is a $β \in Θ_{0} ∖ C$ such that $α \equiv_{x} β$ .

The table is acceptable for A (the set of coatoms of $L$ ) if for each $i > 0$ there is a subset $Θ_{i}^{*}$ of $Θ_{i}$ , containing $Θ_{i - 1}$ such that (1) holds for $Θ_{i + 1}^{*}$ in place of $Θ_{i + 1}$ , (2) holds for $Θ_{i + 1}^{*}$ in place of $Θ_{i}$ , and further, (in the notation of (2)) if $f (α) \in C$ , then $α = α_{0}$ or $α = α_{1}$ (and the same for g and h), and, finally:

For all $x \in A$ , all $i \in ω$ , and all $α_{0}, α_{1} \in Θ_{i}$ there exists $β_{0}, β_{1} \in Θ_{i + 1}^{*} ∖ Θ_{i}$ such that $\begin{matrix} α_{0} \equiv_{x} β_{0}, α_{1} \equiv_{x} β_{1}, and (\forall y \in L) [α_{0} \equiv_{y} α_{1} \to β_{0} \equiv_{y} β_{1}] . \end{matrix}$

{Θ_{i} : i \in ω}

has coding set C, the differentiation property of USL tables is satisfied outside of C (i.e., for each

x ⋢ y

there are

α, β \in Θ_{0} ∖ C

such that

α \equiv_{y} β

yet

α ≢_{x} β

), and it is acceptable for A, it is called coding-ready.

Recursive coding-ready sequential representation ${Θ_{i} : i \in ω}$ for $L$ are constructed shortly. Firstly, motivation and explanation of the definition: the representation will be nested as displayed $\begin{matrix} C ⊊ Θ_{0} ⊊ Θ_{1}^{*} ⊊ Θ_{1} ⊊ Θ_{2}^{*} ⊊ Θ_{2} ⊊ \dots \end{matrix}$ Each $Θ_{i}$ will be a USL table for $L$ such that there are meet interpolants for elements of $Θ_{i}$ inside $Θ_{i + 1}^{*}$ , and there are homogeneity interpolants for $Θ_{i + 1}^{*}$ in $Θ_{i + 1}$ . The elements of C are special, and they indicate coding occurs. Condition (3) ensures that for each $x, y \in L$ joining up nontrivially to ⊤ there is a pair of distinguished coding elements. Condition (4) and the fact that the differentiation property is satisfied outside of C implies that a coding element can be replaced with an element that does not code and still preserve a congruence. Condition (5) in the definition of acceptable for A tells us that if there is a split (this will be defined later), then there is a split not using coding elements, and the requirement that f, g, and h only take on coding values when entirely necessary (i.e. when $β_{0} \in C$ or $β_{1} \in C$ ) means there are homogeneity interpolants which do no coding.

Theorem 3.4.
Let $L$ be a finite lattice with at least two coatoms and A be the set of coatoms of $L$ . Then there is a recursive coding-ready sequential lattice representation for $L$ .

Lerman and Shore [6] construct a sequential representation which is very similar to the required representation; the main difference is in the homogeneity interpolants. In the notation of this paper the $L$ -homomorphisms f, g, h in Lerman and Shore act on $α_{0}$ , $α_{1}$ as follows: $\begin{matrix} f : α_{0}, α_{1} \mapsto β_{0}, γ_{0}, g : α_{0}, α_{1} \mapsto γ_{0}, γ_{1}, h : α_{0}, α_{1} \mapsto γ_{1}, β_{1} . \end{matrix}$ In particular, $f (α_{1}) = γ_{0}$ and $h (α_{0}) = γ_{1}$ instead of $γ_{1}$ and $γ_{0}$ , respectively. (There is also a difference in the coding set; Lerman and Shore have coding elements for each unordered pair ${x, y}$ and this paper has them for each ordered pair $⟨ x, y ⟩$ . The reason for this difference is purely notational and does not present any mathematical difficulties.)

In their construction, Lerman and Shore begin with a finite USL table Θ for $L$ and then construct a finite USL table extension $Θ_{0}$ of Θ and observe that $Θ_{0}$ contains a coding set C disjoint from Θ satisfying properties (3) and (4). Furthermore, as the construction started with a USL table Θ, the differentiation property is satisfied outside C, as required.

Then they proceed inductively: Given $Θ_{i}$ , by Lerman Appendix B.2.6 [5], there is a finite USL table $Θ_{i}^{1}$ which contains meet interpolants for $Θ_{i}$ . They then argue that $Θ_{i}^{1}$ can be extended to a finite USL table $Θ_{i}^{}$ satisfying (5), and as $Θ_{i} \subseteq Θ_{i}^{1} ⊊ Θ_{i + 1}^{}$ they can find meet interpolants for $Θ_{i}$ in $Θ_{i + 1}^{}$ . All of this is uniformly recursive.

Consequently, all that is needed is that given $Θ_{i + 1}^{}$ a finite USL table for $L$ that a finite USL table extension $Θ_{i + 1}$ of $Θ_{i + 1}^{}$ can be found (uniformly and recursively) such that homogeneity interpolants for $Θ_{i + 1}^{}$ can be found in $Θ_{i + 1}$ and the $L$ -homomorphisms avoid the coding set (unless $β_{0} \in C$ , or $β_{1} \in C$ ).

Kjos-Hanssen and Shore [4] have already completed this work for us: Their Proposition 5.6 (taking $\hat{L} = L$ ) says that there is such a USL table extension which has homogeneity interpolants of the kind needed (again uniformly and recursively). An examination of their proof shows that if $α \in Θ_{i + 1}^{}$ then $f (α) \notin Θ_{i + 1}^{}$ unless $α = α_{0}$ or $α = α_{1}$ , and similarly for g and h. Hence applying this Proposition allows the induction to continue and completes the construction.
3.2. Perfect trees and forcing

From here, fix a finite lattice $L$ with a set of coatoms A of cardinality at least two and a recursive coding-ready sequential representation ${Θ_{i} : i \in ω}$ for $L$ .

Definition 3.5 (Uniform tree).

A uniform tree for the representation ${Θ_{i} : i \in ω}$ is a function T with both domain and range the set of all strings σ such that if $σ (n)$ is defined, then $σ (n) \in Θ_{n}$ that satisfies the following properties for all $σ, τ \in dom (T)$ :

(Order) If $σ \subseteq τ$ , then $T (σ) \subseteq T (τ)$ .

(Nonorder) If $σ | τ$ , then $T (σ) | T (τ)$ . In fact, for each length l it is required that there is a string π such that if $| σ | = l$ and $α \in Θ_{l}$ (so that $σ^{⌢} α \in dom (T)$ ), then $T (σ^{⌢} α) \supseteq T {(σ)}^{⌢} π^{⌢} α$ .

(Uniformity) For every fixed length l, there is a string $π_{l}$ and for every $α \in Θ_{l}$ , there is a string $ρ_{l, α}$ whose length does not depend on α such that if $| σ | = l$ , then $T (σ^{⌢} α) = T {(σ)}^{⌢} {π_{l}}^{⌢} ρ_{l, α}$ . Note that $π_{l}$ and $ρ_{l, α}$ only depend on the length of σ.

The uniform tree T is branch-coding-free if for every length l and every $α \in Θ_{l}$ , the string ${π_{l}}^{⌢} ρ_{l, α}$ , which is the extension corresponding to α at this level, does not do unnecessary coding, i.e., for each j if $({π_{l}}^{⌢} ρ_{l, α}) (j) \in C$ , then $j = | π_{l} |$ (and so $α \in C$ ). (This means that the only time a member α of our coding set C appears on a branch is at a fork on the path corresponding to α).

The tree T is congruence-respecting if for every length l, every $α, β \in Θ_{l}$ , and every $x \in L$ if $α \equiv_{x} β$ then ${π_{l}}^{⌢} ρ_{l, α} \equiv_{x} {π_{l}}^{⌢} ρ_{l, β}$ (or, equivalently, $ρ_{l, α} \equiv_{x} ρ_{l, β}$ ).

These trees are related to those in Definition 2.4 of Kjos-Hanssen and Shore [4]. There are some simplifications, again, because $L$ is finite: congruences are preserved all the time, and the trees all have the same domain. The nonorder (and, consequently, uniformity) property is different in that there is the string π that every branch at a level has to follow before splitting. This is a technical requirement that allows the proof of the fusion lemma (Kjos-Hanssen and Shore also need this modification. Their fusion lemma, as written, does not produce a forcing condition). The requirement that the trees are branch-coding-free is new and allows us to code.

Notation.
Uniform trees will be denoted by uppercase Roman letters, most frequently T, S, R, and the set of branches of T is denoted $[T]$ . Strings of members of the lattice representation will be denoted σ, τ, ρ, ν and so on, π is reserved for the π in the uniformity property. The concatenation of σ by τ is written $σ^{⌢} τ$ , and a string of length one is identified with its value. So, for instance, $σ^{⌢} α$ abbreviates $σ \in \prod_{i = 0}^{n} Θ_{i}$ and $α \in Θ_{n + 1}$ .

For technical reasons, the height of a level l is defined to be $| T {(σ)}^{⌢} π_{l} |$ where σ is any string of length l, and $π_{l}$ is the string as in the definition of the uniformity property. By uniformity, this is independent of the choice of σ and so is well defined.

Hyperarithmetic, branch-coding-free, congruence-respecting, uniform trees will be the conditions of the notion of forcing for producing almost-initial-segments. Observe that the identity tree satisfies all these properties.
Definition 3.6 (Subtree).

A uniform tree S is a subtree of a uniform tree T, written $S \subseteq T$ , if the range of S is contained in the range of T.

There are two operations on uniform trees:

Definition 3.7.
If T is a uniform tree and $σ \in \prod_{i = 0}^{l} Θ_{i}$ for some l then $T_{σ}$ is defined by: $\begin{matrix} T_{σ} (τ) = T (σ^{⌢} τ) . \end{matrix}$ If $μ \in \prod_{i = 0}^{l} Θ_{i}$ for some l and $l ⩽ | T (\emptyset) | - 1$ , then the transfer tree of T over μ, written $T^{μ}$ , is the tree such that $T^{μ} (σ)$ is the string $T (σ)$ but with its initial segment of length l replaced by μ. (i.e., the root of T is changed by replacing the initial segment of the right length by μ). For clarity $T_{σ}^{μ}$ denotes ${(T_{σ})}^{μ}$ .
Proposition 3.8.
Let T be a uniform tree. Then $T_{σ}$ and $T^{μ}$ are uniform trees whenever they are defined. Furthermore, if T is branch-coding-free, congruence-respecting, or hyperarithmetic, then $T_{σ}$ and $T^{μ}$ are, correspondingly, branch-coding-free, congruence-respecting, or hyperarithmetic. Finally, $T_{σ}$ is a subtree of T whenever it is defined, and ${(T_{σ})}_{τ} = T_{σ^{⌢} τ}$ .

Proofs of these claims are entirely routine and are omitted.
Definition 3.9 (Perfect forcing).

${Θ_{i} : i \in ω}$ -perfect forcing is the set $P_{{Θ_{i} : i \in ω}} = P$ of all hyperarithmetic, branch-coding-free, congruence-respecting, uniform trees ordered by the subtree relation, i.e., for $T, S \in P$ the tree T extends S or T refines S, written $T ⩽_{P} S$ , if T is a subtree of S.

Now that the notion of forcing is defined the generic objects can be defined. Clearly, for each length l the set ${T \in P : | T (\emptyset) | > l}$ is dense in $P$ . Consequently, a descending sequence of conditions ${T_{i}}_{i = 0}^{\infty}$ meeting these dense sets will correspond to an object $G$ : an element of the product $\prod_{i = 0}^{\infty} Θ_{i}$ defined by $G (n) = α$ iff there is an i such that $T_{i} (\emptyset) (n) ↓ = α$ . For each $x \in L$ a function $G^{x} : ω \to ω$ is defined by $\begin{matrix} G^{x} (n) = G (n) (x) . \end{matrix}$ The embedding under construction will take $x \in L$ to the degree of $G^{x}$ . To ensure that $G^{⊤} ⩾_{h} O$ coding is required.

Definition 3.10 (Coding).

Fix $x, y \in L$ that join up nontrivially to ⊤ (i.e., $x ⊔ y = ⊤$ and $x, y \neq ⊤$ ). The root-coding of T for $⟨ x, y ⟩$ is the number of occurrences of $g (x, y, 0)$ and $g (x, y, 1)$ in the string $T (\emptyset)$ . A subtree S of T does no more root-coding than T for $⟨ x, y ⟩$ if the root-coding of T for $⟨ x, y ⟩$ is the same as that for S and it does no more root-coding if it does no more root-coding for each pair $⟨ x, y ⟩$ which join up nontrivially to ⊤.

Given $G^{x} \oplus G^{y}$ our decoding procedure is as follows:

On input n search for the nth number m such that $G (m) \equiv_{x} g (x, y, 0)$ and either $G (m) \equiv_{y} g (x, y, 0)$ or $G (m) \equiv_{y} g (x, y, 1)$ . If $G (m) \equiv_{y} g (x, y, 0)$ we say n is not in the set, and if $G (m) \equiv_{y} g (x, y, 1)$ then we say n is in the set.

(Note that g is the function in the definition of coding set, and that the decoding procedure for $G^{x} \oplus G^{y}$ depends on the order of x and y.)

This procedure is clearly recursive in $G^{x} \oplus G^{y}$ , as ${Θ_{i} : i \in ω}$ is recursive, and to determine whether $G (m) \equiv_{z} α$ it suffices to know $G^{z} (m)$ . Also, the decoding procedure does not detect noncoding elements: If $γ \equiv_{x} g (x, y, 0)$ , then $γ \equiv_{x} g (x, y, 1)$ too. Hence, if, further, $γ \equiv_{y} g (x, y, 0)$ , then, by the join property, $γ \equiv_{x ⊔ y} g (x, y, 0)$ . But, as $x ⊔ y = ⊤$ , $γ \equiv_{⊤} g (x, y, 0)$ and so $γ = g (x, y, 0)$ . Entirely similarly, if $γ \equiv_{y} g (x, y, 1)$ , then $γ = g (x, y, 1)$ .

Hence, to ensure that our decoding procedure gives the characteristic function of some set X, it suffices to construct a $G$ such that, for each n, at the nth place where $G (m) = g (x, y, 0)$ or $G (m) = g (x, y, 1)$ , that it is $g (x, y, 0)$ iff $n \notin X$ and is $g (x, y, 1)$ iff $n \in X$ . Therefore, a running theme for the remainder of this section will be meeting dense sets of various kinds without increasing the root-coding of a condition.

3.3. The forcing relation

With this strategy in mind the language of forcing and the forcing relation must be defined, and it must be shown that a sufficient degree of genericity can be obtained without interfering with the coding procedure.

Definition 3.11 (Languages and models).

For each $x \in L ∖ {⊤}$ the language $L (ω_{1}^{CK}, G^{x})$ and model $M (ω_{1}^{CK}, G^{x})$ are defined as described in Sacks chapter III, Section 4 [7].

Briefly, $L (ω_{1}^{CK}, G^{x})$ is second-order arithmetic augmented with ranked set variables $X^{δ}$ for $δ < ω_{1}^{CK}$ that can be quantified over. A minor change is that the generic object will be an element of $ω^{ω}$ rather than a subset of ω. This changes the atomic formulas slightly, and requires a function symbol $G^{x}$ rather than a predicate.

A formula is ranked if each of its set variables is ranked; it is $Σ_{1}^{1}$ if it has an initial block of (unranked) set existentials, then a ranked formula. For a sentence $(\exists X^{δ}) φ (X^{δ})$ and a formula $H (n)$ of rank at most δ that has only one free variable, n, which is a natural number variable, $φ (\hat{n} H (n))$ is obtained by replacing each occurrence of $t \in X^{δ}$ with $H (t)$ , for each first-order term t. This operation decreases full ordinal rank.

$M (ω_{1}^{CK}, G^{x})$ is the class of all reals definable from $G^{x}$ by a formula of $L (ω_{1}^{CK}, G^{x})$ . Sacks provides simultaneous inductive definitions of the interpretation of the formulas of $L (ω_{1}^{CK}, G^{x})$ and the class of reals $M (ω_{1}^{CK}, G^{x})$ . Provided that $ω_{1}^{G^{x}} = ω_{1}^{CK}$ , $M (ω_{1}^{CK}, G^{x})$ is precisely the class of reals which are hyperarithmetic in $G^{x}$ , and so the forcing language has a term for every real hyperarithmetic in $G^{x}$ assuming that $ω_{1}^{CK}$ is preserved.

Definition 3.12 (Forcing relation).

Let φ be a sentence of $L (ω_{1}^{CK}, G^{x})$ and T a forcing condition. The relation $T ⊩_{x} φ$ is defined by induction:

If φ is ranked, then $T ⊩_{x} φ$ iff for every $G \in [T]$ , $M (ω_{1}^{CK}, G^{x})$ satisfies φ.

If φ is unranked and $φ = (\exists n) ψ (n)$ , then $T ⊩ φ$ iff there is an $n \in ω$ such that $T ⊩ ψ (\underline{n})$ .

If φ is unranked and $φ = (\exists X^{δ}) ψ (X^{δ})$ , then $T ⊩_{x} φ$ iff there is a term $H (n)$ of rank at most δ such that $T ⊩_{x} φ (\hat{n} H (n))$ .

If φ is unranked and $φ = (\exists X) ψ (X)$ , then $T ⊩_{x} φ$ iff there is a $δ < ω_{1}^{CK}$ such that $T ⊩_{x} (\exists X^{δ}) ψ (X^{δ})$ .

If φ is unranked and $φ = ψ_{1} \land ψ_{2}$ , then $T ⊩_{x} φ$ iff $T ⊩_{x} ψ_{1}$ and $T ⊩_{x} ψ_{2}$ .

If φ is unranked and $φ = \neg ψ$ , then $T ⊩_{x} φ$ iff for all $S \in P$ extending T, $\neg S ⊩_{x} ψ$ .

Notation.
Formulas of our forcing languages are denoted φ, ψ, and occasionally by $H (n)$ for a ranked formula with only one free variable, n, which is a natural number variable.

As $⊩_{x}$ only holds between forcing conditions and sentences in $L (ω_{1}^{CK}, G^{x})$ , the x will be omitted from the ⊩ if it has been declared from which language the sentences come.

It is standard to define forcing to be equal to truth for atomic formulas of a forcing language. However, for this construction all ranked formulas are considered at this ground level and thus forcing is defined to be equal to truth for all of them. This definition obscures the fact, which will need to establish later, that given a condition T and a sentence φ there is an extension of T deciding φ.
Definition 3.13 (Generic sequence).

A sequence ${T_{i} : i \in ω}$ of elements of $P$ is $L (ω_{1}^{CK}, G^{x})$ -generic if $T_{i + 1} ⩽_{P} T_{i}$ for each i, and for every $φ \in L (ω_{1}^{CK}, G^{x})$ there is an i such that $T_{i}$ forces either φ or $\neg φ$ . The sequence is generic if it is generic for each $x \in L ∖ {⊤}$ .

Observe that if ${T_{i} : i \in ω}$ is generic, then it meets each dense set $\begin{matrix} D_{n} = {T \in P : T (\emptyset) (n) ↓}, \end{matrix}$ and so there is a unique $G \in ⋂_{i \in ω} [T_{i}]$ . Such a $G$ is called the generic.

Lemma 3.14 (Standard lemmas).

Let T be a condition, $x \in L ∖ {⊤}$ , and $φ \in L (ω_{1}^{CK}, G^{x})$ . Then the following hold:

(Consistency) $T ⊮ φ \land \neg φ$ .

(Extension) If S extends T and $T ⊩ φ$ , then $S ⊩ φ$ .

(Density) There is an S extending T deciding φ (i.e., S either forces φ or forces its negation).

(Forcing and truth) If ${T_{i} : i \in ω}$ is x-generic and $G$ is the generic object, then $M (ω_{1}^{CK}, G^{x}) ⊧ φ$ iff there is an i such that $T_{i} ⊩ φ$ .

Proof of consistency and extension properties.
First the consistency property: Suppose φ is ranked. Then it follows from the fact that $M (ω_{1}^{CK}, G^{x}) ⊭ φ \land \neg φ$ that T does not force both φ and its negation. If φ is unranked, then the definition of forcing for negation implies that T does not force both φ and its negation.

For the extension property; if φ is ranked and $S ⩽_{P} T$ , then $[S] \subseteq [T]$ , consequently, if every branch of T satisfies φ, then every branch of S does too, and so $S ⊩ φ$ . If φ is unranked, the proof proceeds by induction on the full ordinal rank of φ. Details can be found in Chapter IV Section 4 of Sacks [7]. □

The inductive step in a standard proof of the density property goes through as normal (using the definition of forcing for negation). The issue is with the base case: It is not clear that given a condition that there is a refinement such that every branch satisfies a particular ranked formula. To show the existence of such a condition the, so called, fusion property of trees must be established. There is also the concern of coding unnecessarily at the root.

Before establishing the fusion lemma, some technical facts about the forcing relation:
Lemma 3.15.
The relation $T ⊩ φ$ restricted to $Σ_{1}^{1}$ sentences $φ \in L (ω_{1}^{CK}, G^{x})$ is $Π_{1}^{1}$ .
Proof.
This situation is only slightly different from that in Sacks Chapter IV, Lemma 4.2. The notion of tree and of extension are slightly different, but they are all uniformly arithmetic in codes for the trees and so the complexity has not increased. □
Definition 3.16.
Let $σ \in \prod_{i = 0}^{l} Θ_{i}$ be a string and $x \in L ∖ {⊤}$ . The x-safe version of σ, written $σ_{x}$ , is defined by taking each $n < | σ |$ such that $σ (n) = α \in C$ and defining $σ_{x} (n) = β$ where $β \in Θ_{0} ∖ C$ is the member of the lattice table which agrees with α modulo x, but is not coding, and otherwise not changing σ. (There may be more than once such β, so for each $x \in L ∖ {⊤}$ and coding α pick a particular β and always use that.) Observe that $σ \equiv_{x} σ_{x}$ .

If T is a condition and S extends T then the x-safe version of S with respect to T is the condition $S^{T (σ_{x})}$ , where σ is the string such that $T (σ) = S (\emptyset)$ , and $σ_{x}$ is its x-safe version. Note that ${G^{x} : G \in [S]} = {G^{x} : G \in [S^{T (σ_{x})}]}$ (as T preserves congruences, and so $T (σ) \equiv_{x} T (σ_{x})$ ). Also note the x-safe version of S with respect to T does no more root-coding than T (as $T (σ_{x}) = S^{T (σ_{x})} (\emptyset)$ , $σ_{x}$ does no coding, and T is branch-coding-free).
Lemma 3.17.
Let S and $S^{'}$ be conditions that have the same branches modulo x (i.e., ${G^{x} : G \in S} = {G^{x} : G \in S^{'}}$ ), and let φ be a sentence of $L (ω_{1}^{CK}, G^{x})$ . Then $S ⊩ φ$ iff $S^{'} ⊩ φ$ . Hence, in particular, if there is an extension S of T forcing a sentence, then there is an extension of T forcing that sentence which does no more root-coding than T: namely, the x-safe version of S.
Proof.
Base case, φ is ranked: By the definition of forcing for ranked formulas, as the branches of S and the branches of $S^{'}$ are the same modulo x, then every branch of S satisfies φ iff every branch of $S^{'}$ does.

Inductive step: If $φ = ψ_{1} \land ψ_{2}$ , then $S ⊩ φ$ iff $S ⊩ ψ_{1}$ and $S ⊩ ψ_{2}$ iff (by induction) $S^{'} ⊩ ψ_{1}$ and $S^{'} ⊩ ψ_{2}$ iff $S^{'} ⊩ ψ_{i} \land ψ_{2}$ .

If $φ = (\exists x) ψ (x)$ then $S ⊩ φ$ iff there is an n such that $S ⊩ ψ (\underline{n})$ iff there is an n such that $S^{'} ⊩ ψ (\underline{n})$ iff $S^{'} ⊩ (\exists x) ψ (x)$ .

For $φ = (\exists X^{δ}) ψ (X^{δ})$ then the proof is similar to the natural number existential, but with a witnessing formula $H$ of rank at most δ in place of n.

If $φ = (\exists X) ψ (X)$ then $S ⊩ φ$ iff there is a $δ < ω_{1}^{CK}$ such that $S ⊩ (\exists X^{δ}) ψ (X^{δ})$ iff there is a $δ < ω_{1}^{CK}$ such that $S^{'} ⊩ (\exists X^{δ}) ψ (X^{δ})$ iff $S^{'} ⊩ φ$ .

The case when $φ = \neg ψ$ is somewhat trickier, what is needed is to be able to transform extensions R of S which force ψ into extensions $R^{'}$ of $S^{'}$ also forcing ψ. By the inductive hypothesis, it suffices to ensure that the branches of $R^{'}$ are the same as those of R modulo x.

Given $R ⩽_{P} S$ define $R^{'} (σ) = S^{'} (τ_{σ})$ where $τ_{σ}$ is the (unique) string such that $R (σ) = S (τ_{σ})$ . $R^{'}$ is hyperarithmetic as R, S and $S^{'}$ are, and, furthermore, $R^{'}$ is a branch-coding-free, congruence-respecting, and uniform subtree of $S^{'}$ , as R is for S. It remains to be shown that the branches of R and $R^{'}$ are the same modulo x.

Claim: For each level l the height of S and of $S^{'}$ are the same.

The height of the 0th levels of S and $S^{'}$ are, respectively $| S {(\emptyset)}^{⌢} π_{0}^{S} |$ and $| S^{'} {(\emptyset)}^{⌢} π_{0}^{S^{'}} |$ . Every branch on S extends $S {(\emptyset)}^{⌢} π_{0}^{S}$ , and so every branch on $S^{'}$ must extend this string modulo x. By the implementation of the nonorder property, the different branches of S at this level all disagree at the $| S {(\emptyset)}^{⌢} π_{0}^{S} |$ th place. If $x = ⊥$ then there is only one branch on S, $S^{'}$ , R, $R^{'}$ : The constant 0 branch, and so the claim is shown. Otherwise $x \neq ⊥$ , and there are α, β which disagree modulo x, and so there are branches of S which disagree at the $| S {(\emptyset)}^{⌢} π_{0}^{S} |$ place, modulo x.

This must be reflected in $S^{'}$ , and so there is splitting at the $| S {(\emptyset)}^{⌢} π_{0}^{S^{'}} |$ th place on $S^{'}$ therefore, the height of $S^{'}$ at level 0 must be less than or equal to that of S. Interchanging S and $S^{'}$ in this argument shows the heights at the root must be equal.

Now proceed inductively: For σ of length l assume $| S {(σ)}^{⌢} π_{l}^{S} | = | S^{'} {(σ)}^{⌢} π_{l}^{S^{'}} |$ , hence, it suffices to show that $| ρ_{l, α}^{S ⌢} π_{l + 1}^{S} | = | ρ_{l, α}^{S^{'} ⌢} π_{l + 1}^{S^{'}} |$ . But the argument is similar to the base case: there are mod x disagreements in branches of S at $| S {(σ)}^{⌢} {π_{l}^{S}}^{⌢} {ρ_{α, l}^{S}}^{⌢} π_{l}^{S} |$ , consequently, there must be mod x disagreements in branches of $S^{'}$ at this place too. Hence, the height of the $l + 1$ level of $S^{'}$ is at most the height of the $l + 1$ st level of S. Interchanging S and $S^{'}$ shows they must be equal.

Claim: For every σ and every level l, $S {(σ)}^{⌢} π_{l}^{S} \equiv_{x} S^{'} {(σ)}^{⌢} π_{l}^{S^{'}}$ .

Every branch of S extends $S {(\emptyset)}^{⌢} π_{0}^{S}$ and so they all agree modulo x. This is reflected in the branches of $S^{'}$ and so $S^{'} {(\emptyset)}^{⌢} π_{0}^{S^{'}}$ must agree with the initial segment modulo x.

Then, inductively, if it is true up to level l, consider $S {(σ)}^{⌢} {π_{l}^{S}}^{⌢} {ρ_{l, α}^{S}}^{⌢} π_{l + 1}^{S}$ for any $α \in Θ_{l}$ . By induction, $S {(σ)}^{⌢} π_{l}^{S}$ and $S^{'} {(σ)}^{⌢} π_{l}^{S^{'}}$ agree modulo x and by the last claim they are of the same height. Then, by the implementation of nonorder, the first place where this string is undefined but $S {(σ)}^{⌢} {π_{l}^{S}}^{⌢} {ρ_{l, α}^{S}}^{⌢} π_{l + 1}^{S}$ is defined takes value α. As S is congruence-respecting, then if $α \equiv_{x} β$ , then $ρ_{l, β}^{S} \equiv_{x} ρ_{l, α}^{S}$ , and so every branch of S (and so of $S^{'}$ ) which looks like α (modulo x) at this place looks the same for the rest of the string $ρ_{l, α}^{S}$ modulo x. Consequently, $ρ_{l, α}^{S^{'}}$ must agree modulo x with $ρ_{l, α}^{S}$ , because $S^{'}$ is also congruence-respecting.

Claim: The R and $R^{'}$ above have the same branches modulo x.

If $G \in [R]$ is a path, there is some sequence ${σ_{i} : i \in ω}$ of compatible strings such that $R (σ_{i})$ converges to G, and $| σ_{i} | = i$ . As R is a subtree of S, there is a sequence of compatible strings ${τ_{i} : i \in ω}$ such that $S (τ_{i}) = R (σ_{i})$ . By the previous claim, $S^{'} (τ_{i}) \equiv_{x} S (τ_{i})$ , and so $\begin{matrix} R^{'} (σ_{i}) = S^{'} (τ_{i}) \equiv_{x} S (τ_{i}) = R (σ_{i}) \end{matrix}$ and so there is some $G^{'} \in [R^{'}]$ such that $G \equiv_{x} G^{'}$ . Interchanging the role of R and $R^{'}$ shows that every branch of $R^{'}$ has a corresponding branch in R which agrees modulo x, hence the branches are the same modulo x as required.

So, suppose $S^{'} ⊩ \neg ψ$ , then there is no $R^{'} ⩽ S^{'}$ such that $R^{'} ⊩ ψ$ . If there were $R ⩽ S$ forcing ψ, then we can construct $R^{'} ⩽ S^{'}$ which forces ψ (as we can construct $R^{'}$ with the same branches as R modulo x and so, by induction, forcing ψ). Consequently, S must force $\neg ψ$ , which completes the proof. □
Lemma 3.18 (Fusion).

Let ${φ_{i} : i \in ω}$ be a hyperarithmetic sequence of $Σ_{1}^{1}$ formulas of $L (ω_{1}^{CK}, G^{x})$ , and let T be a condition such that for every $S ⩽_{P} T$ and every $j \in ω$ , there is an $R ⩽_{P} S$ such that $R ⊩ φ_{j}$ . Then there is a condition $V ⩽_{P} T$ forcing each $φ_{i}$ which does no more root coding than T.

Proof.
Fix such a sequence ${φ_{i} : i \in ω}$ and a condition T. By the previous lemma, for every $S ⩽_{P} T$ and $i \in ω$ , as there is an $R ⩽_{P} S$ forcing φ, there is one forcing φ and doing no more root-coding than S. Consider the predicate
$R \in P$ , refines $S \in P$ , does no more root-coding than S, and forces $φ_{i}$ .
As $P$ and the forcing relation are $Π_{1}^{1}$ , and the other clauses are arithmetic, this predicate is uniformly $Π_{1}^{1}$ in R, S, i. By Krisel’s uniformization theorem, there is a partial $Π_{1}^{1}$ function which produces R in terms of S and i. Call this function $R (S, i)$ . By assumption, R is total on the conditions S extending T.

We want to construct a single condition V that extends T and forces each $φ_{i}$ simultaneously. We construct V level by level as well as auxiliary conditions $U_{j}^{l}$ where $l \in ω$ is a level, and j varies between 0 and the number $m (l)$ , which is one less than the number of branches of T at level l (i.e., $m (l) = \prod_{k = 0}^{l} | Θ_{k} | - 1$ ). Fix a simultaneous hyperarithmetic enumeration $α_{k}^{l}$ of each $Θ_{l}$ , and order strings lexicographically.

Stage 0: $V (\emptyset) = T (\emptyset)$ .

Define $U_{0}^{0}$ to be $R (T_{α_{0}^{0}}, 0)$ , a subtree of $T_{α_{0}^{0}}$ that forces $φ_{0}$ and does no more root-coding than $T_{α_{0}^{0}}$ . By the uniformity of T, ${(U_{0}^{0})}^{T (α_{1}^{0})}$ is a subtree of $T_{α_{1}^{0}}$ and so of T. Define $U_{1}^{0} = R ({(U_{0}^{0})}^{T (α_{1}^{0})}, 0)$ , and continue in this fashion across the level defining $U_{k + 1}^{0} = R ({(U_{k}^{0})}^{T (α_{k}^{0})}, 0)$ . By uniformity, ${(U_{m (0)}^{0})}^{T (α_{k}^{0})}$ is a subtree of $U_{k}^{0}$ for every k and, as such, must force $φ_{0}$ .

Define $V (α) = {(U_{m (0)}^{0})}^{T (α)} (\emptyset)$ for each $α \in Θ_{0}$ . By the uniformity of both T and $U_{m (0)}^{0}$ , V, as defined so far, is uniform and congruence-respecting.

To see it is branch-coding-free, observe that if $V (α) (n) = β \in C$ and $n ⩾ | V (\emptyset) |$ , then, by definition, ${(U_{m (0)}^{0})}^{T (α)} (\emptyset) (n) = β$ . If $n < | T (α) |$ , then ${(U_{m (0)}^{0})}^{T (α)} (\emptyset) (n) = T (α) (n)$ , and as T is branch-coding-free, this means that $α = β$ and n is precisely $| T {(\emptyset)}^{⌢} π_{0}^{T} |$ , which is not unnecessary coding. Otherwise, $n ⩾ | T (α) |$ . Let k be the first stage such that $U_{k}^{0} (\emptyset) (n) ↓$ . $U_{0}^{0}$ does no more root-coding than $T (α_{0}^{0})$ , by the choice of R, and so, inductively across the level, $U_{j + 1}^{0}$ does no more root-coding than ${(U_{j}^{0})}^{T (α_{j + 1}^{0})}$ which does no more root-coding than $T_{α_{j + 1}^{0}}$ . Therefore, $β = α_{k}^{0}$ and n must be precisely $| T {(α_{k}^{0})}^{⌢} π_{1}^{T} |$ , which is not unnecessary coding.

Stage $l > 0$ : Assume V is defined up to level l, and so far it is branch-coding-free, congruence-respecting, and uniform and $U_{m (l - 1)}^{l - 1}$ is a tree which, by induction, is a forcing condition that is a subtree of $T_{τ}$ where τ is last string in our uniform enumeration of strings of length l and has root at least as long as the height of V so far.

Starting with the least string $σ^{⌢} α$ of length l set $U_{0}^{l} = R ({(U_{m (l - 1)}^{l - 1})}_{{0^{l - 1}}^{⌢} α}^{V (σ^{⌢} α)}, l)$ ; then given $U_{k}^{l}$ and the $k + 1$ th string $σ^{⌢} α$ define $\begin{matrix} U_{k + 1}^{l} = R ({(U_{k + 1}^{l})}^{S (σ^{⌢} α)}, l) . \end{matrix}$ At the end $U_{m (l)}^{l}$ is defined, and by a similar argument as in the base case, if $σ^{⌢} α$ is the kth string of length l then ${(U_{m (l)}^{l})}^{U_{k}^{l} (\emptyset)}$ is a subtree of $U_{k}^{l}$ which forces $φ_{l}$ . So, let $\begin{matrix} V (σ^{⌢} α) = {(U_{m (l)}^{l})}^{U_{k}^{l} (\emptyset)} (\emptyset) . \end{matrix}$ This preserves that V is (so far) branch-coding-free, congruence-preserving, and uniform, as each $U^{l}$ is. Also the root of $U_{m (l)}^{l}$ is sufficiently long and has the various other properties assumed by the induction.

This completes the inductive construction of V, which is a forcing condition extending T doing no more root-coding. V forces each $φ_{i}$ as for every string σ of length i every path on V extending $V (σ)$ is a path on one of the $U_{k}^{i}$ s, and so, by construction of the Us and the fact that the formulas are $Σ_{1}^{1}$ , every path on V makes $φ_{i}$ true, and so $φ_{i}$ is forced by V. □

With the fusion lemma in hand, the proofs of the standard lemmas regarding the forcing relation can be completed.
Proof of the density property.
Let φ be a sentence in $L (ω_{1}^{CK}, G^{x})$ and T a forcing condition. If φ is unranked, then there is an $S ⩽_{P} T$ deciding φ, by the definition for forcing the negation of an unranked formula. By choosing the x-safe version of S, it is ensured that S does no more root-coding than T.

If φ is ranked, then proceed by induction on the full ordinal rank and logical complexity of the formula. To decide atomic sentences, pick $T_{σ}$ for some sufficiently long σ. Note that σ can be chosen so as to do no more root-coding.

The induction step for ∧ and ¬ are standard; the difficulty comes with existential quantifiers. For instance, if $φ = (\exists X^{δ}) ψ (X^{δ})$ , then let $H_{i} (n)$ be an effective enumeration of all formulas of rank at most δ whose sole free variable is n. If there is an i and an $S ⩽_{P} T$ such that $S ⊩ ψ (\hat{n} H_{i} (n))$ , then $S ⊩ ψ$ , and choosing the x-safe version of S does no more root-coding.

Otherwise, for each $S ⩽_{P} T$ and i, $S ⊮ φ (\hat{n} H (n))$ , and so, by induction, for each i and $S ⩽_{P} T$ there is an $R ⩽_{P} S$ such that $R ⊩ \neg ψ (\hat{n} H (n))$ .

Now apply the fusion lemma to the sequence $\neg ψ (\hat{n} H_{i} (n))$ to find an $S ⩽_{P} T$ forcing each $\neg ψ (\hat{n} H_{i} (n))$ , and so $S ⊩ \neg ψ$ . Furthermore, choose S to do no more coding, as the fusion lemma allows this.

The case for a natural number existential is similar. Observe that each extension could be chosen to do no more root-coding. □
Proof that truth is forcing.
Suppose ${T_{i} : i \in ω}$ is x-generic and $G$ is the generic object. Firstly, let φ be a ranked formula. Then, as the sequence is x-generic, there is an i such that $T_{i}$ decides φ. By the definition of forcing for ranked formulas, either every branch of $T_{i}$ satisfies φ or every branch satisfies its negation. In particular, as $G \in [T_{i}]$ , if $G^{x}$ satisfies φ then every branch does, and if $G^{x}$ satisfies its negation, then every branch does.

If φ is unranked, then proceed by induction on the logical complexity of φ. The proof, from here, is standard. □
Lemma 3.19.
Let $G$ be x-generic. Then $G^{x}$ preserves $ω_{1}^{CK}$ .
Proof.
As in Chapter IV Section 5 of Sacks [7], the fusion lemma provides the proof. □

Observe that a generic sequence can be constructed by, step-by-step, extending the current condition to decide the next sentence without increasing the root-coding of the current condition. Now the various properties needed of the embedding are proved.
3.4. Producing almost-initial-segments

A generic sequence ${T_{i} : i \in ω}$ must be constructed such that the generic object $G$ induces an embedding $x \mapsto degree (G^{x})$ that preserves ⊑, ⋢, ⊔, ⊓, sends $L ∖ {⊤}$ to an initial segment, and sends ⊤ to $O$ .

Notation.
For each $x \in L ∖ {⊤}$ , number the ranked terms $H (t)$ of $L (ω_{1}^{CK}, G^{x})$ by ordinals $δ < ω_{1}^{CK}$ and denote the characteristic function of the set they stand for by ${δ}^{G^{x}}$ (of course, ${δ}^{G^{x}}$ depends on a choice of forcing condition and need not be total).
Definition 3.20.
A condition T decides ${δ}^{G^{x}}$ via q (a map into ${0, 1}$ ), if for every n and $σ \in dom (T)$ of length l, $T_{σ} ⊩ {δ}^{G^{x}} (\underline{l}) = \underline{q (n, σ)}$ . We say T decides ${δ}^{G^{x}}$ if it decides it for some q.
Lemma 3.21.
Let T be a condition which decides ${δ}^{G^{x}}$ via q. Then q is hyperarithmetic.
Proof.
The forcing relation is uniformly $Π_{1}^{1}$ (as the formulas are ranked), and so q is a total $Π_{1}^{1}$ function. Consequently, q is $Δ_{1}^{1}$ . □
Lemma 3.22.
Let T be a condition, $x \in L$ , and $δ < ω_{1}^{CK}$ . Then there is an $S ⩽_{P} T$ which decides ${δ}^{G^{x}}$ , and does not more root-coding than T.
Proof.
This follows from the coding-free fusion lemma. □

As the lattice representation ${Θ_{i} : i \in ω}$ is recursive and each $Θ_{i}$ is a USL table, the map, $x \mapsto degree (G^{x})$ , preserves ⊑ and ⊔. It is additionally needed that the map be injective and preserve ⋢. Note that injectivity follows from preservation of ⋢.

It suffices to show for $x ⋢ y$ that $G^{x}$ is not hyperarithmetic in $G^{y}$ . As $G^{y}$ preserves $ω_{1}^{CK}$ for each $y \neq ⊤$ , it is enough that $G_{x} \notin M (ω_{1}^{CK}, G^{y})$ , i.e., that there is no term ${δ}^{G^{y}}$ in the language $L (ω_{1}^{CK}, G^{y})$ which defines $G^{x}$ . Clearly, $y \neq ⊤$ as there is no corresponding x not below ⊤.
Lemma 3.23 (Diagonalization).

Let $x, y \in L$ satisfy $x ⋢_{L} y$ , $δ < ω_{1}^{CK}$ , and T be a condition. Then there is an $n \in ω$ and an extension of T which does no more root-coding than T, decides the values of $G^{x} (n)$ and of ${δ}^{G^{y}} (n)$ , and decides them to be different.

Proof.
Firstly, as y is not above x, $y \neq ⊤$ , so $L (ω_{1}^{CK}, G^{y})$ and $M (ω_{1}^{CK}, G^{y})$ are defined. Replacing T with an extension if necessary, it is given than T decided ${δ}^{G^{y}}$ via q. Fix $α, β \in Θ_{0} ∖ C$ differentiating x and y, i.e., $α \equiv_{y} β$ yet $α ≢_{x} β$ .

By the uniformity of T, there is a string π such that $T (α) \supseteq T {(\emptyset)}^{⌢} π^{⌢} α$ and $T (β) \supseteq T {(\emptyset)}^{⌢} π^{⌢} β$ . In particular, if $n = | T {(\emptyset)}^{⌢} π |$ , then $T_{α} (\emptyset) (n) = α$ and $T_{β} (\emptyset) (n) = β$ . Consequently, every branch of $T_{α}$ disagrees modulo x with every branch of $T_{β}$ at n.

Let $α^{n}$ be n many copies of α and define $β^{n}$ similarly. As T decides ${δ}^{G^{y}}$ via q, $\begin{matrix} T_{α^{n}} ⊩ {δ}^{G^{y}} (n) = q (n, α^{n}) and T_{β^{n}} ⊩ {δ}^{G^{y}} (n) = q (n, β^{n}) . \end{matrix}$ It follows that $q (n, α^{n}) = q (n, β^{n})$ . To see this, note that as $α \equiv_{y} β$ then $T_{α^{n}}$ and $T_{β^{n}}$ have the same branches modulo y. This implies, by Lemma 3.17, that $T_{α^{n}}$ and $T_{β^{n}}$ force precisely the same sentences of $L (ω_{1}^{CK}, G^{y})$ , which establishes the claim.

In summary, $T_{α^{n}}$ and $T_{β^{n}}$ force the same value of ${δ}^{G^{y}} (n)$ yet force different values of $G^{x} (n)$ . As such, at least one of $T_{α^{n}}$ or $T_{β^{n}}$ diagonalizes against the δth reduction. Neither tree does more root-coding than T, as T is branch coding free and neither α nor β are in C, hence the existence of the desired condition is established. □

So, by repeatedly applying the above Lemma, the map is forced to be an uppersemilattice embedding. Provided the image of the map is also an almost-initial-segment, meets are preserved for free. Hence it needs to established that splitting subtrees exist, which is considerably more complicated than anything done so far.
Definition 3.24.
For each reduction δ and condition T deciding ${δ}^{G^{x}}$ via q, σ and τ (of the same length) are $(δ, x)$ -splitting on T (modulo y) if ( $σ \equiv_{y} τ$ and) there is an $n ⩽ | σ |$ such that $q (n, σ ↾ n) \neq q (n, τ ↾ n)$ .
Lemma 3.25.
Let δ be a reduction and T a condition deciding ${δ}^{G^{x}}$ (where $x \neq ⊤$ ). There is a ρ such that the set $\begin{matrix} Sp (ρ) = {y \in L : there are no σ, τ that (δ, x) -split on T_{ρ} modulo y} \end{matrix}$ is maximal. Moreover, this set is closed under meet, and so has a least element, and ρ can be chosen to do no coding.
Proof.
As $L$ is finite there is clearly a ρ such that $Sp (ρ)$ is maximal. It is shown that if ρ is replaced by its x-safe version, then $Sp (ρ_{x})$ is still maximal. It suffices to observe that, as $T_{ρ}$ and $T_{ρ_{x}}$ have the same branches modulo x, then they both decide ${δ}^{G^{x}}$ via the same map q. Hence, σ, τ $(δ, x)$ -split on $T_{ρ}$ iff they $(δ, x)$ -split on $T_{ρ_{x}}$ . Thus, $Sp (ρ) = Sp (ρ_{x})$ , and one is maximal iff the other is.

Now it is shown that $Sp (ρ)$ is closed under meet. Suppose $y, z \in Sp (ρ)$ , it suffices to show that there are no $(δ, x)$ -splits on $T_{ρ^{⌢} 0}$ modulo $y ⊓ z$ (here ρ is extended by one place for technical reasons). Suppose there was such a split σ and τ. By the existence of meet-interpolants there are $\hat{γ_{1}}, \hat{γ_{2}}, \hat{γ_{3}} \in \prod_{i = 1}^{| σ | + 1} Θ_{i}$ such that for each $0 < j < | σ | + 1$ $\hat{γ_{1}} (j)$ , $\hat{γ_{2}} (j)$ , $\hat{γ_{3}} (j)$ are meet interpolants for $σ (j)$ and $τ (j)$ . In particular, $\begin{matrix} σ \equiv_{y} \hat{γ_{1}} \equiv_{z} \hat{γ_{2}} \equiv_{y} \hat{γ_{3}} \equiv_{z} τ . \end{matrix}$ Now as σ and τ form a $(δ, x)$ -split on $T_{ρ^{⌢} 0}$ , then so too do one of the consecutive pairs listed above. But then, supposing it is the first pair, $0^{⌢} σ$ and $0^{⌢} \hat{γ_{1}}$ forms a $(δ, x)$ -split modulo y, contradicting the fact that $y \in Sp (ρ)$ . The other pairs are similar, and so there are no $y ⊓ z$ splits on $T_{ρ}$ as required. □

Using the above lemma splitting subtrees are constructed:
Lemma 3.26.
Let δ be a reduction, T a condition deciding ${δ}^{G^{x}}$ (where $x \neq ⊤$ ) via q, ρ be a string such that $Sp (ρ)$ is maximal yet ρ does no coding, and z be the least element of $Sp (ρ)$ . Then there is a condition S extending T that does no more root-coding than T such that for any σ, τ if $σ ≢_{z} τ$ then σ and τ $(δ, x)$ -split on S. Such an S is called a $z - (δ, x)$ -splitting tree.
Proof.
Define S inductively. Begin with $S (\emptyset) = T (ρ)$ , which, by choice of ρ, does no more root-coding than T. Now suppose $S (σ) = T (τ_{σ})$ for each σ of length l, then $S (σ^{⌢} α)$ must be defined for all σ and $α \in Θ_{l}$ in a congruence-respecting, branch-coding-free, and uniform fashion across the level.

List the strings of length $l + 1$ as ${σ_{j}}^{⌢} α_{j}$ for $j < m = | \prod_{i = 0}^{l} Θ_{i} |$ . Define by a subinduction on $r < m (m - 1) / 2$ strings $ρ_{j, r}$ (simultaneously for $j < m$ ) and set $\begin{matrix} τ_{{σ_{j}}^{⌢} α_{j}} = {τ_{σ_{j}}}^{⌢} {α_{j}}^{⌢} {ρ_{j, 0}}^{⌢} \dots^{⌢} ρ_{j, m (m + 1) / 2} . \end{matrix}$ Uniformity is maintained by ensuring that $| ρ_{j, r} | = | ρ_{j^{'}, r} |$ for each j, $j^{'}$ ; respecting-congruences is maintained by insisting if $α_{j} \equiv_{y} α_{j^{'}}$ , then $ρ_{j, r} \equiv_{y} ρ_{j^{'}, r}$ for each r and y; and no unnecessary coding is done by ensuring that each $ρ_{j, r}$ never takes on a coding value. Provided this is all effective, the object produced will be a condition.

By induction on $r < m (m + 1) / 2$ suppose ${τ_{j}}^{⌢} {α_{j}}^{⌢} {ρ_{j, 0}}^{⌢} \dots^{⌢} ρ_{j, r - 1} = ν_{j}$ is given for all $j < m$ . Suppose ${p, q}$ is the pair of distinct numbers both less than m numbered by r. A split corresponding to $α_{p}$ and $α_{q}$ must be forced if necessary. If $α_{p} \equiv_{z} α_{q}$ , then a split is not necessary, and so define $ρ_{j, r} = \emptyset$ for each $j < m$ .

Otherwise, let y be the largest $w \in L$ such that $α_{p} \equiv_{w} α_{q}$ , of course, $z ⋢ y$ . By choice of z, there are σ, τ such that $ν_{p}$ extended by σ and τ, respectively, form a $(δ, x)$ -splitting modulo y on $T_{ρ}$ . Consequently, ${ν_{q}}^{⌢} τ$ must also $(δ, x)$ split with one of ${ν_{p}}^{⌢} σ$ and ${ν_{p}}^{⌢} τ$ . If it splits with ${ν_{p}}^{⌢} τ$ , then we set $ρ_{j, r + 1} = τ_{x}$ the x-safe version of τ. This is uniform and congruence-respecting (because the same extension for each j is picked) and, furthermore, ${ν_{p}}^{⌢} τ_{x}$ and ${ν_{q}}^{⌢} τ_{x}$ still form a $(δ, x)$ -split, because ${ν_{p}}^{⌢} τ_{x} \equiv_{x} {ν_{p}}^{⌢} τ$ , and so they force the same values for ${δ}^{G^{x}}$ wherever defined.

Now suppose ${ν_{q}}^{⌢} τ$ splits with ${ν_{p}}^{⌢} σ$ . If $α_{p} \equiv_{w} α_{q}$ , then $w ⊑ y$ by maximality of y, and so $σ \equiv_{w} τ$ , as $σ \equiv_{y} τ$ . Pick homogeneity interpolants $γ_{0} (s)$ , $γ_{1} (s)$ in $Θ_{s + 1}$ and $L$ -homomorphisms $f_{s}, g_{s}, h_{s} : Θ_{s} \to Θ_{s + 1}$ such that $\begin{matrix} f_{s} : α_{p}, α_{q} \mapsto σ (s), γ_{1} (s), g_{s} : α_{p}, α_{q} \mapsto γ_{0} (s), γ_{1} (s), h_{s} : α_{p}, α_{q} \mapsto γ_{0} (s), τ (s) . \end{matrix}$ As ${ν_{p}}^{⌢} σ$ and ${ν_{q}}^{⌢} τ$ $(δ, x)$ -split on $T_{ρ}$ , one of the pairs ${ν_{p}}^{⌢} σ$ , ${ν_{q}}^{⌢} \hat{γ_{1}}$ , or ${ν_{p}}^{⌢} \hat{γ_{0}}$ , ${ν_{q}}^{⌢} \hat{γ_{1}}$ , or ${ν_{p}}^{⌢} \hat{γ_{0}}$ , ${ν_{q}}^{⌢} τ$ must $(δ, x)$ -split on $T_{ρ}$ too. Set $ρ_{j, r + 1} (s) = f_{s} (α_{j})$ or $g_{s} (α_{j})$ or $h_{s} (α_{j})$ corresponding to which pair splits. This is uniform as $ρ_{j, r + 1}$ depends only on $α_{j}$ , and, as each $f_{s}$ , $g_{s}$ , $h_{s}$ are $L$ -homomorphisms, we respect-congruences.

The final thing to show is that there is no unnecessary coding. As ${Θ_{i} : i \in ω}$ is coding-ready, then it is acceptable for A, so, by definition, $f_{s} (α) \in C$ implies that $α = σ (s)$ or $α = τ (s)$ (and the same for $g_{s}$ , $h_{s}$ ). So, it suffices to show that σ and τ which can be chosen to do no coding.

As $ν_{p} = {τ_{σ_{j}}}^{⌢} {α_{j}}^{⌢} {ρ_{j, 0}}^{⌢} \dots^{⌢} ρ_{j, r - 1}$ , then $| ν_{p} | > 0$ ; therefore, the σ, τ we are trying to pick live in $\prod_{i = k}^{i = k^{'}} Θ_{i}$ for some $k^{'} > k > 0$ . Consequently, if $σ (s) \in C$ , then $σ (s) \in Θ_{0} \subseteq Θ_{k + s}^{}$ (similarly for $τ (s)$ ), and so, by the definition of acceptable for A, there are $σ^{'} (s)$ and $τ^{'} (s) \in Θ_{k + s} ∖ Θ_{k + s}^{}$ such that $\begin{matrix} σ (s) \equiv_{x^{'}} σ^{'} (s), τ (s) \equiv_{x^{'}} τ^{'} (s), and for all w \in L [σ (s) \equiv_{w} τ_{s} \Rightarrow σ^{'} (s) \equiv_{w} τ^{'} (s)] . \end{matrix}$ Picking a coatom $x^{'} > x$ , construct $σ^{'}$ , $τ^{'}$ which do not take coding values and such that $σ^{'} \equiv_{x^{'}} σ$ and $τ^{'} \equiv_{x^{'}} τ$ , and, therefore, which still form a $(δ, x)$ -split on $T_{ρ}$ modulo y. Thus, σ, τ can be chosen to do no coding, and then nothing else can code as ${Θ_{i} : i \in ω}$ is acceptable for A. □
Lemma 3.27.
If T is a $z - (δ, x)$ -splitting tree, then T forces ${δ}^{G^{x}} \equiv_{h} G^{z}$ .
Proof.
Fix $G \in [T]$ . Firstly it is established that $G^{z} ⩾_{h} {δ}^{G^{x}}$ . Pick an n. Using $G^{z}$ find all $σ \in dom (T)$ of length n such that $T (σ) (m) (z) \equiv_{z} G^{z} (m)$ for all $m ⩽ n$ , i.e, narrow down the possible paths through T to those consistent with $G^{z}$ . All these σ are equivalent modulo z, and so each $T_{σ}$ forces the same value of ${δ}^{G^{x}} (n)$ , by the choice of z. As $T (σ)$ is an initial segment of $G$ for one of these σ, then ${δ}^{G^{x}} (n)$ must be the correct value for that σ, and hence, all such σ.

Now the converse. Given ${δ}^{G^{x}}$ consider all $σ, τ \in dom (T)$ of length n. If $σ ≢_{z} τ$ , then σ and τ form a $(δ, x)$ -split on T and so, in particular, $T_{σ}$ and $T_{τ}$ force different values for ${δ}^{G^{x}}$ at some $m < n$ . Thus, of the $\equiv_{z}$ equivalence classes of σs and τs of length n, only the correct one will force the correct value of ${δ}^{G^{x}}$ , so all the incorrect ones can be ruled out, as T and q are hyperarithmetic. This leaving us with a single $\equiv_{z}$ equivalence class, and every member determines the same initial segment of $G$ modulo z, and so the initial segment must be correct modulo z. □

This is the penultimate step on the way to Theorem 2.3: It has been shown that we can construct an embedding of $L$ into $D_{h}$ such that $L ∖ {⊤}$ is an initial segment. This is done by diagonalizing against each hyperarithmetic reduction δ for each pair $x ⋢ y \in L$ and by constructing splitting trees. This is only countably many requirements and so each can be satisfied in turn. Additionally each sentence of $L (ω_{1}^{CK}, G^{x})$ for each $x \in L ∖ {⊤}$ must be decided to preserve $ω_{1}^{CK}$ for each such x.

All of this can be achieved while doing no coding, hence intersperse instructions:

If n is the first place which has not been coded for the pair x, y joining up nontrivially to ⊤, then if $n \in O$ take $T_{g (x, y, 1)}$ and if $n \notin O$ take $T_{g (x, y, 0)}$ as the next condition (where g is the function in the definition of coding set).

This implements the coding scheme, and so $G^{⊤} ⩾_{h} O$ . It needs to be checked that $G^{⊤} ⩽_{h} O$ . It suffices to construct a generic sequence hyperarithmetically in $O$ . But this is only so much checking: The notion of forcing and the extension relation are hyperarithmetic in $O$ , as are the languages $L (ω_{1}^{CK}, G^{x})$ . Also, the various constructions we effected can all be made uniformly hyperarithmetic in $O$ by always picking “least” strings or extensions doing various things, with some fixed hyperarithmetic enumeration of strings.

It may be noted that any set can be coded in for ⊤, and provided that set X is hyperarithmetically above $O$ , then there is a generic $G$ with top element having the same hyperdegree as X.
4. Extending embeddings

This section concerns Theorem 2.4, which says that if $U$ and $V$ are USL^⊤s and $U$ is an almost-initial-segment of $V$ , then every embedding of $U$ into $D_{h} (⩽ O)$ extends to one of $V$ (here, embedding means an injective map, preserving ⊔, mapping ⊥ to the degree of the hyperarithmetic sets, and ⊤ to the degree of $O$ ). The strategy is to prove the result for two special cases and to show that, together, these imply the full result.

Definition 4.1 (Free extension).

Let $U$ be a USL^⊤ and X a set disjoint from $U$ . Then the ⊤-preserving free extension of $U$ by X, written $U [X]$ , is the USL^⊤ with domain $\begin{matrix} V = ((U ∖ {⊤}) \times {[X]}^{< ω}) \cup {⊤}, \end{matrix}$ with the partial order $⊑_{V}$ defined by setting ⊤ to be greater than everything, and declaring $(u_{1}, X_{1}) ⊑_{V} (u_{2}, X_{2})$ for $u_{1}, u_{2} \in U$ and $X_{1}$ , $X_{2}$ finite subsets of X iff $u_{1} ⊑_{U} u_{2}$ and $X_{1} \subseteq X_{2}$ . Its least element is $(⊥, \emptyset)$ , its greatest element is ⊤, and $⊔_{V}$ is defined by $\begin{matrix} (u_{1}, X_{1}) ⊔_{V} (u_{2}, X_{2}) = (u_{1} ⊔_{U} u_{2}, X_{1} \cup X_{2}) \end{matrix}$ provided $u_{1} ⊔_{U} u_{2} \neq ⊤$ and is ⊤ otherwise.

Proposition 4.2.
$V$ , as defined above, is a USL ^⊤ , and there is a natural embedding from $U$ to $V$ taking $⊤_{U}$ to $⊤_{V}$ and taking any other $u \in U ∖ {⊤}$ to $(u, \emptyset)$ , which realizes $U$ as an almost-initial-segment of $V$ .

The verification is completely routine and is omitted.
Notation.
Any structure isomorphic to $U [X]$ will also be called a free extension of $U$ , and $U$ will be identified with its image under the natural embedding above.

Furthermore the “⊤-preserving” will be omitted from “⊤-preserving free extension of $U$ by X”, for brevity.
Definition 4.3 (Simple extension).

Let $U$ and $V$ be USL^⊤s such that $V$ is an extension of $U$ generated over $U$ by one element. Then $V$ is called a simple extension of $U$ .

Observe that if $U$ is finite, then any simple extension of $U$ is also finite, as is any free extension by finitely many free generators.

Theorem 4.4.
Let $U$ be a finite USL ^⊤ and $V$ a finite almost-end-extension. Then $V$ is a ${subUSL}^{⊤}$ of a simple almost-end-extension of a free extension of $U$ . Moreover, the free extension can be chosen with only finitely many free generators, and so the two extensions can be chosen to be finite.

Jockusch and Slaman provide a proof of the above for USLs (without a named greatest element) and the corresponding notion of free and simple extension. Indeed, their proof applies to countable structures (although the extensions chosen must then be countable). This proof follows theirs and also works in the countable case with little adjustment:
Proof.
Let $U$ be an almost-initial-segment of a finite USL $V$ . Enumerate $V ∖ U = {v_{1}, v_{2}, \dots v_{n}}$ , let $A = {a_{1}, \dots, a_{n}}$ be a set of new objects of the same size, and let g be the map taking $v_{i}$ to $a_{i}$ . Define $U_{1} = U [A]$ the free extension of $U$ by A, which is finite, as both $U$ and A are finite. Define a map $h : U_{1} \to V$ by $\begin{matrix} h (x) = \{\begin{matrix} x_{1} ⊔_{V} ⨆_{V} {v_{i} : g (v_{i}) = a_{i} \in A_{1}} & if x = (x_{1}, A_{1}), \\ ⊤ & if x = ⊤ . \end{matrix} \end{matrix}$ It is not hard to check that h is a homomorphism from $U_{1}$ to $V$ (i.e., h preserves the least and greatest elements, $⊔_{U}$ , and $⊑_{U}$ ). Observe that if $x \in U$ , then $h (x) = x$ (considering $U$ as an almost-initial-segment of $U [A]$ ), and if $v \in V ∖ U$ , then $h (g (v)) = v$ .

Let b be a new element, and let $U_{2}^{'}$ be the free extension of $U_{1}$ by ${b}$ (for short, write $(x, b)$ instead of $(x, {b})$ ). Define an equivalence relation ≡ on $U_{2}^{'}$ by $y_{0} \equiv y_{1}$ iff $y_{0} = y_{1}$ , or $\begin{array}{l} (\exists x_{0}, x_{1} \in U_{1}) [y_{0} = (x_{0}, b) and y_{1} = (x_{1}, b) and h (x_{0}) = h (x_{1})], \\ or y_{0} = ⊤_{U_{2}^{'}} and (\exists x_{1} \in U_{1}) [y_{1} = (x_{1}, b) and h (x_{1}) = ⊤_{V}], \\ or y_{1} = ⊤_{U_{2}^{'}} and (\exists x_{0} \in U_{1}) [y_{0} = (x_{0}, b) and h (x_{0}) = ⊤_{V}] . \end{array}$ It is not hard to check that this is an equivalence relation, and that if $x_{0}, x_{1} \in U_{1}$ then $x_{0} \equiv x_{1}$ iff $x_{0} = x_{1}$ , indeed, the only element of $U_{1}$ with a possibly nontrivial ≡ equivalence class is ⊤.

Additionally, ≡ is also a congruence relation for the join structure of $U_{2}^{'}$ , i.e., if $y_{1}, y_{2}, y_{1}^{'}, y_{2}^{'} \in U_{2}^{'}$ and $y_{1} \equiv y_{1}^{'}$ , $y_{2} \equiv y_{2}^{'}$ , then $y_{1} ⊔_{U_{2}^{'}} y_{2} \equiv y_{1}^{'} ⊔_{U_{2}^{'}} y_{2}^{'}$ . The proof is a case analysis:

Case 1, none of the ys are ⊤: In this case each of the ys are of the form $(x, B)$ where $x \in U_{1}$ and $B \subseteq {b}$ ; write $y_{1} = (x_{1}, B_{1})$ , $y_{2} = (x_{2}, B_{2})$ and so on. Now, $\begin{matrix} y_{1} ⊔_{U_{2}^{'}} y_{2} = (x_{1} ⊔_{U_{1}} x_{2}, B_{1} \cup B_{2}) and y_{1}^{'} ⊔_{U_{2}^{'}} y_{2}^{'} = (x_{1}^{'} ⊔_{U_{1}} x_{2}^{'}, B_{1}^{'} \cup B_{2}^{'}) . \end{matrix}$ If each of the Bs are empty, then $y_{1} = y_{1}^{'}$ and $y_{2} = y_{2}^{'}$ and so the joins displayed above are equal, and so trivially equivalent. Otherwise suppose WLOG that $B_{1}$ (and hence, $B_{1}^{'}$ ) are nonempty.

Subcase a, neither $x_{1} ⊔_{U_{1}} x_{2} = ⊤$ nor $x_{1}^{'} ⊔_{U_{1}} x_{2}^{'} = ⊤$ : In this case it suffices to show that $h (x_{1} ⊔_{U_{1}} x_{2}) = h (x_{1}^{'} ⊔_{U_{1}} x_{2}^{'})$ . It has been observed already that h is a homomorphism; therefore $h (x_{1} ⊔_{U_{1}} x_{2}) = h (x_{1}) ⊔_{V} h (x_{2})$ . The assumption that $y_{1} \equiv y_{1}^{'}$ , $y_{2} \equiv y_{2}^{'}$ implies that $h (x_{1}) = h (x_{1}^{'})$ and $h (x_{2}) = h (x_{2}^{'})$ . Hence, $\begin{matrix} h (x_{1} ⊔_{U_{1}} x_{2}) = h (x_{1}) ⊔_{V} h (x_{2}) = h (x_{1}^{'}) ⊔_{V} h (x_{2}^{'}) = h (x_{1}^{'} ⊔_{U_{1}} x_{2}^{'}), \end{matrix}$ which completes the subcase.

Subcase b, $x_{1} ⊔_{U_{1}} x_{2} = ⊤$ : It suffices to show that either $x_{1}^{'} ⊔_{U_{1}} x_{2}^{'} = ⊤$ or that $h (x_{1}^{'} ⊔_{U_{1}} x_{2}^{'}) = ⊤$ . If $x_{1}^{'} ⊔_{U_{1}} x_{2}^{'} \neq ⊤$ , then, as $h (x_{1}) = h (x_{1}^{'})$ , $h (x_{2}) = h (x_{2}^{'})$ and h is a homomorphism, $\begin{matrix} h (x_{1}^{'} ⊔_{U_{1}} x_{2}^{'}) = h (x_{1}^{'}) ⊔_{V} h (x_{2}^{'}) = h (x_{1}) ⊔_{V} h (x_{2}) = h (x_{1} ⊔_{U_{1}} x_{2}) = ⊤ \end{matrix}$ as required. This also completes the case where $x_{1}^{'} ⊔_{U_{1}} x_{2}^{'} = ⊤$ .

Case 2, $y_{1} = ⊤$ : In this case $y_{1} ⊔_{U_{2}^{'}} y_{2} = ⊤$ , and so, it suffices to show that either $x_{1}^{'} ⊔_{U_{1}} x_{2}^{'} = ⊤$ or $h (x_{1}^{'} ⊔_{U_{1}} x_{2}^{'}) = ⊤$ . If $y_{1}^{'} = ⊤$ then we are done. Otherwise $y_{1}^{'} = (x_{1}^{'}, B_{1}^{'})$ and, as $x_{1} \equiv x_{1}^{'}$ , $h (x_{1}^{'}) = ⊤$ . Therefore, $\begin{matrix} h (x_{1}^{'} ⊔_{U_{1}} x_{2}^{'}) = h (x_{1}^{'}) ⊔_{V} h {(x_{2})}^{'} = ⊤, \end{matrix}$ which concludes this case, as well as the similar cases where one of the ys equals ⊤. Therefore, the claim is proved.

With this, define $U_{2} = U_{2}^{'} / \equiv$ and equip it with $⊔_{U_{2}}$ defined by the action of $⊔_{U_{2}^{'}}$ on the equivalence classes. This induces a (suggestively notated) binary relation $⊑_{U_{2}}$ on $U_{2}$ by $\begin{matrix} [y_{1}] ⊑_{U_{2}} [y_{2}] iff [y_{1}] ⊔_{U_{2}} [y_{2}] = [y_{2}] iff y_{1} ⊔_{U_{2}^{'}} y_{2} \equiv y_{2} . \end{matrix}$ Using an easy yet tedious case analysis as above, it is not hard to see that this is a partial order on $U_{2}$ and that $⊔_{U_{2}}$ is its join operator, and, furthermore, that $[⊤_{U_{2}^{'}}]$ and $[⊥_{U_{2}^{'}}]$ are, respectively, the least and greatest elements. The details are omitted.

The goal is to show that $U_{2}$ is a simple almost-end-extension of $U_{1}$ , or rather, that the natural embedding of $U_{1}$ into $U_{2}$ given by $x \mapsto [(x, \emptyset)]$ realizes $U_{1}$ as an almost-initial-segment and $U_{2}$ is simple over this image. It was already observed that there are no nontrivial ≡ relationships between elements of $U_{1}$ , so the map is injective, and it also preserves ⊤, $⊥_{U_{1}}$ , $⊑_{U_{1}}$ , and $⊔_{U_{1}}$ . It is also necessary that it preserves $⋢_{U_{1}}$ . If $x_{1} ⋢_{U_{1}} x_{2}$ , then $x_{1} ⊔_{U_{1}} x_{2} \neq x_{2}$ , and, as there are no nontrivial ≡ relationships between elements of $U_{1}$ , further $x_{1} ⊔_{U_{1}} x_{2} ≢ x_{2}$ , so $⋢_{U_{1}}$ is preserved.

$U_{2}$ is clearly simple over this image of this embedding (as it is generated by $[(⊥, b)]$ ), so it remains to show $U_{1}$ is an almost-initial-segment. Suppose $x \in U_{1}$ is not ⊤ and $[y] ⊑_{U_{2}} [x]$ for some $y \in U_{2}^{'}$ . It suffices to show that $y \in U_{1}$ . By definition, $y ⊔_{U_{2}^{'}} x \equiv x$ . If $y ⊔_{U_{2}^{'}} x = x$ , then $y ⊑_{U_{2}^{'}} x$ , and, as $U_{1}$ is an almost-initial-segment of $U_{2}^{'}$ , $y \in U_{2}$ . Otherwise, the ≡ relation is nontrivial, but it was already observed that the ≡ equivalence class of x must be trivial, as $x \in U_{1}$ but is not ⊤. Hence, $U_{2}$ is an almost-end-extension as required.

So, we have natural embeddings $U$ into $U_{1}$ into $U_{2}$ both as almost-initial segments. Finally it must be shown that this embedding of $U$ into $U_{2}$ extends to $V$ . The correct map is $\begin{matrix} f (v) = \{\begin{matrix} [⊤] & if v = ⊤, \\ [((v, \emptyset), \emptyset)] & if v \in U ∖ {⊤}, \\ [(g (v), b)] & if v \in V ∖ U . \end{matrix} \end{matrix}$ Clearly, this map extends the natural one of $U$ into $U_{2}$ . It remains to be seen that it is a USL^⊤ embedding of $V$ . The verification of this is another long case analysis as provided previously. The proof of the preservation of ⊔ when one of the elements is in $U$ is provided to guide the reader if they wish to check all the details.

It has been shown that the action of f on $U$ is a USL^⊤ embedding, so it suffices to check that $f (v_{1} ⊔_{V} v_{2}) = f (v_{1}) ⊔_{U_{2}} f (v_{2})$ when (WLOG) $v_{1} \in V ∖ U$ and $v_{2} \in U$ .

Case 1, $v_{1} ⊔_{V} v_{2} = ⊤$ : In this case $f (v_{1} ⊔_{V} v_{2}) = ⊤$ and so it suffices to show that $f (v_{1}) ⊔_{U_{2}} f (v_{2}) = ⊤$ . If $v_{2} = ⊤$ , then the argument is complete, so suppose otherwise. In this case $\begin{array}{l} f (v_{1}) ⊔_{U_{2}} f (v_{2}) & = [(g (v_{1}), b)] ⊔_{U_{2}} [((v_{2}, \emptyset), \emptyset)] \\ = [(g (v_{1}), b) ⊔_{U_{2}^{'}} ((v_{2}, \emptyset), \emptyset)] \\ = [(g (v_{1}) ⊔_{U_{1}} (v_{2}, \emptyset), b)] \end{array}$ to show $(g (v_{1}) ⊔_{U_{1}} (v_{2}, \emptyset), b) \equiv ⊤$ it suffices to show $h (g (v_{1}) ⊔_{U_{1}} (v_{2}, \emptyset)) = ⊤$ . But, of course, $\begin{array}{l} h (g (v_{1}) ⊔_{U_{1}} (v_{2}, \emptyset)) & = h (g (v_{1})) ⊔_{V} h ((v_{2}, \emptyset)) \\ = v_{1} ⊔_{V} v_{2} \\ = ⊤, \end{array}$ as required.

Case 2, $v_{1} ⊔_{V} v_{2} \neq ⊤$ : As V is an almost-end-extension of $U$ , $v_{1} \in V ∖ U$ and $v_{1} ⊔_{V} v_{2} \neq ⊤$ , then this join is strictly a member of $V$ . Hence, the goal is to show that $[(g (v_{1} ⊔_{V} v_{2}), b)] = [(g (v_{1}), b)] ⊔_{U_{2}} f (v_{2})$ . If $v_{2} \in U ∖ {⊤}$ (note it can’t be equal to ⊤), then $f (v_{2}) = [((v_{2}, \emptyset), \emptyset)]$ and so $\begin{matrix} [(g (v_{1}), b)] ⊔_{U_{2}} f (v_{2}) = [(g (v_{1}), b)] ⊔_{U_{2}} [((v_{2}, \emptyset), \emptyset)] = [(g (v_{1}) ⊔_{U_{1}} (v_{2}, \emptyset), b)] . \end{matrix}$ Thus, we want to show that $g (v_{1} ⊔_{V} v_{2}) \equiv g (v_{1}) ⊔_{U_{2}^{'}} (v_{2}, \emptyset)$ , but, quite similarly to the end of Case 1, $h (g (v_{1} ⊔_{V} v_{2})) = h (g (v_{1}) ⊔_{V} (v_{2}, \emptyset)) = v_{1} ⊔_{U_{2}^{'}} v_{2}$ .

Further details are omitted. □

In light of the previous Theorem, it suffices to prove Theorem 2.4 in the cases where $V$ is a finite free extension or a simple extension of $U$ . The free extension results can be proved by Cohen forcing: Let $f : U \to D_{h} (⩽_{h} O)$ be any USL^⊤ embedding and let X be any Cohen real hyperarithmetic in $O$ meeting every dense subset of Cohen forcing which is hyperarithmetic in $f (u)$ for any $u \in L ∖ {⊤}$ . Then, the columns of X are independent over each degree in the image of $U ∖ {⊤}$ , and so, if $V$ is freely generated over $U$ by $v_{1}, \dots, v_{n}$ , then extend f by mapping the generators $v_{i} \mapsto X^{[i]}$ and using the induced map on joins. This extends f to a USL^⊤ embedding of $V$ into $D_{h} (⩽_{h} O)$ (See Sacks Chapter IV Section 3 [7] for an exposition of hyperarithmetical Cohen forcing).

This the focus turns to simple end extensions. There is a further reduction to an even more specialized case. The idea is that if a free extension has the fewest possible ‘positive’ facts $x ⩽ y ⊔ z$ , then the reduction changes the full simple end-extension case to allowing one new positive cupping fact to hold.
Theorem 4.5 (Bounded Posner-Robinson).

Let $a$ , $b$ , $c_{i}$ , $d_{i}$ be degrees in $D_{h} (⩽_{h} O)$ for $i = 1, \dots n$ and let $e_{j} \in D_{h} (< O)$ for $j = 1, \dots, m$ . Then the following holds $\begin{array}{l} (⋀_{i = 1}^{n} [d_{i} ≰_{h} c_{i} & (a ≰_{h} c_{i} or d_{i} ≰_{h} b ⊔_{h} c_{i})]) \\ \to (\exists g < O) [b ⩽ a ⊔_{h} g & ⋀_{i = 1}^{n} d_{i} ≰_{h} c_{i} ⊔_{h} g & ⋀_{j = 1}^{m} g ≰_{h} e_{j}] \end{array}$

Barnes [1] has shown the above result without the bounds on the parameters and the generic object g. The version here, says that if the parameters are sufficiently bounded, then object g can also be bounded.

Suppose the antecedent in the statement of Theorem 4.5 and let $A \in a$ , $B \in b$ , $C_{i} \in c_{i}$ , $D_{i} \in d_{i}$ and $E_{j} \in e_{j}$ be representatives of the degrees. Barnes’s construction uses Kumabe-Slaman forcing to produce a sequence of forcing conditions ${(Φ_{i}, X_{i}) : i \in ω}$ where each $Φ_{i}$ is a finite use monotone Turing functional, and each $X_{i}$ is a finite set of reals. It is shown that $O$ can produce a generic of the correct kind.

The construction is complicated by the disjunction in the antecedent; If $a ≰_{h} c_{i}$ for the pair $(c_{i}, d_{i})$ then i is called an easy case, otherwise it is called a hard case. As there are only finitely many pairs, it can be hard coded into the construction which is are easy and which are hard, so $O$ need not be able to determine this uniformly.

The coding procedure for cupping $a$ above $b$ is to add axioms $(x, y, α)$ to the generic object such that $α \subset A$ and $B (x) = y$ (intuitively, when A is plugged into the generic functional $Φ_{g}$ the characteristic function of B is obtained). Hence, the coding procedure is uniform and recursive in A and B, and, as such, is recursive in $O$ .

For technical reasons, to the easy case is associated the usual Kumabe-Slaman forcing and a forcing language $L_{ω_{1}, ω}^{r} (C_{i})$ , and to the hard case a restricted version of the forcing and the language $L_{ω_{1}, ω}^{r} (B \oplus C_{i})$ . The restricted version of the forcing consists of all the conditions which do not explicitly get the coding procedure wrong. Importantly, the restriction is hyperarithmetic in $A \oplus B$ and so hyperarithmetic in $O$ . Additionally, the languages are recursive in $O^{C_{i}}$ and $O^{B \oplus C_{i}}$ , respectively. As $C_{i}$ does not compute $D_{i}$ in the easy case and $B \oplus C_{i}$ does not compute $D_{i}$ in the hard case, neither of these are equal to $O$ , hence, their hyperjumps are hyperarithmetically equivalent to $O$ , and so the languages of forcing are hyperarithmetic in $O$ .

So, now it is to be shown that $O$ can construct a generic sequence of conditions while maintaining the coding. There will be one sequence ${p_{n} = (Φ_{p_{n}}, X_{p_{n}})}_{i = 0}^{\infty}$ of Kumabe-Slaman conditions called the master sequence. To keep the complexity of the construction down, the reals added to the infinite part of a condition $X$ must be simple. This requires a little extra technical work; roughly speaking, a dense set corresponding to some fact we wish to force about $Φ_{g} \oplus C_{i}$ must be met by extending the condition $(Φ_{p_{n}}, X_{p_{n}})$ . Temporarily “forget” reals $X \in X_{p_{n}}$ that are too complicated to obtain a modified condition $(Φ_{p_{n}}, X_{p_{n}}^{'})$ . Find a simple extension of this condition which forces whichever fact is to be forced, and then reinsert the “forgotten” reals. There is an obvious worry that this new condition need not refine $(Φ_{p_{n}}, X_{p_{n}})$ , so it needs to show that an extension of $(Φ_{p_{n}}, X_{p_{n}}^{'})$ which doesn’t add new axioms to $Φ_{p_{n}}$ which apply to the reals we have forgotten can be found. This procedure is analogous to Barnes’s Lemma 5.4 [1].

Begin with the condition $p_{0} = (\emptyset, \emptyset)$ . Each sentence of our forcing language must be decided. The process depends on whether it is an easy or hard case under consideration. Note that given a real S strictly hyperarithmetic in $O$ and a finite set $X$ of reals each strictly hyperarithmetic in $O$ , that $O$ can uniformly determine which of the $X \in X$ are hyperarithmetic in S. Hence, the “forgetting” procedure mentioned above can be made effective in $O$ . It must be preserved throughout that for each condition $p_{n}$ of our master sequence that each $X \in X_{p_{n}}$ will be strictly hyperarithmetic in $O$ (although their join may not be).

In the easy case Corollary 3.6 in Barnes [1] says that given a sentence φ and a condition $(Φ_{p}, X_{p})$ , there is an extension deciding φ, without messing up the coding, found uniformly in $A \oplus C_{i}^{(α + 1)} \oplus X_{p}$ (where α is an ordinal less than $ω_{1}^{C_{i}} = ω_{1}^{CK}$ which measures the complexity of φ). So suppose there is a condition $p_{n} = (Φ_{p_{n}}, X_{p_{n}})$ such that $Φ_{n}$ has coded correctly so far and $X_{p_{n}}$ does not contain A. Let $p^{'} = (Φ_{p_{n}}, X_{p_{n}}^{'})$ where $X_{p_{n}}^{'}$ is the intersection of $X_{p_{n}}$ with the set of reals which are hyperarithmetic in $C_{i}$ . Extend Corollary 3.6 of Barnes [1] so that the extension can be picked to not add any axioms to any $X \in X_{p_{n}} ∖ X_{p_{n}}^{'}$ . The proof already does this for an arbitrary S which is not $Δ_{0}^{(α + 1)}$ , and the proof for finitely many such S goes through in the same way. As each $X \in X_{p_{n}} ∖ X_{p_{n}}^{'}$ is not hyperarithmetic in $C_{i}$ this result can be applied to those reals. Thus, an extension $q^{'}$ of $p^{'}$ which decides the sentence, such that $q = (Φ_{q^{'}}, X_{q^{'}} \cup X_{p_{n}})$ extends $p_{n}$ , does not interfere with the coding, and each $X \in X_{q^{'}}$ is hyperarithmetic in C is produced. Define $p_{n + 1} = q$ .

In the hard case instead use Corollary 4.5 of Barnes [1](with similar modifications as in the easy case) to forget the reals not hyperarithmetic in $B \oplus C_{i}$ , and find an extension deciding a sentence which is compatible with the starting condition.

It is also necessary to diagonalize against cupping $C_{i}$ above $D_{i}$ (in the hard case instead diagonalize against cupping $B \oplus C_{i}$ above $D_{i}$ ). The relevant results are Corollaries 3.11 and 4.8 in Barnes [1], respectively. Although it is not observed directly in the statements of these Corollaries, it is clear from the proofs that the diagonalizing extension can be found uniformly in (some jump of) the previous condition (where the number of jumps needed is tied nicely to the complexity of the reduction that is being diagonalized against). Consequently, the trick of temporarily forgetting reals which aren’t hyperarithmetic in $C_{i}$ (or $B \oplus C_{i}$ ) implies that a reduction can’t be diagonalized against by forcing nontotality or for by forcing to be incorrect on some fixed input, then hyperarithmetically in $C_{i}$ (or $B \oplus C_{i}$ ) it can be recovered what the current condition determines the outputs of this reduction to be. Hence, the assumption that $D_{i}$ is not hyperarithmetic in $C_{i}$ (or $B \oplus C_{i}$ ) means that any reduction that can’t be diagonalized against won’t turn out to compute $D_{i}$ .

Additionally, $ω_{1}^{C_{i}}$ or $ω_{1}^{B \oplus C_{i}}$ must be preserved, depending on the case. For both, force over nonstandard models $M_{i}$ of ZFC, in particular, force over countable ω-models omitting $ω_{1}^{CK}$ , yet containing $C_{i}$ (or $B \oplus C_{i}$ ). Harrington, Shore, and Slaman [2] have shown that such models can be produced that are strictly hyperarithmetic in $O$ . As such, $O$ can determine which $X \in X_{p_{n}}$ are not in $M_{i}$ , and so can produce a modified condition $p_{n}^{'}$ which has forgotten each real not appearing in the model. Furthermore, $O$ can enumerate each element of the model that is a dense subset of (the model’s version of) Kumabe-Slaman forcing. Then $O$ can search for an extension of $p_{n}^{'}$ in $M_{i}$ meeting a dense set appearing in the model. By Lemma 5.4 of Barnes [1], there is such an extension that adds no new computations to any of the forgotten reals, and so such an extension q can be chosen and master sequence can be extended by defining $p_{n + 1} = (Φ_{q}, X_{q} \cup X_{p})$ , which does not interfere with the coding procedure.

Hence, for each i, the master sequence induces a sequence $p_{n}^{'} = (Φ_{p_{n}}, X_{p_{n}} \cap {(2^{ω})}^{M_{i}})$ such that each $p_{n}^{'} \in M_{i}$ and the sequence ${p_{n}^{'}}$ is $M_{i}$ -generic for $M_{i}$ ’s Kumabe-Slaman forcing. Thus, on general grounds, the generic object $G^{'}$ corresponding to ${p_{n}}$ preserves $ω_{1}^{CK}$ and, indeed, as $C_{i} \in M_{i}$ it even follows that $C_{i} \oplus G^{'}$ preserves $ω_{1}^{CK}$ . Note, though, that the generic object $G^{'}$ is the same object as $G$ , the generic for the master sequence, and so, $C_{i} \oplus G$ preserves $ω_{1}^{CK}$ as required.

Finally, ideals below $E_{j}$ must be avoided. Barnes [1] does not do this via genericity, instead he uses a counting argument. However, it is not hard to see that $O$ can determine which sets are hyperarithmetic in $E_{j}$ , and so attempt to diagonalize against our generic equaling these sets. This is certainly not difficult to do, but the coding procedure must be maintained.

Fix a condition $(Φ_{p}, X_{p})$ and a set $Y ⩽_{H} E_{j}$ . It is shown that $Φ_{g} \neq Y$ may be forced. WLOG assume that Y is a use monotone Turing functional that is correct for B on input A (see Barnes [1] for definitions), as $Φ_{g}$ will be such an object. Suppose that every candidate n to put into $Φ_{p}$ (i.e. $n \notin Y$ but is allowed to enter $Φ_{p}$ ) would interfere with our coding procedure, i.e., is of the form $(x, y, α)$ with $α \subset A$ . As $X_{p}$ does not contain A (by induction) there is some sufficiently long initial segment of A not an initial segment of any $X \in X_{p}$ (and sufficiently long so as to not mess with use monotonicity, or that $Φ_{p}$ is a Turing functional, and so on). Let x be the least number such that there is no axiom about x applying to A in $Φ_{p}$ (i.e., is the next value we need to code). As Y is a use monotone Turing functional correct for B on input A there is only one axiom $(x, y, α) \in Y$ with $α \subset A$ , so all we need to do is put in $(x, y, α^{'})$ where $α^{'} \subset A$ is sufficiently long to be allowed, and is not precisely α. This information can all be determined uniformly in $O$ and so $O$ can diagonalize by meeting appropriate dense sets.

Consequently, a generic of the correct kind can be produced hyperarithmetically in $O$ as required.

The last thing is to show that Theorem 4.5 implies the full simple almost-end-extension case. But this is almost precisely Jockusch and Slaman’s Theorem 3.1 [3] with very minor changes to allow for the production of USL^⊤ embeddings instead of USL embeddings (also, note that their proof makes use of allowing infinitely many $(c_{i}, d_{i})$ and $e_{j}$ but when the USLs are finite, only arbitrary long finite lists are required). The completes the project of the this document.

References

J.S.

Barnes, On the decidability of the

Σ_{2}

-theories of the arithmetic and hyperarithmetic degrees as uppersemilattices, The Journal of Symbolic Logic, Forthcoming.

L.A.

Harrington,

R.A.

Shore and

T.A.

Slaman,

Σ_{1}^{1}

in every real in a

Σ_{1}^{1}

class of reals is

Σ_{1}^{1}

, Computability and Complexity, A. Day, M. Fellows, N. Greenberg, B. Khoussainov and A. Melnikov, eds, Springer-Verlag, to appear.

C.G.

Jockusch and

T.A.

Slaman, On the Σ₂-theory of the upper semilattice of Turing degrees, in: The Journal of Symbolic Logic, Vol. 58, Association for Symbolic Logic, 1993.

Kjos-Hanssen and

R.A.

Shore, Lattice initial segments of the hyperdegrees, in: Journal of Symbolic Logic, Vol. 75, Association for Symbolic Logic, 2010.

Lerman, Degrees of unsolvability, in: Perspectives in Mathematical Logic, Omega Series, Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1983.

Lerman and

R.A.

Shore, Decidability and invariant classes for degree structures, in: Transactions of the American Mathematical Society, Vol. 310, AMS, 1988.

G.E.

Sacks, Higher Recursion Theory, Springer-Verlag, 1990.

Spector, On degrees of recursive unsolvability, Annals of Mathematics 64(3) (1956), 581–592. doi:10.2307/1969604.