An ω -REA set forming a minimal pair with 0 ~ ′

Abstract

It is easy to see that no n-REA set can form a (non-trivial) minimal pair with ${\underset{~}{0}}^{'}$ and only slightly more difficult to observe that no ω-REA set can form a (non-trivial) minimal pair with ${\underset{~}{0}}^{″}$ . Shore has asked whether this can be improved to show that no ω-REA set forms a (non-trivial) minimal pair with ${\underset{~}{0}}^{'}$ . We show that no such improvement is possible by constructing an ω-REA set C with $\underset{~}{0} <_{T} C ⩽_{T} {\underset{~}{0}}^{″}$ forming a minimal pair with ${\underset{~}{0}}^{'}$ . We then show that no α-REA set (for any notation α) can form a (non-trivial) minimal pair with ${\underset{~}{0}}^{″}$ .

Keywords

REA Turing reducible computability minimal pair

1. Introduction

1.1. Notation

The notation we use in this proof is largely standard. We use $σ, τ, δ, ϵ$ to denote finite partial functions from ω to ${0, 1}$ and write $σ ≺ τ$ to denote that the function τ extends σ. We identify sets with their characteristic functions so that $σ ≺ X$ has the expected meaning for $X \subset ω$ and use capital roman letters to range over subsets of ω or partial functions (from ω to ${0, 1}$ ) understood as pieces of such sets.

We say σ is incompatible (compatible) with τ, denoted $σ ∣ τ$ ( $σ ∤ τ$ ), if there is some (no) $x \in dom σ \cap τ$ with $σ (x) \neq τ (x)$ . We regard functions as sets of ordered pairs so if $σ ∤ τ$ then $σ \cup τ$ gives us the least common extension and ∅ denotes the empty partial function. We let $α, β, γ$ range over elements in $ω^{< ω}$ , write $α^{-}$ for the parent of α and let $α^{+}$ range over children of α. We denote the length of a α by $| α |_{}$ and the concatenation of α with β by $α^{⌢} β$ . In the special case β is the function of length 1 sending 0 to x we abbreviate $α^{⌢} β$ by $α^{⌢} ⟨ x ⟩$ .

$Φ_{e} (Z; x)$ denotes the e-th ${0, 1}$ valued partial computable functional applied to oracle Z on the input x. We adopt the convention that if $Φ_{e} (Z; x)$ converges in s steps, written $Φ_{e} (Z; x) ↓_{s}$ , then $Φ_{e} (Z ↾_{s}; x) = Φ_{e} (Z; x)$ . $W_{e}^{Z}$ is the e-th set c.e. in Z and $W_{e, s}^{Z}$ is its stage s approximation. We use $⟨ x, y ⟩$ to denote the integer code of the pair $(x, y)$ and assume, $\overline{C}$ for the complement of C, $C^{'}$ for the jump of C and $⩽_{T}, \equiv_{T}, \land_{T}, \lor_{T}$ for Turing reducibility, equivalence, meet and join respectively. We adopt the usual abuse of notation allowing us to write $C ⩽_{T} \underset{~}{d}$ with the obvious meaning. We follow the standard practice of identifying $X^{[n]}$ , the n-th column of X, with ${y | ⟨ n, y ⟩ \in X}$ and $X^{[⩽ n]}$ for ${⟨ m, y ⟩ \in X | m ⩽ n}$ . We extend this notation to partial $0, 1$ valued functions on ω in the obvious manner and stipulate that $X^{[< 0]} = \emptyset$ .

1.2. Overview

In [1] Jockusch and Shore introduce the α-REA sets (for $α < ω_{1}^{CK}$ ) as the sets produced by effectively iterating the construction of a relatively c.e. set α many times. Since we will restrict our attention here to $α = ω$ we will use an equivalent (up to Turing degree) definition.

Definition 1.1.
$C \subseteq ω$ is ω-REA iff there is a computable function f such that $C^{[n]} = W_{f (n)}^{C^{[< n]}}$ .

Professor Shore has observed that if $C ≰_{T} \underset{~}{0}$ is ω-REA then $\exists B ⩽_{T} C$ with $\underset{~}{0} <_{T} B <_{T} {\underset{~}{0}}^{″}$ but asked (private communication) if this would still hold if ${\underset{~}{0}}^{″}$ was replaced with ${\underset{~}{0}}^{'}$ . In this paper we answer this question in the negative by proving the following theorem. Theorem 1.2.
There is an ω-REA set $C ≢_{T} \underset{~}{0}$ such that ${\underset{~}{0}}^{'} \land_{T} \underset{~}{C} \equiv_{T} \underset{~}{0}$ .

1.3. Failure at ${\underset{~}{0}}^{″}$

Before we embark on this construction it is instructive to see why this claim fails for ${\underset{~}{0}}^{″}$ .

Proposition 1.3.
If C is ω-REA and $C ≢_{T} \underset{~}{0}$ then $C \land_{T} {\underset{~}{0}}^{″} ≢_{T} \underset{~}{0}$ .
Proof.
Assume C fails the lemma. We first argue that for every n, $C^{[⩽ n]}$ must be computable. Since $C^{[n + 1]}$ is $Δ_{2}^{0}$ in $C^{[⩽ n]}$ if n is maximal integer with $C^{[⩽ n]} ⩽_{T} \underset{~}{0}$ we must have $\underset{~}{0} <_{T} C^{[n + 1]} ⩽_{T} {\underset{~}{0}}^{'} ⩽_{T} {\underset{~}{0}}^{″}$ . Hence if $C \land_{T} {\underset{~}{0}}^{″} \equiv_{T} \underset{~}{0}$ then $C^{[⩽ n]} ⩽_{T} \underset{~}{0}$ for all $n \in ω$ .

So suppose $C^{[⩽ n]} ⩽_{T} \underset{~}{0}$ for all $n \in ω$ . We now argue that ${\underset{~}{0}}^{″}$ can compute C. Note that given a c.e. index for a computable set R, ${\underset{~}{0}}^{″}$ can recover a c.e. index for $\overline{R}$ and from c.e. indexes for $C^{[⩽ n]}$ and $\overline{C^{[⩽ n]}}$ a c.e. index for $C^{[⩽ n + 1]}$ is uniformly computable. Thus, if $C^{[⩽ n]}$ is computable for all $n \in ω$ , by induction, ${\underset{~}{0}}^{″}$ can recover $i_{n}, j_{n}$ with $C^{[⩽ n]} \equiv_{T} W_{i_{n}} \equiv_{T} \overline{W_{j_{n}}}$ . Clearly these indexes allow ${\underset{~}{0}}^{″}$ to compute C. □

The lesson to be drawn from this proof is that any C satisfying Theorem 1.2 must be the join of a countable collection of computable sets. Thus the non-computability of C must result from the non-uniformity of this join. The difficulty in building C is therefore how to encode enough about ${\underset{~}{0}}^{'}$ in $C^{[< n]}$ so $C^{[n]}$ can successfully diagonalize against the $Δ_{2}^{0}$ sets while making sure $C^{[< n]}$ only encodes a finite amount of non-computable information.
2. Machinery

2.1. Building ω-REA sets

Evidently if we are to build $C \notin Δ_{2}^{0}$ we will need to uniformly specify a c.e. procedure for building $C^{[n]}$ from $C^{[< n]}$ while dealing with the fact that our approximation to $C^{[< n]}$ will never settle on the correct value. Rather than trying to explicitly give such a procedure upfront we will instead enumerate rules, called axioms, committing us to enumerate certain elements into $C^{[n]}$ when certain conditions are met by $C^{[< n]}$ .

Definition 2.1.
A axiom is a triple $⟨ l : σ \to y ⟩$ where $l \in ω$ , σ is a function from a finite subset of $ω^{[< l]}$ to ${0, 1}$ and $y \in ω^{[⩾ l]}$ .

We think of the axiom $⟨ l : σ \to y ⟩$ as a commitment to place y in C if $σ ≺ C$ . The parameter l serves only to ensure that attempts to enumerate elements in the n-th column of C are only allowed to consult the first $n - 1$ columns of C, thus avoiding any circularity. The utility of this definition is made clear by the following lemma.
Lemma 2.2.
If $A$ is a c.e. set of axioms then the set C defined by $\begin{matrix} (2.1) & y \in C ⟺ (\exists l \in ω) (\exists σ ≺ C) [⟨ l : σ \to y ⟩ \in A] \end{matrix}$ then $A$ is ω-REA.
Proof.
Note that $\begin{matrix} ⟨ n, x ⟩ \in C ⟺ (\exists l ⩽ n) (\exists σ ≺ C^{[< l]}) [⟨ l : σ \to ⟨ n, x ⟩ ⟩ \in A] \end{matrix}$ Thus $C^{[n]}$ only depends on $C^{[< n]}$ so C is well defined. Furthermore, the above equation explicitly defines $C^{[n]}$ from $C^{[< n]}$ and n via a (uniformly) $Σ_{1}^{0}$ formula. Thus, by an application of the s-m-n theorem [2] there is a computable function f satisfying Definition 1.1. □

Our construction will proceed by building a c.e. set $A$ of axioms which will yield an ω-REA set via the preceding lemma. To make proper use of this machinery we introduce two more definitions. We first try and capture the notion that some axiom $⟨ l : σ^{'} \to y ⟩$ only has an effect if $σ ≺ C$ .
Definition 2.3.
The axiom $⟨ l : σ^{'} \to y ⟩$ depends on σ if $σ ≺ σ^{'}$ . We say the axiom $⟨ l : σ \to y ⟩$ is enumerated dependent on δ to mean we enumerate $⟨ l : σ \cup δ^{[< l]} \to y ⟩$ into $A$ .

We will also speak loosely of an element $x \in ω^{[l]}$ being enumerated as shorthand for the axiom $⟨ l : \emptyset \to x ⟩$ being enumerated. We will also say that an axiom is enumerated dependent on $C (n) = 0$ (or just n) when the axiom is enumerated dependent on the partial function σ defined by $σ (n) = 0$ . Finally, we say an axiom $⟨ l : σ \to y ⟩$ is compatible (incompatible) with a partial function τ just if σ is compatible (incompatible) with τ.

During our construction, we will frequently want to satisfy some requirement on the assumption that C behaves a particular way on some domain. In particular, our construction will make guesses about the behavior of C on some finite number of columns supplemented by a finite number of additional locations. We, therefore, introduce a notion of how the axioms would affect C if such a guess were correct.
Definition 2.4.
Given any partial function τ we say that a set of axioms $A$ yields $C \subset ω$ over τ just if $\begin{matrix} x \in C ⟺ τ (x) = 1 \lor (\exists σ ≺ C) (\exists l \in ω) [x \notin dom τ \land ⟨ l : σ \to x ⟩ \in A] \end{matrix}$ Given compatible partial functions $C_{α}$ and δ we say that $A$ yields C over $C_{α}, δ$ when $A$ yields C over $C_{α} \cup δ$ .

In other words $A$ yields C over $C_{α}, δ$ just if we assume that C really does extend both $C_{α}$ and δ (ignoring any axioms to the contrary) and apply the construction from Lemma 2.2 starting from $C_{α} \cup δ$ . The fact that axioms1
¹
In the above equation we presume that all elements in $A$ are valid axioms.

are only allowed to reference prior columns ensures not only that C is well defined but also that, if $A$ is finite, then C can be uniformly computed from $C_{α}, δ$ and $A$ . Sometimes we will informally talk of $A$ yielding σ over $C_{α}, δ$ when it yields $C ≻ σ$ .
3. Requirements & modules

We fix a computable array $V_{e, s}$ of sets via the limit lemma [5] such that every $Δ_{2}^{0}$ set is of the form $V_{e} = {lim}_{s \to \infty} V_{e, s}$ and build C to meet the following requirements. $\begin{array}{l} R_{e, i} : Φ_{i} (C) \neq V_{e} or V_{e} ⩽_{T} \underset{~}{0} whenever V_{e} is defined \\ N_{e} : W_{e} \neq \overline{C} \end{array}$ We reserve columns $3 ⟨ e, i ⟩$ , $3 ⟨ e, i ⟩ + 1$ for $R_{e, i}$ and the column $3 e + 2$ for meeting $N_{e}$ and grant each requirement the right to modify a finite initial segment of later columns but not earlier columns. Each column of C will be either finite or co-finite thereby making $C^{[< n]}$ computable as our observation above required.

As C can’t be computable in ${\underset{~}{0}}^{'}$ during the construction later requirements won’t know, even in the limit, how the earlier requirements are satisfied. To deal with this we perform our construction along a tree, assigning to each $α \in ω^{< ω}$ in the tree a module $P_{α}$ of the form $R_{α}$ or $N_{α}$ tasked with handling a particular requirement on the assumption that α correctly encodes how the higher priority requirements are met. In particular we assign requirements to modules as follows. $\begin{matrix} (3.1) & P_{α} = \{\begin{matrix} R_{α} handling R_{e, i} & if | α |_{} = 2 ⟨ e, i ⟩ \\ N_{α} handling N_{e} & if | α |_{} = 2 e + 1 \end{matrix} \end{matrix}$

Given $α \in ω^{< ω}$ we define $l_{α}$ to be the first column reserved for the requirement handled by the module at α. Note that $l_{α}$ only depends on $| α |_{}$ , so all modules tasked with meeting a given requirement share columns and as $l_{β} ⩽ l_{α}$ iff $| β |_{} ⩽ | α |_{}$ the descendants of β can’t affect $C^{[< l_{β}]}$ . In other words, if α implements $R_{α}$ ( $N_{α}$ ) then all nodes of length $| α |_{}$ share the columns $l_{α}, l_{α} + 1$ (column $l_{α}$ ) and all nodes of length $| α^{+} |_{}$ share the column $l_{α^{+}} = l_{α} + 2$ (columns $l_{α^{+}} = l_{α} + 1, l_{α^{+}} + 1$ ). Note that, while every node only directly acts to modify C on the columns reserved for it, the module $R_{α}$ can indirectly affect locations in latter columns by enumerating elements which affect the application of axioms enumerated by nodes of longer length.

3.1. Action along the tree

As explained above the module at α will act to meet its requirement using the information encoded in α about how earlier requirements were met. At each stage we will have some guess at how the various requirements are met, and that guess will control which modules are executed at that stage, i.e., only those modules that appear to have correct guesses execute. The resulting construction takes the form of a standard $Π_{2}^{0}$ priority tree argument as described in [6].

We remind the reader that a priority tree seeks to define a function f, the truepath, such that if $α^{-} ≺ f$ then $f (| α |_{})$ indicates how the module at α satisfies its associated requirement. At each stage s, we build an approximation $f_{s} \in ω^{< ω}$ to the truepath by inductively defining $f_{s} (n)$ to be the outcome selected by the module located at $f_{s} ↾_{n}$ at stage s, provided this isn’t the first time that $f_{s} ↾_{n}$ is visited. Note that our choice of $f_{s}$ differs from the notation $δ_{s}$ used in [6], as does our decision to limit the length of $f_{s}$ so that only a single previously unvisited node is visited each stage.

4. The construction

A full description of the construction will consist of giving the behavior of each module $P_{α}$ , the approximation to its outcome $f_{s} (α)$ and (computably) associating to each node α a (index for a) computable partial function $C_{α}$ with domain $ω^{[< l_{α}]}$ and a finite partial function $δ_{α}$ . The partial computable function $C_{α}$ represents a guess at the first $l_{α}$ columns of C, and $δ_{α}$ represents a guess at the behavior of C as a result of axioms enumerated (by incompatible nodes) before α is visited (as impacted2

²
For instance, if α implements a module of the form $R_{α}$ then both $δ_{α^{⌢} ⟨ 1 ⟩}$ and $δ_{α^{⌢} ⟨ 3 ⟩}$ build on $δ_{α}$ by capturing the effect of axioms previously enumerated by nodes extending $α^{⌢} ⟨ 0 ⟩$ but the differing predictions these nodes make on column $l_{α} + 1$ affect which of these axioms succeeds in their enumeration.

by the action of nodes

β ≺ α

). Note that we will ensure that

C_{α}

and

δ_{α}

are always compatible and that whenever

α ≻ β

then

δ_{α} ≻ δ_{β}

and

C_{α} ≻ C_{β}

The partial function $δ_{β}$ will also play a secondary role as a restraint on nodes $α ⪰ β$ , as no node α is allowed to enumerate axioms attempting to place $y \in dom δ_{α}$ into C. By ensuring that $dom δ_{α^{+}}$ includes the use of any computations being preserved by $R_{α}$ , we will avoid any injury by descendant nodes. Note that, while both $C_{α}$ and $δ_{α}$ are functions only of α and don’t depend on the stage, they aren’t defined until the first stage at which α is visited. This allows both $C_{α}$ and $δ_{α}$ to accommodate actions taken before α is visited, which will be critical to accommodate the other modules sharing the same columns.

4.1. Basic approach

The global construction is a standard priority tree construction in which we try to ensure that if $α ∣ β$ then the modules at α and β don’t interfere. Ideally, this would be accomplished simply by ensuring that whenever $α ∣ β$ then $δ_{α} ∣ δ_{β}$ . By always enumerating any axiom produced by the module at α dependent on $δ_{α}$ , this would allow us to ensure only axioms enumerated along the true path have any effect on C.3

³
At least on the assumption, which we will later vindicate, that $δ_{α} ≺ C$ .

However, we can’t accomplish this without disrupting computations we need to preserve.4

⁴

In particular, $R_{α}$ couldn’t commit to placing z in C only if it observes incompatible approximations to $Φ_{i} (C)$ since enumerating z could destroy the incompatible approximations.

So, instead we will ensure a weaker condition which will ensure that, after α is first visited, it can ignore axioms subsequently enumerated by incompatible nodes β and that those axioms it can’t ignore have their effect safely confined to

δ_{α}

. Specifically, we will satisfy the following condition.

Condition 1.

The following hold for any node α.

Suppose $α ≺ f_{s_{0}}, f_{s_{2}}$ , $β ∣ α$ and $β ≺ f_{s_{1}}$ with $s_{0} < s_{1} < s_{2}$ then $δ_{β} ∣ δ_{α}$ .

If $β ∣ α$ but $δ_{β} ∤ δ_{α}$ then any y mentioned in an axiom enumerated by β before α is visited satisfies $y \in dom δ_{α}$ .

Before giving a precise account of each module’s behavior we informally sketch our strategy for meeting each requirement in isolation. The module $N_{α}$ works to meet $N_{e}$ as follows.

Initially, $N_{α}$ picks some $y \notin C$ outside of $δ_{α}$ but in the column designated for α’s use. This allows $N_{α}$ to hold y out of C to ensure $C \cup W_{e} \neq ω$ , as long as y doesn’t enter $W_{e}$ . If y does enter $W_{e}$ the module enumerates y into C to ensure $C \cap W_{e} \neq \emptyset$ . This guarantees $N_{e}$ is satisfied while imposing what a simpler construction would call finite injury, but in a priority tree construction corresponds to the approximation to the truepath shifting left to visit virgin copies of any lower priority modules.

The module $R_{α}$ working to satisfy $R_{e, i}$ provides a more interesting case. Here our strategy will be to lay dormant (unactivated) as long as the action of nodes $α^{'} ≻ α$ never leads us to change our mind about (our approximation to) $Φ_{i} (C)$ , i.e., flip the value of $Φ_{i} (C; x)$ for some x. If our minds are never changed, we will argue that $Φ_{i} (C)$ is computable. If we do see a change in our approximation, say at $Φ_{i} (C; x)$ , we will activate $R_{α}$ and steer C towards whichever possibility ensures that $Φ_{i} (C; x) \neq V_{e, s} (x)$ . Should the value of $V_{e, s} (x)$ change at a latter stage, we steer C towards the other approximation. Assuming we can change our minds as many times as we wish, we either succeed in diagonalizing against $V_{e}$ or $V_{e, s} (x)$ changes its mind infinitely often and $V_{e}$ isn’t defined. Either way we satisfy $R_{e, i}$ .

This leaves us two challenges. First, ensuring that if α’s approximation to $Φ_{i} (C; x)$ ever takes on a new value we can restore the old value, even if $Φ_{i} (C; x)$ diverges for a long period between realizing the disagreeing computations. Second, we must be able to repeat this process and alternate between these incompatible outcomes as many times as we wish.

We tackle the first challenge by making sure that if $α ≺ f_{s}$ then $R_{α}$ has the means to ‘rollback’ the axioms compatible with $C_{α}, δ_{α}$ to any previous stage t at which α was visited. The idea here is that, by the remarks above, only axioms enumerated by descendants of α can change α’s approximation to C.5

⁵

That is, the approximation to C on the assumption that α is on the truepath at stages where $α ≺ f_{s}$ . This is essentially the set yielded by $A_{s + 1}$ over $C_{α}, δ_{α}$ but we will offer a more precise definition latter and show that, at stages α is visited, the global approximation to C matches this approximation.

We enable this rollback by ensuring all and only the (relevant) axioms enumerated after stage t depend on

C (y) = 0

for some value y in column

l_{α} + 1

. By enumerating y into C we recover the approximation to C (as seen from α) at stage t.

We tackle the second challenge by taking y in and out of C as needed to disagree with $V_{e, s} (x)$ . By only enumerating y into C dependent on $C (⟨ l_{α}, n ⟩) = 0$ for some n, we can later remove y from C by enumerating $⟨ l_{α}, n ⟩$ into C. If $V_{e, s} (x)$ changes back again we can reenumerate y dependent on $C (⟨ l_{α}, n + 1 ⟩) = 0$ and so on. Note that if we flip-flop infinitely often then $C^{[l_{α}]} =^{*} ω$ and otherwise $C^{[l_{α}]} =^{*} \emptyset$ . At this point the broad outlines of the proof should be apparent, but the remainder of the paper is necessary to verify that the technical details can be filled in as I’ve suggested and when they are the construction behaves as expected.

Before moving on to the details there is one last big picture concern that must be addressed: ensuring that part 1 of Condition 1 can be satisfied with respect to the infinitary outcome $α^{+}$ of α. That is, ensuring that axioms enumerated by finitary outcomes don’t affect C if it extends $δ_{α^{+}}$ .6

⁶

The infinitary outcome predicts the same content for column $l_{α} + 1$ as the finitary outcomes leaving y out of C and column $l_{α}$ can’t keep $δ_{α^{+}}$ incompatible with finitary outcomes that have flip-flopped sufficiently many times.

Of course, if all the finitary outcomes guessed y wasn’t in C there would be an easy solution. So we simply replicate that situation by adding a flag q into column

l_{α} + 1

which, unlike y, is always enumerated into C at finitary outcomes while also being canceled each time we visit the infinitary outcome. Essentially, q acts as a flag indicating whether α has an infinitary (

C (q) = 0

) or finitary (

C (q) = 1

) outcome, and we can simply insert q into the domain of

dom δ_{α^{+^{'}}}

for the appropriate children

α^{+^{'}}

of α.

4.2. Global actions

To ensure the modules interact appropriately we specify two global rules which modify the axioms enumerated by the modules on the tree before they are enumerated into $A$ .

If $P_{α}$ enumerates axiom π then π is enumerated dependent on $δ_{α}$ .

If $P_{α}$ wants to enumerate axiom π at stage s and $β ≺ α$ implements an unactivated $R_{β}$ module then $R_{β}$ intercepts the enumeration of π, chooses $m_{s}^{β}$ large and enumerates π dependent on the partial function sending $⟨ l_{β} + 1, m_{l}^{β} ⟩$ to 0 for each $l ⩽ s$ for which $m_{l}^{β}$ is defined. The resulting axiom $π^{'}$ is then passed down the tree for the next longest such β to modify or to be enumerated into $A$ if there is no such β.

The purpose served by these rules has already been discussed above. However, it is still worth noting that enumerating $m_{s}^{β}$ will cancel the effect of every axiom enumerated at or after stage s by any node $α ≻ β$ and thus serve as the value y mentioned above. We now give the detailed actions of the various modules with the understanding that any axioms they enumerated will be modified in the obvious way to obey the above rules before being enumerated into $A$ .

4.3. The basic $R_{β}$ strategy

Suppose $R_{β}$ is assigned to β to handle $R_{e, i}$ and β is visited at stage s. If $R_{β}$ hasn’t yet been activated 7

⁷
Note that we will later observe no node is ever revisited after initialization so we need not consider such cases.

we search for an integer y such that if y is enumerated into

C^{[l_{β} + 1]}

it alters (incompatibly) the result of

Φ_{i} (C)

. If we don’t find such a y no action is taken and we describe the actions taken if it is found below. More formally we search for

x, y \in ω, Y_{0}, Y_{1} \in 2^{< ω}

such that

\begin{array}{l} (4.1) & \begin{aligned} x, y, | Y_{0} |_{}, | Y_{1} |_{} < s \\ Φ_{i} (Y_{0}; x) ↓_{y} \neq Φ_{i} (Y_{1}; x) ↓_{s} \\ | Y_{0} |_{} < y \\ y \in ω^{[l_{β} + 1]} \\ A_{s} yields some C_{1} ≻ Y_{1} over C_{β}, δ_{β} \\ A_{s} \cup {⟨ l_{β} + 1 : \emptyset \to y ⟩} yields some C_{0} ≻ Y_{0} over C_{β}, δ_{β} \end{aligned} \end{array}

When this occurs we say that $R_{β}$ is activated at stage s and select $q \in ω^{[l_{β} + 1]}$ large to serve as our ‘flag’ by satisfying $q \in C$ iff $R_{β}$ only cancels the enumeration of y finitely many times. Also pick8

⁸

In particular, we need $⟨ l_{β}, k_{s}^{β} ⟩ > q + 2$ so we may later select l with $q < l < ⟨ l_{β}, k_{s}^{β} ⟩$ .

k_{s}^{β}

large with the intent of enumerating

k_{s}^{β}

into column

l_{β}

of C whenever we need to cancel an earlier decision to place y in C. If we enumerate

⟨ l_{β}, k_{s}^{β} ⟩

into C at stage s we let

k_{s + 1}^{β} = k_{s}^{β} + 1

. Otherwise

k_{s + 1}^{β} = k_{s}^{β}

, even if β isn’t executed at stage s. Note that we don’t increment the value of

k_{s + 1}^{β}

until

k_{s}^{β}

is placed into

C^{[l_{β}]}

, so

k_{s}^{β}

functions as a kind of marker indicating the next element (if any) we will place in

C^{[l_{β}]}

. Finally, let

j_{s} = 1

to indicate that if no further action is taken C will extend

Y_{1}

. This completes the action of

R_{β}

at this stage.

Now suppose $R_{β}$ was activated at some prior stage, i.e., before s. Let $s_{0} < s$ be the last stage at which β was visited and let $j_{s} \in {0, 1}$ be such that $Φ i (Y_{j_{s}}; x) \neq V_{e, s} (x)$ . Say that stage s is eventful for $R_{β}$ just if $j_{s} \neq j_{s_{0}}$ (note that we regard the stage at which $R_{β}$ is activated as uneventful). In other words eventful stages are ones where we’ve changed our mind about what we want the value of $Φ_{i} (C; x)$ to be.

If s is an eventful stage then we consider the following two cases. If $j_{s} = 1$ we wish to make $C ≻ Y_{1}$ so we must cancel some prior enumeration of y into C that was made dependent on $C (⟨ l_{β}, k_{s}^{β} ⟩) = 0$ . We thus enumerate $⟨ l_{β}, k_{s}^{β} ⟩$ into C and (per the rule above) set $k_{s + 1}^{β} = k_{s}^{β} + 1$ . If $j_{s} = 0$ then we wish to make $C ≻ Y_{0}$ so we enumerate y into C dependent on $C (⟨ l_{β}, k_{s}^{β} ⟩) = 0$ .

If s is not an eventful stage we don’t need to take any action to add or remove y from C. However, we need to ensure that our ‘flag’ q indicates that we took a finite outcome. To this end, enumerate9

⁹

We could have produced the same effect by enumerating q only at the first non-eventful stage following an eventful stage.

q into C dependent on

C (⟨ l_{β}, k_{s}^{β} ⟩) = 0

, i.e., place q into C provided

k_{s}^{β}

doesn’t enter

C^{[l_{β}]}

. Note that at the next eventful stage t at which

j_{t} = 1

we cancel this enumeration of q by placing

k_{s}^{β}

into

C^{[l_{β}]}

Letting n be the number of eventful stages at or before stage s, we define the possible outcomes of β at stage s (i.e., the value of $f_{s} (| β |_{})$ ) $\begin{matrix} f_{s} (| β |_{}) = \{\begin{matrix} 0 & if P_{β} hasn’t yet been activated \\ 1 & if s is an eventful stage and j_{s} = 1 \\ (Outcome guessing {lim}_{s \to \infty} V_{e, s} (x) ↑, q \notin C, y \notin C) \\ n + 2 & if s is uneventful and j_{s} = 1 (Outcome guessing finitary diagnolization, q \in C, y \notin C) \\ n + 2 & if j_{s} = 0 (Outcome guessing finitary diagnolization, q \in C, y \in C) \end{matrix} \end{matrix}$

Note that outcomes of the form $n + 2$ correspond to the guess that $y \notin C$ ( $j_{s} = 1$ ) if $n \equiv 0 mod 2$ and $y \in C$ ( $j_{s} = 0$ ) if $n \equiv 1 mod 2$ .

If $R_{β}$ is activated at stage t and $C_{1}, C_{0}, x, y$ are as in Eq. (4.1) at stage t then let $δ_{0}, δ_{1}$ be $C_{0} ↾_{l}$ and $C_{1} ↾_{l}$ respectively where l is chosen large at the start of execution of $R_{β}$ at stage t so that $| Y_{0} |_{}, | Y_{1} |_{}, y < l < q < k_{t}^{β}$ . Since l is large, $δ_{0}, δ_{1}$ capture the effect of any axioms in $A_{t}$ over $C_{β}, δ_{β} \cup (y, 1)$ and $C_{β}, δ_{β}$ respectively. We now define $δ_{β^{⌢} ⟨ w ⟩}$ to extend $δ_{0}$ or $δ_{1}$ depending on whether this outcome (if true, i.e., $β^{⌢} ⟨ w ⟩ ≺ f$ ) places $y \in C$ . Note the infinitary outcome $w = 1$ doesn’t place y (or q) into C since every axiom enumerating y (or q) is eventually canceled. This definition will also ensure $δ_{β^{⌢} ⟨ w ⟩}$ reflects the disposition of q and, for the finitary outcomes, enough elements in column $l_{β}$ to reflect how many times we’ve canceled a previous enumeration of y. Specifically, keeping in mind the remark above about the features of the outcome $n + 2$ based on the value of $n mod 2$ we define $\begin{matrix} (4.2) & δ_{β^{⌢} ⟨ w ⟩} (x) = \{\begin{matrix} δ_{β} (x) & if x \in dom δ_{β} \\ δ_{1} (x) & if x \in dom δ_{1} \land (w = 1 \lor (w > 1 \land w \equiv 0 mod 2)) \\ δ_{0} (x) & if x \in dom δ_{0} \land w > 1 \land w \equiv 1 mod 2 \\ 0 & if w = 1 \land x = q \\ 1 & if w > 1 \land x = q \\ 1 & if w > 1 \land x = ⟨ l_{β}, m ⟩ \land k_{t}^{β} ⩽ m < k_{t}^{β} + ⌊ \frac{w - 2}{2} ⌋ \\ 0 & if w > 1 \land x = ⟨ l_{β}, k_{t}^{β} + ⌊ \frac{w - 2}{2} ⌋ ⟩ \\ ↑ & otherwise \end{matrix} \end{matrix}$

Note that if $w, w^{'} \neq 0$ then $δ_{β^{⌢} ⟨ w ⟩} ∣ δ_{β^{⌢} ⟨ w^{'} ⟩}$ . The outcome $w = 1$ is differentiated by $δ_{β^{⌢} ⟨ w ⟩} (q) = 0$ . The partial functions $δ_{β^{⌢} ⟨ w ⟩}, δ_{β^{⌢} ⟨ w^{'} ⟩}$ with $w = 2 n + j + 2, w^{'} = 2 n^{'} + j^{'} + 2$ and $j, j^{'} \in {0, 1}$ disagree on $k_{t}^{β} + ⌊ \frac{n}{2} ⌋$ if $n < n^{'}$ , $k_{t}^{β} + ⌊ \frac{n^{'}}{2} ⌋$ if $n^{'} < n$ and y if $j \neq j^{'}$ . Also note that $δ_{0}, δ_{1}$ incorporate the effects of any axioms enumerated before any $δ_{β^{⌢} ⟨ w ⟩}, w \neq 0$ is visited.

We are now in a position to define $C_{β^{⌢} ⟨ w ⟩}$ to be the partial function extending $C_{β}$ with domain $ω^{[⩽ l_{β + 1}]}$ by specifying its behavior on $l_{β}, l_{β + 1}$ . As the only behavior not already captured in our definition of $δ_{β^{⌢} ⟨ w ⟩}$ , is the effect of the infinitary outcome on column $l_{β}$ it is enough to define (where t is still the stage at which β was activated) $\begin{matrix} (4.3) & \begin{matrix} C_{β^{⌢} ⟨ w ⟩} (⟨ l_{β}, x ⟩) & = \{\begin{matrix} δ_{β^{⌢} ⟨ w ⟩} (⟨ l_{β}, x ⟩) & if ⟨ l_{β}, x ⟩ \in dom δ_{β^{⌢} ⟨ w ⟩} \\ 1 & if w = 1 \land k_{t}^{β} ⩽ x \\ 0 & otherwise \end{matrix} \\ C_{β^{⌢} ⟨ w ⟩} (⟨ l_{β + 1}, x ⟩) & = \{\begin{matrix} δ_{β^{⌢} ⟨ w ⟩} (⟨ l_{β} + 1, x ⟩) & if ⟨ l_{β} + 1, x ⟩ \in dom δ_{β^{⌢} ⟨ w ⟩} \\ 0 & otherwise \end{matrix} \end{matrix} \end{matrix}$

4.4. The basic

N_{β}

strategy

Suppose $N_{β}$ is assigned to β handling $N_{e}$ . $N_{β}$ ensures that $\overline{C} \neq W_{e}$ by ensuring that, for some y, either $y \notin C \cup W_{e}$ or $y \in C \cap W_{e}$ . We now describe the action of the module $R_{β}$ which ensures this.

Suppose that β is visited at stage s. If this is the first time that β is visited then choose $y \in ω^{[l_{β}]}$ large (and in particular not in $dom δ_{β}$ ). Whether or not this is the first time β is visited, if $N_{β}$ hasn’t previously acted check if $y \in W_{e, s}$ . If so enumerate y into C, i.e., enumerate the axiom $⟨ l : \emptyset \to y ⟩$ . We say $N_{β}$ acts at such a stage and once $N_{β}$ has acted it never acts again.

We define the outcomes of the module as follows. $\begin{matrix} (4.4) & f_{s} (| β |_{}) = \{\begin{matrix} 0 & if N_{β} hasn’t acted at or before stage s \\ 1 & if N_{β} acted at or before stage s \end{matrix} \end{matrix}$

For $w = 0$ we define $δ_{β^{⌢} ⟨ 0 ⟩} = δ_{β}$ . For $w = 1$ let t be the stage at which $N_{β}$ acts and let l be chosen large at stage t (in particular $l > y$ ). Let X be the set such that $A_{s} \cup {⟨ l : \emptyset \to y ⟩}$ 10

¹⁰
Since this axiom (modified by global rules) is enumerated into $A$ at stage s it first appears in $A_{s + 1}$ .

yields X over

C_{β}, δ_{β}

and define

δ_{β^{⌢} ⟨ 1 ⟩} = X ↾_{l}

. Note that this ensures

δ_{β^{⌢} ⟨ 1 ⟩}

extends

δ_{β}

and

δ_{β^{⌢} ⟨ 1 ⟩} (y) = 1

Finally, define $C_{β^{⌢} ⟨ w ⟩}$ to be the partial function with domain $ω^{[⩽ l_{β}]}$ extending $C_{β}$ and satisfying $\begin{matrix} (4.5) & C_{β^{⌢} ⟨ w ⟩} (⟨ l_{β}, x ⟩) = 1 ⟺ δ_{β^{⌢} ⟨ w ⟩} (⟨ l_{β}, x ⟩) = 1 \end{matrix}$

5. Verification

We now verify that the construction above produces the desired set C. By Lemma 2.2 we have built an ω-REA set so all that remains is to show that $C ≰_{T} \underset{~}{0}$ and $C ⩾_{T} X \in Δ_{2}^{0} ⟹ X ⩽_{T} \underset{~}{0}$ . We first demonstrate that this is a valid tree construction.

Lemma 5.1.
$f = {lim inf}_{s \to \infty} f_{s}$ is well-defined.
Proof.
Suppose, by way of induction, that $f (m)$ is defined for $m < n$ and $f ↾_{n} = α$ . If $P_{α}$ is of the form $N_{α}$ the either $N_{α}$ never acts and $f (n) = 0$ or at some stage $N_{α}$ acts and $f (n) = 1$ . If $P_{α}$ is of the form $R_{α}$ then either $R_{α}$ is never activated giving $f (n) = 0$ , $R_{α}$ has infinitely many eventful stages giving $f (n) = 1$ or $R_{α}$ has exactly m eventful stages giving $f (n) = m + 2$ . Thus, $f (n)$ is well-defined and by induction f is well-defined. □

We note that no node is ever revisited after being initialized.
Lemma 5.2.
Suppose $α ⪯ f_{s_{0}}$ and for some $s_{1} ⩾ s_{0}$ , $f_{s_{1}}$ passes to the left of α then for no stage $s_{2} ⩾ s_{1}$ do we have $α ⪯ f_{s_{2}}$ .
Proof.
Suppose, for contradiction, $α^{+}$ is a ≺ minimal node for which the lemma fails as witnessed by stages $s_{0}, s_{1}, s_{2}$ . If $f_{t}$ passed to the left of α for some $t \in [s_{0}, s_{2}]$ then the stages $s_{0}, t, s_{2}$ would witness the failure of the lemma at α contradicting the minimality of $α^{+}$ . Thus, α must visit some outcome n with $α^{⌢} ⟨ n ⟩ = α^{+}$ at stages $s_{0}, s_{2}$ and visit some outcome $m < n$ at $s_{1}$ . To derive the contradiction it is now enough to note that only the outcome $n = 1$ of the module $R_{α}$ is ever revisited after another outcome, and if outcome 1 is visited $R_{α}$ never again visits outcome 0. □

We now observe that the construction satisfies the stated condition.
Lemma 5.3.
Condition 1 is satisfied.
Proof.
We first verify part 1 of Condition 1. Suppose α is visited at stages $s_{0}, s_{2}$ and $β ∣ α$ visited at $s_{1}$ with $s_{0} < s_{1} < s_{2}$ . Let γ be the longest common initial segment of $α, β$ and let $γ^{⌢} ⟨ a ⟩, γ^{⌢} ⟨ b ⟩$ be the (incompatible) children of γ with $γ^{⌢} ⟨ b ⟩ ⪯ β$ and $γ^{⌢} ⟨ a ⟩ ⪯ α$ . As neither module visits outcome 0 after visiting any other outcome neither a or b can be equal to 0. As the module $N_{γ}$ would have only two outcomes, γ implements $R_{γ}$ . Thus, by the comments immediately following Eq. (4.2) $δ_{γ^{⌢} ⟨ a ⟩} ∣ δ_{γ^{⌢} ⟨ b ⟩}$ .

To verify part 2 of Condition 1, suppose that $β ∣ α$ , $δ_{β} ∤ δ_{α}$ and β visited before α. Let γ be the longest initial segment common to both $β, α$ . By the considerations above and the fact that all modules initially visit the 0 outcome, it follows that β extends $γ^{⌢} ⟨ 0 ⟩$ . However, both modules choose $δ_{γ^{⌢} ⟨ w ⟩}$ for $w > 0$ to have domain extending $ω ↾_{l}$ where l is chosen large after the last stage at which $γ^{⌢} ⟨ 0 ⟩$ is ever visited. The desired claim now follows from the fact that $δ_{α} ⪰ δ_{γ^{⌢} ⟨ w ⟩}$ . □

We now observe that this is enough to let us ignore axioms that are enumerated later by incompatible nodes.
Lemma 5.4.
If $α ⪯ f_{s}$ then for all $β ∣ α$ if $P_{β}$ enumerates the axiom $⟨ l : σ \to y ⟩$ after stage s then $σ ∣ δ_{α}$ .
Proof.
This follows immediately from Lemma 5.2 and the application of rule (I). □

The strategy employed by the module $R_{α}$ depends on the fact that if $Φ_{i} (C; x) = j$ and $α ≺ f$ then, at some point, the approximation to C as seen by α also sees this computation, i.e., at some stage s with $α ⪯ f_{s}$ the set X yielded by $A_{s}$ over $C_{α}, δ_{α}$ satisfies $Φ_{i} (X; x) ↓_{s} = j$ . To see how this might fail, imagine that at each stage s we both enumerate y into C dependent on $C (x_{s}) = 0$ while simultaneously enumerating $x_{s - 1}$ into C. Ultimately, $C (y) = 0$ but the approximation to C given by looking at the effect of $A_{s}$ would always believe y is in C.

In our construction we were careful to ensure that if $α^{+} ⪯ f_{s}$ , then the axioms enumerated by α at or before stage s ( $A_{s + 1}$ ) are compatible with the guess ( $C_{α^{+}}, δ_{α^{+}}$ ) which α makes about C at that stage. These axioms may not yet enumerate all elements in $C_{α^{+}}$ but they don’t enumerate any element which $C_{α^{+}}$ or $δ_{α^{+}}$ predicts isn’t in C.11
¹¹
Note that in verifying this claim it is important to be able to see that the claim holds for α based only on the actual elements enumerated by $β ≺ α$ so far and not merely that it’s true over $C_{α}, δ_{α}$ .

To convince oneself of the truth of this claim, it might suffice to carefully walk through the operation of the modules. However, to formalize both the claim and its justification we introduce the following definition.
Definition 5.5.
Using $k_{s + 1}^{β}$ to refer to the value defined in Section 4.3 in the description of module $R_{β}$ we define $\begin{array}{l} ϵ (s) & = C_{f_{s}} ↾_{\overline{S}} \cup δ_{f_{s}} where \\ S & = {⟨ l_{β}, x ⟩ | β^{⌢} ⟨ 1 ⟩ ⪯ f_{s} \land β implements R_{β} \land x ⩾ k_{s + 1}^{β}} \end{array}$

The idea is that $ϵ (s)$ captures the part of the guess $f_{s}$ makes about what C looks like which would be realized by $A_{s + 1}$ .12
¹²
Note that we need to wait until stage $s + 1$ until the axioms enumerated at stage s appear in $A$ .

Note that $ϵ (s)$ is always defined on ${n \in ω | n < s}$ since $k_{s + 1}^{β} > s$ .

We can now formalize the idea that the outcome our construction guesses at any given stage is compatible with the results of the axioms enumerated so far.
Lemma 5.6.
Suppose $β ⪯ f_{s}$ and $A_{s + 1}$ yields $X_{β, s}$ over $C_{β}, δ_{β}$ then $X_{β, s} ≻ ϵ (s)$ .

We will prove this lemma via induction but, for clarity, we separate out the largely technical inductive step.
Lemma 5.7.
Suppose $β^{+} ⪯ f_{s}$ and $A_{s + 1}$ yields $X_{β, s}$ over $C_{β}, δ_{β}$ then
$X_{β, s} ≻ {ϵ (s)}^{[< l_{β^{+}}]}$

$δ_{β^{+}} ≺ X_{β, s}$

In other words this lemma asserts that $X_{β, s}$ agrees with $ϵ (s)$ on the domain of both $C_{β^{+}}$ and $δ_{β^{+}}$ .
Proof.
(1) Note that agreement on $C_{β}$ comes for free, so it is enough to verify $ϵ (s)$ agrees with $X_{β, s}$ on the columns used by β. By Lemma 5.4 we may ignore any axioms enumerated by nodes incompatible with β visited after β and by part 2 of Condition 1 any axioms enumerated by incompatible nodes before β is visited can be ignored as they don’t have effect outside of $dom δ_{β}$ . Axioms enumerated by nodes compatible with β other than β either don’t have effect outside $dom C_{β}$ or only affect columns after those reserved for β. It is thus enough to examine the construction and note that at stages where $β^{+} ≺ f_{s}$ the axioms enumerated by β (on the assumption $C_{β}, δ_{β} ≺ C$ ) suffice to yield $δ_{s}$ on the columns used by β. This is straightforward for module $N_{β}$ and for module $R_{β}$ is entailed by the discussions immediately preceding Eqs (4.2) and (4.3).

(2) This claim is trivial if $β^{+} = β^{⌢} ⟨ 0 ⟩$ as, in this case, $δ_{β^{+}} = δ_{β}$ so assume $β^{+} = β^{⌢} ⟨ w ⟩, w \neq 0$ .

Since we assume $δ_{β} ≺ C$ , as above, Lemma 5.4 and part 2 of Condition 1 let us ignore any axioms not enumerated by β or a descendant. Note that if β implements $N_{β}$ there are only two possible outcomes and if β implements $R_{β}$ then $dom {δ_{β^{⌢} ⟨ w ⟩}}^{[⩾ l_{β^{+}}]} = dom {δ_{β^{⌢} ⟨ w^{'} ⟩}}^{[⩾ l_{β^{+}}]}$ for any $w, w^{'} > 0$ . As no descendant of $δ_{β^{⌢} ⟨ w ⟩}$ is allowed to enumerate elements into $dom δ_{β^{⌢} ⟨ w^{'} ⟩}$ only axioms enumerated by β and nodes extending $β^{⌢} ⟨ 0 ⟩$ can affect $X_{β, s}$ on $dom δ_{β^{+}}$ . Let t be first the stage some child of β besides $β^{⌢} ⟨ 0 ⟩$ is visited. Since outcome 0 is never revisited it is enough to show that $A_{t}$ plus any axioms enumerated by β by or at stage s yield $δ_{β^{+}}$ over $C_{β}, δ_{β}$ .

If β implements $N_{β}$ then at stage t we defined $δ_{β^{+}} = δ_{β^{⌢} ⟨ 1 ⟩}$ to be $X ↾_{l}$ where X is the result of $A_{t}$ plus the axiom enumerated by β at stage t over $C_{β}, δ_{β}$ and no further axioms are ever enumerated by β. If β implements $R_{β}$ then the discussion preceding Eq. (4.2) and an examination of the behavior of the module guarantees that the definition13
¹³
Note that if $β^{+} = β^{⌢} ⟨ 1 ⟩$ then at every stage $β^{+}$ is visited all axioms enumerated by β are canceled as is reflected in the definition of $δ_{β^{⌢} ⟨ 1 ⟩}$ . If $β^{+} \neq β^{⌢} ⟨ 1 ⟩$ then it is enough to verify the claim for the first stage s at which $β^{+}$ is visited since β enumerates no further axioms until permanently abandoning the outcome corresponding to $β^{+}$ .

of $δ_{β^{+}}$ takes account of $A_{t}$ and all the axioms enumerated up through stage s by β, i.e., is compatible with the set yielded by those axioms over $C_{β}, δ_{β}$ . □

We now give the proof of Lemma 5.6.
Proof.
We prove this claim by (reverse) induction on β, i.e., with base case $β = f_{s}$ . First we note that if $β = f_{s}$ then the claim holds trivially since $ϵ (s) ≺ C_{β} \cup δ_{β}$ . Now, assume the claim holds for all $β^{'}$ with $β ≺ β^{'} ⪯ f_{s}$ . Let $β^{+}$ be the child of β satisfying $β ≺ β^{+} ⪯ f_{s}$ .

By part 2 of Lemma 5.7 we know that $X_{β, s} ≻ δ_{β^{+}}$ . If $V = ω^{[⩽ l_{β^{+}}]}$ then by part 1 of Lemma 5.7 we also have $X_{β, s} ≻ ϵ (s) ↾_{V}$ . By Definition 5.5 this implies $X_{β, s}$ extends $C_{β^{+}}$ excepting only those locations in column $l_{β}$ where $ϵ (s)$ is undefined if β implements $R_{β}$ . However, no node other than β ever enumerates axioms dependent on these locations and β only enumerates elements inside V so we may proceed as if $X_{β, s}$ extended $C_{β^{+}}$ in determining the behavior of $X_{β, s}$ on $\overline{V}$ . By the inductive assumption $ϵ (s) ≺ X_{β^{+}, s}$ which is the set yielded by $A_{s + 1}$ over $C_{β^{+}} \cup δ_{β^{+}}$ . By the previous remark $X_{β, s} ↾_{\overline{V}} = X_{β + 1, s} ↾_{\overline{V}}$ and thus $X_{β, s} ≻ ϵ (s) ↾_{\overline{V}}$ . Putting this together with the above mentioned fact that $X_{β, s} ≻ ϵ (s) ↾_{V}$ lets us derive $X_{β, s} ≻ ϵ (s)$ . □
Lemma 5.8.
$\begin{matrix} C = ⋃_{α ≺ f} C_{α} \end{matrix}$

Moreover, if $α ≺ f$ then $δ_{α} ≺ C$ .
Proof.
It is enough to show that if $α ≺ f$ then $C_{α} ≺ C$ since $dom ⋃_{α ≺ f} C_{α} = ω$ and if $β ≻ α$ then $δ_{β} ≻ δ_{α}$ and $δ_{β}$ is (by construction) always compatible with $C_{α}$ .

We prove that $α ≺ f ⟹ C_{α} ≺ C$ by induction on α. Note that the claim is trivially true for $α = \emptyset$ so we assume the claim holds for α and that $α^{+} ≺ f$ and demonstrate $C_{α^{+}} ≺ C$ . We first show that ${C_{α^{+}}}^{[l_{α}]} ≺ C$ . Let z be in column $l_{α}$ and find $s_{0}$ large enough that if $s ⩾ s_{0}$ then $z \in dom ϵ (s)$ (by the note after Definition 5.5 $s_{0} = z + 1$ suffices). First, suppose $C (z) = 1$ . By Lemma 2.2 let $⟨ l : σ \to z ⟩ \in A$ witness the fact that $C (z) = 1$ and let $s > s_{0}$ with $α^{+} ≺ f_{s}$ and $⟨ l : σ \to z ⟩ \in A_{s}$ . By Definition 2.1 $dom σ \subset ω^{[< l_{α}]}$ . Thus, since $σ ≺ C$ and, by the inductive hypothesis, $C_{α} ≺ C$ , we have $σ ≺ C_{α}$ and thus $X_{α^{+}, s} (z) = 1$ . By Lemma 5.6 $X_{α^{+}, s} ≻ ϵ (s)$ so $ϵ (s) (z) = 1$ and by Definition 5.5 we can infer $C_{α^{+}} (z) = 1$ .

Conversely, suppose $C (z) = 0$ but $C_{α^{+}} (z) = 1$ . Again let $s > s_{0}$ with $α^{+} ≺ f_{s}$ and apply Lemma 5.6 to infer $X_{α^{+}, s} ≻ ϵ (s)$ . As $ϵ (s) (z) = C_{α^{+}} (z) = 1$ there must be some axiom $⟨ l : σ \to z ⟩ \in A$ witnessing $X_{α^{+}, s} (z) = 1$ and, as $X_{α^{+}, s} ≻ C_{α}$ , we can infer that $C (z) = 1$ for a contradiction. Thus, $C_{α^{+}} (z) = 0$ .

If α implements a module of the form $N_{α}$ we are done. Otherwise we prove the claim for column $l_{α} + 1$ in a similar fashion, using the fact that ${C_{α^{+}}}^{[l_{α}]} ≺ C$ . The argument that $C (z) = 1$ (where z is now in column $l_{α} + 1$ ) implies $C_{α^{+}} (z) = 1$ goes through with only the slight modification of choosing s large enough that $dom ϵ (s) \supset dom σ$ to ensure that $X_{α^{+}, s} (z) = 1$ .

Provided $α^{+} \neq α^{⌢} ⟨ 1 ⟩$ the same strategy works to show $C (z) = 0$ implies $C_{α^{+}} (z) = 0$ as well, since in this case ${ϵ (s)}^{[l_{α}]} = {C_{α^{+}}}^{[l_{α}]} ≺ C$ . However, if $α^{+} = α^{⌢} ⟨ 1 ⟩$ we instead use the fact that the only values of z for which $C_{α^{+}} (z) = 1$ are enumerated via axioms that, by Eqs (4.2) and (4.3), don’t depend on any elements outside of $dom δ_{α^{+}} \subset dom ϵ (s)$ , i.e., $C_{α^{⌢} ⟨ 1 ⟩} (z) = 1$ only if $δ_{α^{+}} (z)$ which is enough to complete the proof. □
Lemma 5.9.
C is not computable.
Proof.
If C were computable then $\overline{C} = W_{e}$ for some e. Now pick $α ≺ f$ such that α implements a module $N_{α}$ working to satisfy $N_{e}$ , and let y be as in the description of the module. Now if $y \in W_{e}$ then the truepath extends $α^{⌢} ⟨ 1 ⟩$ and $y \in C_{α^{⌢} ⟨ 1 ⟩}$ . Otherwise the truepath extends $α^{⌢} ⟨ 0 ⟩$ and $y \notin C_{α^{⌢} ⟨ 1 ⟩}$ . Either way, the previous lemma ensures that $\overline{C} \neq W_{e}$ . □
Lemma 5.10.
Suppose that $α ≺ f$ implements $R_{α}$ working to satisfy $R_{e, i}$ and there are stages $s_{0} < s_{1}$ such that
$R_{α}$ isn’t activated at or before $s_{1}$

$α ≺ f_{s_{0}}, f_{s_{1}}$

$Φ_{i} (ϵ (s_{0}) ↾_{s_{0}}) ↓_{s_{0}} ∣ Φ_{i} (ϵ (s_{1}) ↾_{s_{1}}) ↓_{s_{1}}$
then at the least stage $s > s_{1}$ with $α ≺ f_{s}$ $R_{α}$ is activated.
Proof.
To prove the claim we must show there are $Y_{0}, Y_{1}, x, y$ satisfying Eq. (4.1) at stage s. We let $Y_{0} = ϵ (s_{0}) ↾_{s_{0}}$ , $Y_{1} = ϵ (s_{1}) ↾_{s_{1}}$ and let x be a location at which the computations disagree. We choose y to be the value $⟨ l_{α} + 1, m_{l}^{α} ⟩$ where l is the least number greater than $s_{0}$ such that $m_{l}^{α}$ is defined.

By Lemma 5.6 $ϵ (s_{0}) ↾_{s_{0}} ≺ {\hat{C}}_{0}$ and $ϵ (s_{1}) ↾_{s_{1}} ≺ C_{1}$ , where ${\hat{C}}_{0}$ is the result of $A_{s_{0} + 1}$ over $C_{α}, δ_{α}$ and $C_{1}$ is the result of $A_{s_{1} + 1}$ over $C_{α}, δ_{α}$ . By Lemma 5.4, $C_{1}$ is also the result of $A_{s}$ over $C_{α}, δ_{α}$ , since α isn’t visited in the interval $(s_{1}, s)$ . To verify the claim we need only show that if $C_{0}$ is the result of $A_{s} \cup {⟨ l_{α} + 1 : \emptyset \to y ⟩}$ over $C_{α}, δ_{α}$ then $ϵ (s_{0}) ↾_{s_{0}} ≺ C_{0}$ .

By Lemma 5.4 any axiom enumerated by $β ∣ α$ after $s_{0}$ is incompatible with $δ_{α}$ , no axiom enumerated by $β ≺ α$ enumerates any element outside of $dom C_{α}$ , by assumption α isn’t activated and therefore enumerates no axioms before stage s and by global rule (II) any axiom enumerated by $β ≻ α$ is enumerated dependent on $C (y) = 0$ . As y is chosen large after stage $s_{0}$ it follows that ${\hat{C}}_{0} ↾_{s_{0}} = C_{0} ↾_{s_{0}}$ establishing the claim. □
Lemma 5.11.
If $V \in Δ_{2}^{0}$ and $V ⩽_{T} C$ then V is computable.
Proof.
By assumption there is some e such that $V = {lim}_{s \to \infty} V_{e, s}$ and i such that $Φ_{i} (C) = V$ . Let $α ≺ f$ be a node implementing the module $R_{α}$ working to meet $R_{e, i}$ . By construction, if $R_{α}$ is ever activated with $Y_{0}, Y_{1}, x, y$ witnessing the satisfaction of Eq. (4.1) then $f ≻ α^{+}$ with $Φ_{i} (δ_{α^{+}}; x) ↓ \neq V (x)$ . By Lemma 5.8 $C ≻ δ_{α^{+}}$ contradicting the assumption that $Φ_{i} (C) = V$ . Thus, we may assume that $R_{α}$ is never activated.

In this case we claim $V (x) = Φ_{i} (ϵ (s) ↾_{s}; x)$ for some stage s such that $α ≺ f_{s}$ and $Φ_{i} (ϵ (s) ↾_{s}; x) ↓_{s}$ . By Lemmas 5.6 and 5.8 whenever $f_{s} ≺ f$ we have $ϵ (s) ≺ C$ . Thus, as $Φ_{i} (C) = V$ and $ω ↾_{s} \subset dom ϵ (s)$ such a stage must always exist. If there were two such stages $s_{0}, s_{1}$ which disagreed on the value of $V (x)$ then, by Lemma 5.10, $R_{α}$ would eventually be activated. Hence, by searching for the first stage s satisfying the above, we witness the computability of V. □

This completes the proof of Theorem 1.2.
6. Generalizations

At this point, one might naturally wonder if this result could be improved by moving to ordinals past ω. One might conjecture there is some $ω \cdot ω$ -REA degree C that forms a nontrivial minimal pair with ${\underset{~}{0}}^{″}$ . Disappointingly this conjecture turns out to be false. We sketch the proof below following the same approach as in Proposition 1.3 but now considering limit stages. The notation we use for computable ordinals is from [4]. Note that for the remainder of the paper we let $α, β, λ$ and γ range over $O^{}$ , i.e., notations for constructive ordinals.

We first remind the reader of the definition of an α-REA set. We differ from the definition in [1] only in that we define α-REA sets and not all α-REA operators.

Definition 6.1 (α-REA set).

An α-REA set is a set of the form $C_{f}^{α}$ , for a computable function f defined on ${β | β <_{O^{}} α}$ , where $C_{f}^{α}$ is recursively defined as follows.

$C_{f}^{0} = \emptyset$

$C_{f}^{β +_{O^{}} 1} = C_{f}^{β} \oplus W_{f (β)}^{C_{f}^{β}}$

$C_{f}^{λ} = ⨁_{β <_{O^{}} λ} C_{f}^{β}$ if λ a limit.

α

-REA set for an ordinal

α

is a α-REA set for any notation α with

| α | = α

Lemma 6.2.

For any α-REA set $C_{f}^{α} ⩽_{T} \underset{~}{0}$ , ${\underset{~}{0}}^{″}$ can (uniformly in α and an index for f) compute an index for $C^{α}$ as a c.e. set.

Proof.

The essential idea here is that ${\underset{~}{0}}^{″}$ can search for indexes giving a computable definition for $C_{f}^{α}$ which it then verifies by using those indexes to generate computable indexes for the sets $C_{f}^{β}, β <_{O^{}} α$ . Using the definition of $C_{f}^{α}$ as an α-REA set ${\underset{~}{0}}^{″}$ can then check that the version of $C_{f}^{α}$ built back up from the computable indexes for $C_{f}^{β}, β <_{O^{}} α$ matches the initial guess at $C_{f}^{α}$ . As this procedure can check that $C_{f}^{α}$ satisfies every part of Definition 6.1.

We will show that we can uniformly computably generate an index for $C_{f}^{α}$ as a c.e. set from a guess at a computable definition for $C_{f}^{α}$ such that the sets only agree when our guess was accurate. In particular, we prove that there is a computable function $q (γ, i_{γ}, {\hat{i}}_{γ}) = v_{γ}$ such that $\begin{matrix} (6.1) & W_{i_{γ}} = \overline{W_{{\hat{i}}_{γ}}} ⟹ (W_{i_{γ}} = W_{q (γ, i_{γ}, {\hat{i}}_{γ})} ⟺ W_{i_{γ}} = C_{f}^{γ}) . \end{matrix}$

Note that this suffices to prove the claim since we can now find a c.e. index for $C_{f}^{α}$ simply by searching for a pair $i_{γ}, {\hat{i}}_{γ}$ such that $W_{i_{γ}} = \overline{W_{{\hat{i}}_{γ}}}$ and $W_{i_{γ}} = W_{q (γ, i_{γ}, {\hat{i}}_{γ})}$ . Applying the above equation in the other direction ensures us that there is a solution and since we can verify such a solution computably in ${\underset{~}{0}}^{″}$ this suffices to prove the claim.

We now construct q by using definition via effective transfinite recursion. We will define a computable function $I (e)$ such that $Φ_{I (e)} (γ, i_{γ}, {\hat{i}}_{γ})$ satisfies Eq. (6.1) if for all $β <_{O^{}} γ$ , $Φ_{e} (β, i_{β}, {\hat{i}}_{β})$ satisfies Eq. (6.1) with respect to β. Then by application of the recursion theorem [3] we will recover a fixed point e such that $Φ_{I (e)} ≃ Φ_{e}$ is the desired function satisfying Eq. (6.1).

Before we construct $I (e)$ , we observe that there is a total computable function h such that for all β if $C_{f}^{β} = W_{i}$ and $\overline{C_{f}^{β}} = W_{\hat{i}}$ then $C_{f}^{β +_{O^{}} 1} = W_{h (β, i, \hat{i})}$ and for all $i, i^{'}$ , $W_{h (β, i, i^{'})} = W_{i} \oplus X$ for some X. The existence of h follows immediately from the computability of f and definition of $C_{f}^{β +_{O^{}} 1}$ . Additionally, there is a computable function g such that if $W_{i} = C_{f}^{γ}$ and $β <_{O^{}} γ$ then $C_{f}^{β} = W_{g (γ, β, i)}$ and if $W_{\hat{i}} = \overline{W_{i}}$ then $W_{g (γ, β, \hat{i})} = \overline{W_{g (γ, β, i)}}$ . Such a g exists as it merely unwraps14

¹⁴

More formally, we define g as follows. If $γ = β$ then $g (γ, β, i) = i$ . Let $g (β +_{O^{}} 1, β, i)$ return the index such that $W_{g (β +_{O^{}} 1, β, i)} = {2 x | x \in W_{i}}$ . If $β^{'} <_{O^{}} β$ define $g (β +_{O^{}} 1, β^{'}, i) = g (β, β^{'}, g (β +_{O^{}} 1, β, i))$ . Finally, if λ a limit and $β <_{O^{}} λ$ then let g return the index such that $W_{g (λ, β, i)} = {x | ⟨ β, x ⟩ \in W_{i}}$ .

the effective join operations building up

C^{γ}

until it reaches

C^{β}

. Furthermore, we can assume that

W_{g (γ, β, i)}

is always empty unless

β <_{O^{}} γ

If $γ = 0$ then $Φ_{I (e)} (\emptyset; γ, i_{γ}, {\hat{i}}_{γ})$ returns a c.e. index for the empty set then Eq. (6.1) is obviously satisfied. If $γ = β +_{O^{}} 1$ then $Φ_{I (e)} (\emptyset; γ, i_{γ}, {\hat{i}}_{γ})$ first computes $i_{β} = g (γ, β, i_{γ})$ and ${\hat{i}}_{β} = g (γ, β, {\hat{i}}_{γ})$ and then $v_{β} = Φ_{e} (\emptyset; β, i_{β}, {\hat{i}}_{β})$ before returning $v_{γ} = h (β, v_{β}, {\hat{i}}_{β})$ . Clearly, if $W_{i_{γ}} = C_{f}^{γ}$ and $W_{i_{γ}} = \overline{W_{{\hat{i}}_{γ}}}$ then, by the properties of g, $W_{i_{β}} = C_{f}^{β}$ and by the inductive assumption $W_{i_{β}} = W_{v_{β}}$ . By the properties of h we can conclude $W_{i_{γ}} = W_{q (γ, i_{γ}, {\hat{i}}_{γ})}$ . Now, suppose, $W_{i_{γ}} = W_{q (γ, i_{γ}, {\hat{i}}_{γ})}$ and $W_{i_{γ}} = \overline{W_{{\hat{i}}_{γ}}}$ . The definition of h ensures that $W_{q (γ, i_{γ}, {\hat{i}}_{γ})}$ has the form $W_{v_{β}} \oplus X$ and the definition of g ensures that not only $W_{i_{β}} = \overline{W_{{\hat{i}}_{β}}}$ but also that $W_{i_{γ}}$ has the form $W_{i_{β}} \oplus X^{'}$ . Thus, it follows that $W_{i_{β}} = W_{v_{β}}$ and by the inductive assumption we can infer that $W_{i_{β}} = C_{f}^{β}$ . Hence, $\overline{W_{{\hat{i}}_{β}}} = W_{v_{β}}$ and by the definition of h it follows that $W_{i_{γ}} = C_{f}^{γ}$ .

If λ is a limit we define $Φ_{I (e)} (\emptyset; λ, i_{λ}, {\hat{i}}_{λ})$ . Using g we can, define $i_{β} = g (λ, β, i_{λ}), {\hat{i}}_{β} = g (λ, β, {\hat{i}}_{λ})$ as computable functions of $β <_{O^{}} λ$ and $v_{β} = Φ_{e} (\emptyset; () β, i_{β}, {\hat{i}}_{β})$ . Finally, let $v_{λ}$ be the index for $⨁_{β <_{O^{}} λ} W_{v_{β}}$ and output $v_{λ}$ . The verification is essentially the same as above. Supposing $W_{i_{λ}} = \overline{W_{{\hat{i}}_{λ}}}$ , if $C_{f}^{λ} = W_{i_{λ}}$ then $C_{f}^{β} = W_{i_{β}}$ and by the inductive assumption both are equal to $W_{v_{β}}$ which is enough to infer that $W_{i_{λ}} = W_{v_{λ}}$ . Going the other way, we note that if $W_{i_{λ}} = W_{v_{λ}}$ then we can infer agreement $W_{i_{β}} = W_{v_{β}}$ for each component and then use the inductive hypothesis plus the definition of λ-REA sets when λ a limit to show $W_{i_{λ}} = C_{f}^{λ}$ .

Finally, as mentioned above, $q (γ, i_{γ}, {\hat{i}}_{γ})$ is now defined to be $Φ_{e} (\emptyset; γ, i_{γ}, {\hat{i}}_{γ})$ where $Φ_{e} ≃ Φ_{I (e)}$ is a fixed point of I. □

Proposition 6.3.

Suppose that C is of non-computable α-REA degree then $C \land_{T} {\underset{~}{0}}^{″} ≢_{T} \underset{~}{0}$ .

Proof.

By the definition of α-REA sets $C = C_{f}^{α}$ . Thus, there is some least $β ⩽_{O^{}} α$ such that $C_{f}^{β}$ isn’t computable. If β is a successor then, just as in Proposition 1.3, $C^{β} ⩽_{T} {\underset{~}{0}}^{'}$ . So assume β is a limit. By Lemma 6.2 we can uniformly find a c.e. code for each $C^{γ}$ with $γ <_{O^{}} β$ . To determine if $⟨ γ, x ⟩ \in C_{f}^{β}$ , we first ask ${\underset{~}{0}}^{″}$ if $γ <_{O^{}} β$ . If not $⟨ γ, x ⟩ \notin C^{β}$ . Otherwise ask ${\underset{~}{0}}^{″}$ for a c.e. code i for $C_{f}^{γ}$ and report $⟨ γ, x ⟩ \in C_{f}^{β}$ iff ${\underset{~}{0}}^{″}$ determines $x \in C_{f}^{γ}$ . Hence, in either case, $\underset{~}{0} <_{T} C^{β} ⩽_{T} {\underset{~}{0}}^{″}$ and as $C^{β} ⩽_{T} C$ we have $C \land_{T} {\underset{~}{0}}^{″} ≢_{T} \underset{~}{0}$ . □

Footnotes

Acknowledgements

Partially supported by NSF EMSW21-RTG-0739007 and EMSW21-RTG-0838506.

References

C.G.

Jockusch and

R.A.

Shore, Pseudojump operators II: Transfinite iterations, hierarchies and minimal covers, The Journal of Symbolic Logic 49 (1984), 1205–1236. doi:10.2307/2274273.

S.C.

Kleene, General recursive functions of natural numbers, Math. Ann. 112(1) (1936), 727–742. doi:10.1007/BF01565439.

S.C.

Kleene, On notation for ordinal numbers, The Journal of Symbolic Logic 3(4) (1938), 150–155. doi:10.2307/2267778.

G.E.

Sacks, Higher Recursion Theory, Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1990.

J.R.

Shoenfield, On degrees of unsolvability, Ann. of Math. (2) 69 (1959), 644–653. doi:10.2307/1970028.

R.I.

Soare, Recursively Enumerable Sets and Degrees: A Study of Computable Functions and Computably Generated Sets, Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1987.