Extending properly n

Abstract

In 1982, Soare and Stob proved that if A is an r.e. set which isn’t computable then there is a set of the form $A \oplus W_{e}$ which isn’t of r.e. Turing degree. If we define a properly $n + 1$ -REA set to be an $n + 1$ -REA set which isn’t Turing equivalent to any n-REA set this result shows that every properly 1-REA set can be extended to a properly 2-REA set. This result was extended by Cholak and Hinman in 1994. They proved that every 2-REA set can be extended to a properly 3-REA set. This leads naturally to the hypothesis that every properly n-REA set can be extended to a properly $n + 1$ -REA set. Here we show this hypothesis is false and that there is a properly 3-REA set which can’t be extended to a properly 4-REA set. Moreover we show this set A can be $Δ_{2}^{0}$ .

Keywords

REA sets recursively enumerable and above Turing degree recursively enumerable computability theory recursion theory

1. Introduction

In [1] Jockusch and Shore introduce the $n - REA$ sets. A $1 - REA$ set is just an $r.e.$ set, while an $n + 1 - REA$ set is a set of the form $A \oplus W_{e}^{A}$ where A is $n - REA$ . Despite the fact that the $n - REA$ sets are merely the result of iterating the operation of adding an $r.e.$ set, many basic questions remain even when n is finite.

One natural property to investigate about $n - REA$ sets is when they are properly $n - REA$ .

Definition 1.1.
A set B is properly $n - REA$ if B is $n - REA$ and B isn’t Turing equivalent to any $m - REA$ set with $m < n$ .

It is evident that for all $n \in ω$ there are properly $n - REA$ sets. But it’s obviously not the case that for every $n - REA$ set A there is a properly $n + 1 - REA$ set of the form $A \oplus W_{e}^{A}$ , i.e., not every $n - REA$ set can be extended to a properly $n + 1 - REA$ set. For instance, the empty set is a $1 - REA$ set but can’t be extended to a properly $2 - REA$ set.

A natural hypothesis is that any properly $n - REA$ set can be extended to a properly $n + 1 - REA$ set. This represents the most optimistic possible hypothesis about when $n - REA$ sets can be extended to properly $n + 1 - REA$ sets.
Hypothesis 1.2.
If A is a properly $n - REA$ set then there is a properly $n + 1 - REA$ set (Turing equivalent to a set2
²
We add this caveat because, in the argument below, we adopt a slightly different form for $n - REA$ sets that makes the argument more convenient.

) of the form $A \oplus W_{e}^{A}$ . In such cases, we say A can be extended to a properly $n + 1 - REA$ set.

Further evidence for this hypothesis comes in the form of a result by Soare and Stob [5] who demonstrate that for any $r.e.$ set $W_{e} >_{T} 0$ there is a set $1 - REA$ in $W_{e}$ but not of $r.e.$ degree. This establishes that every properly $1 - REA$ set can be extended to a properly $2 - REA$ set. This result was extended to $n = 2$ by Cholak and Hinman when they established the following result (recast using the above definitions) in [2].
Theorem 1.3.
If X is properly $2 - REA$ then there is a $REA (X)$ set $W_{e}^{X} \oplus X$ which is properly $3 - REA$ .

In other words any $2 - REA$ set which isn’t of $r.e.$ degree can be extended to a $3 - REA$ set not of $2 - REA$ degree. However, despite the suggestive evidence we show that the above attractive hypothesis in fact fails by proving the following theorem.
Theorem 1.4.
There is a properly $3 - REA$ set A which can’t be extended to a properly $4 - REA$ set. The set A can also be taken to be $Δ_{2}^{0}$ .

Note that, if A isn’t properly $3 - REA$ then it is evident that no set of the form $A \oplus W_{e}^{A}$ will be properly $4 - REA$ . Our strategy, roughly speaking, will be to build a $3 - REA$ set A such that enumeration into the first and second components of A (where the first component of A is the $r.e.$ part of A and the second component is the part of A $r.e.$ in the first component) doesn’t result in further changes to $W_{i}^{A}$ . The construction takes the form of a finite injury argument, with the complexity arising from the difficulty of showing that the requirements eventually succeed. However, before we present the main construction, we first review some notation and define the $n - REA$ sets in Section 2. Note that in this section we also introduce the idea that $n - REA$ sets can be viewed as $n + 1$ column sets (with the 0-th column empty) produced by an $r.e.$ set of axioms.

Readers familiar with $n - REA$ sets may wish to jump ahead to Section 3, where we describe the requirements that our construction will meet and delineate some basic conditions that our construction will satisfy.
2. Background

2.1. Notational conventions

We largely adopt the standard notation seen in [3] which we briefly review. The use of $Φ_{i, s} (X; y)$ is denoted by $u [Φ_{i, s} (X; y)]$ , the e-th set $r.e.$ in X by $W_{e}^{X}$ and we write $y ↘_{s} X$ ( $y ↘_{s} \overline{X}$ ) to indicate y enters (leaves) X at stage s. We let $⟨ ⟨ x_{0}, \dots x_{n} ⟩ ⟩$ ( $⟨ x, y ⟩ \overset{def}{=} \frac{1}{2} (x + y) (x + y + 1) + y$ ) denote a canonical bijection of $ω^{< ω}$ ( $ω^{2}$ ) with ω and define $A \oplus B$ , $⨁_{n \in S} X_{n}$ and $X^{[n]} / X^{[< n]}$ standardly.3

³
That is, $A \oplus B \overset{def}{=} {y ∣ y = 2 x \land x \in A \lor y = 2 x + 1 \land x \in B}$ and $⨁_{n \in S} X_{n} \overset{def}{=} {⟨ n, x ⟩ | n \in S \land x \in X_{n}}$ .

We write

σ | τ

(

σ / | τ

) to indicate that two strings/partial functions/etc. are incompatible (compatible).

We also adopt some less common notational conventions and assumptions. We let the variables χ, ξ, η range over ${0, 1, ↑}^{< ω}$ (binary partial functions with finite domain) with extension denoted by ≻. By identifying sets with their characteristic functions (so $A_{s}$ is really a ${0, 1, ↑}^{< ω}$ ) we gain the ability for our approximations to a set A to take no position on whether $x \in A$ . This turns out to be helpful in giving well-behaved stagewise approximations to $n - REA$ sets.

With this notation in place, we briefly review $n - REA$ sets and describe how we identify such sets with $n + 1$ (non-trivial) column sets (and whose remaining columns are empty). The reader familiar with $n - REA$ sets may wish to skip ahead to Section 3 after familiarizing themselves with the notion of an A supported approximation in Definition 2.6.

2.2.

α - REA

sets

In [1] Jockusch and Shore introduce the $α - REA$ sets for any ordinal notation $α \in O_{1}$ . In this paper, we will only be concerned with finite values of α so we adopt the following definition (equivalent up to 1-degree for finite α).

Definition 2.1.
Given a computable function f, we define the $n - REA$ operator $J_{f}^{n} (X)$ (or $J_{e}^{n} (X)$ where e is an index for f), $n \in ω$ via the following inductive definition (where we let $W_{f (m)}^{Z} = \emptyset$ if $f (m) ↑$ ). $\begin{array}{l} {\hat{J}}_{f}^{0} (X) = X \\ (1) & {\hat{J}}_{f}^{m + 1} (X) = W_{f (m)}^{J_{f}^{m} (X)} \\ J_{f}^{n} (X) = ⨁_{m < n + 1} {\hat{J}}_{f}^{m} (X) \end{array}$ Furthermore, C is an $n - REA (X)$ set just if $C = J_{f}^{n} (X)$ for some computable function f and C is an $n - REA$ set if it is an $n - REA (\emptyset)$ set. We define $X_{e}^{n}$ (written just as $X_{e}$ when n is understood) to be $J_{e}^{n} (\emptyset)$ .

Note that, because of how we define $⨁_{m < n + 1}$ an $n - REA (X)$ set Z will have $Z^{[m]} = \emptyset$ for $m > n$ . We further note that we can describe the construction of $n - REA (X)$ with $n \in ω$ sets via the enumeration of ‘axioms’ defined as follows.
Definition 2.2.
An axiom is a pair $⟨ σ \to y ⟩$ with $σ \in {0, 1, ↑}^{< ω}$ , $y \in ω$ . An REA axiom is an axiom that further satisfies $y = ⟨ m, z ⟩$ with $m > 0$ and $dom σ \subset ω^{[< m]}$ . Finally, an n-REA axiom is an REA axiom with $m ⩽ n$ .

We think of the axiom $⟨ σ \to y ⟩$ as an instruction to put y into a set Z provided $σ ≺ Y$ . Thus, regarding y as coding an element of $2^{< ω}$ , an $r.e.$ set of axioms defines (if compatible) a computable functional. An REA axiom $⟨ σ \to ⟨ m, z ⟩ ⟩$ is then an instruction to put z into $X^{[m]}$ provided $σ ≺ X^{[< m]}$ (as this is equivalent to $σ ≺ X$ ).

We now argue that for $n \in ω$ we may identify $n - REA$ operators $J_{e}^{n}$ (and hence $n - REA (X)$ sets) with $r.e.$ sets of n-REA axioms and effectively translate between $r.e.$ indices for sets of n-REA axioms and indices for $n - REA$ operators.
Lemma 2.3.
If A is a $r.e.$ set of $n - REA$ axioms ( $n \in ω$ ) then the operator $J_{A}^{n}$ defined by $\begin{matrix} (2) & ⟨ l, y ⟩ \in J_{A}^{n} (X) ⟺ (l = 0 \land y \in X) \lor \exists [σ ≺ J_{A}^{n} (X)] [⟨ σ \to ⟨ l, y ⟩ ⟩ \in A] \end{matrix}$ is an $n - REA$ operator. Conversely, given an $n - REA$ operator $J_{f}^{n}$ there is a $r.e.$ set $A_{f}$ such that $J_{A_{f}}^{n} = J_{e}^{n}$ . Furthermore, we can effectively translate between $r.e.$ indices of sets of $n - REA$ axioms and indices of $n - REA$ operators.
Proof.
We first prove that $J_{A}^{n}$ is an $n - REA$ operator. Note that, for $0 < l ⩽ n$ , $J_{A}^{n} (X)^{[l]}$ is determined by $J_{A}^{n} (X)^{[< l]}$ and X so $J (X)$ is well defined. Furthermore, the above equation explicitly defines $J_{A}^{n} (X)^{[l]}$ from $J_{A}^{n} (X)^{[< l]}$ and l via a (uniformly) $Σ_{1}^{0}$ formula. Thus, by an application of the s-m-n theorem [4] there is a computable function f satisfying Definition 2.1.

Given $J_{e}^{n}$ we simply enumerate axioms $⟨ σ \to ⟨ m + 1, x ⟩ ⟩$ into A when $Φ_{f (m)} (σ; x) ↓$ for $m < n$ . The uniformity claim is evident from the proof. □

In light of this result we adopt the following notation.
Notation 2.4.
$A (J)$ denotes a canonical enumeration of an $r.e.$ set of axioms corresponding to the $n - REA$ operator J. When $X_{e}$ is an $n - REA$ set we write $A (X_{e})$ for $A (J_{e}^{n})$ (remember $X_{e} \overset{def}{=} J_{e}^{n} (\emptyset)$ )

In various cases we’ll further specify which of the many potential enumerations of axioms we mean to specify with $A (X_{e})$ . For instance, we’ll explicitly define the enumeration of axioms for the $n - REA$ sets we explicitly construct and rely on Lemma 2.3 to produce the corresponding $n - REA$ set. We adopt the following definition to assist us in defining the axioms we enumerate in these construction.
Definition 2.5.
The axiom $⟨ σ^{'} \to y ⟩$ depends on σ if $σ ≺ σ^{'}$ . We say the axiom $⟨ σ \to y ⟩$ (element y) is enumerated dependent on δ to mean we enumerate $⟨ σ \cup δ \to y ⟩$ $⟨ δ \to y ⟩$ into A.

We will call an axiom $⟨ σ \to y ⟩$ compatible (incompatible) with a partial function τ just if the partial function σ determining when the axiom applies is compatible (incompatible) with τ. We now argue that we can use an axiom set to approximate an $n - REA$ set in well-behaved ways.
Definition 2.6.
If A is a set of n-REA axioms we say that $χ \in {0, 1, ↑}^{< ω}$ is A supported just if for all m, x with $χ (⟨ m, x ⟩) ↓$ all of the following hold
If $m = 0$ then $χ (⟨ m, x ⟩) = X (x)$ .

If $m > n$ then $χ (⟨ m, x ⟩) = 0$ .

If $0 < m ⩽ n$ then $χ (⟨ m, x ⟩) = 1 ⟺ (\exists σ) [⟨ σ \to ⟨ m, x ⟩ ⟩ \in A \land σ ≺ χ]$

If χ is an $A_{s} (J)$ supported approximation we say that χ is an s-supported4
⁴
Technically, being s-supported is relative to the choice of an enumeration of axioms but we will only use this notation when there is no ambiguity about the enumeration of the set $A (J)$ .

approximation to $J (X)$ .

Note that the notion of being s-supported is relative to a choice of a canonical enumeration of axioms for $J (X)$ . Also, it’s worth observing the following point.
Remark 2.7.
Given any set of axioms A and finite domain $D \subset ω$ there is a unique A-supported χ with domain D.

It turns out that for any $n - REA$ operator J we can effectively find an enumeration of axioms $A_{s}$ and a computable functional $Y_{s}^{X}$ with ${lim}_{s \to \infty} dom Y_{s} = ω$ , such that $Y_{s}^{X}$ is always an $A_{s}$ supported approximation to $J (X)$ and infinitely often $Y_{s}^{X} ≺ J (X)$ . A proof of this claim can be found in the appendix to give the reader an idea how this can work. However, we don’t actually need the full strength of this result and will instead directly specify a stagewise enumeration of axioms and a $A_{s}$ approximation $A_{s}$ to the $n - REA$ sets we are constructing. We will ensure this approximation has the following property (where A here is the $n - REA$ set being constructed).
Condition 1.
$(\exists^{\infty} s) A_{s} ≺ A$ .

In fact, our approximation to A (which we define below) will turn out to satisfy the stronger condition that there are infinitely many stages such that $(\forall t > s) A_{s} ≺ A_{t}$ . Note that, this implies that our approximation $A_{s}$ is a $Δ_{2}^{0}$ approximation to A.
3. Construction overview

We adopt the following notation for easier manipulation of $n - REA$ sets defined in terms of columns pursuant to Definition 2.1.

Definition 3.1.

$A \overline{\oplus} B \overset{def}{=} ⨁_{n \in ω} A^{[n]} \oplus B^{[n]}$ .

For A an $n - REA (X)$ set we let $A ↾_{[s]} = {⟨ k, x ⟩ | k ⩽ n \land x < s}$ .

$l_{s} > 4$ is a number chosen large5
⁵
Specifically, we will need that $l_{s}$ is large enough that if x is mentioned at or before stage s then $l_{s} > ⟨ k, x + 2 ⟩$ , $0 ⩽ k ⩽ 3$ so that $l_{s}$ is large enough to see the next two elements in each column.

at the end of stage s.

Note that if both A and B are both $n - REA$ then so is $A \overline{\oplus} B$ . Using these conventions we can now describe the broad outline of our proof of Theorem 1.4.

To establish the desired claim we’ll need to build a properly $3 - REA$ set A that can’t be extended to a properly $4 - REA$ set. In other words, for every $i \in ω$ the set $A \oplus W_{i}^{A}$ must not be properly $4 - REA$ . So in addition to the set A we’ll build a sequence of $3 - REA$ sets $A \overline{\oplus} Y_{i}$ Turing equivalent to the sets $A \oplus W_{i}^{A}$ (note that by using $A \overline{\oplus} Y_{i}$ rather than just $Y_{i}$ we avoid the need for unnecessarily copying changes to A over to $Y_{i}$ ). To verify these equivalences we’ll also need computable functionals so, in addition to the $3 - REA$ set A we’ll also build sets $Y_{i}$ and functionals $Γ_{i}$ , Θ to satisfy all of the following requirements where $X_{e}$ denotes the e-th $2 - REA$ set.
$P_{i}$ :
$Γ_{i} (A \oplus W_{i}^{A}) = Y_{i} \land Θ (Y_{i}) = W_{i}^{A}$
$R_{j, e}$ :
$Φ_{j} (A) \neq X_{e} \lor Φ_{j} (X_{e}) \neq A$

We now observe that satisfying the above requirements is sufficient to prove the claimed theorem. However, the impatient reader may wish to jump ahead to the informal description of how $R_{j, e}$ is met in Section 3.1. Note that the general method there will be familiar to anyone familiar with the methods in [2,5] and broadly resembles the construction of properly n- $r.e.$ sets (with some extra bookkeeping). Readers eager to jump ahead to the unique challenges and features of this construction should turn to Section 3.3 for an informal discussion or to the full construction in Section 4.

First we observe that our choice to avoid index profusion by using j as the index for both computations in $R_{j, e}$ is harmless.
Lemma 3.2.
Suppose A and $Y_{i}, i \in ω$ satisfy the requirements $P_{i}$ and $R_{j, e}$ for all i, j, e then A is properly $3 - REA$ but can’t be extended to a properly $4 - REA$ set.
Proof.
If $P_{i}$ is satisfied for all i it follows that the $3 - REA$ set $A \overline{\oplus} Y_{i}$ is Turing equivalent to $A \oplus W_{i}^{A}$ . It only remains to demonstrate that A is properly $3 - REA$ .

Suppose, for a contradiction, that $A \equiv_{T} X_{e}$ for some $2 - REA$ set $X_{e}$ . Then either $A^{[3]} = \emptyset$ , making A literally $2 - REA$ , or $A^{[3]} \neq \emptyset$ . In the first case $R_{j, e}$ would fail when j is an index for the identity function and e an index for the empty set. In the second case suppose that the Turing equivalence is witnessed by $Φ_{j_{0}} (A) = X_{e}$ and $Φ_{j_{1}} (X_{e}) = A$ and z is the least element in $A^{[3]}$ . Now let $Φ_{j} (Z)$ be the functional which asks if $⟨ 3, z ⟩ \in Z$ and if not computes $Φ_{j_{1}} (Z)$ and if so computes $Φ_{j_{0}} (Z)$ . Hence, if A is equivalent to some $2 - REA$ set $X_{e}$ it follows that some $R_{j, e}$ isn’t satisfied. □

We will build A or $Y_{i}$ by enumerating axioms into A and $A (Y_{i})$ respectively which, by the remarks above, uniquely determines the corresponding sets. We will define approximations $A_{s}$ , $Y_{i, s}$ to the sets A, $Y_{i}$ and adopt the convention that an attempt to enumerate x into A (or $Y_{i}$ ) at stage s means enumerating x dependent on a large initial segment of the prior columns as defined by $A_{s}$ , $Y_{i, s}$ .

We now formally specify our approximation $A_{s}$ and specify some properties it will be constructed to have.
Property 1.

$A_{s}$ is the unique s-supported approximation (i.e., $A_{s}$ -supported) with $dom A_{s} = ω ↾_{[l_{s}]}$ .

If x is enumerated into $A^{[k]}$ at stage s then $x \notin A_{s - 1}^{[k]}$ and x is enumerated dependent on $A_{s}^{[k^{'}]}$ for $k^{'} < k$ (hence on prior columns of A up to height $l_{s}$ ).

At odd stages no axioms are enumerated into A and at most one axiom is enumerated into A at even stages.

To avoid the potential circularity induced by the interaction of Definition 3.1 and Property 1 b we queue any request made to enumerate an element made during stage s until after $l_{s}$ is chosen at the end of the stage. Using $A_{s}^{[< n]}$ and $l_{s}$ we can build an axiom satisfying Property 1 b for an element queued for enumeration into $A^{[n]}$ which, in turn, lets us determine $A_{s}^{[< n + 1]}$ . Working inductively, this lets us identify an axiom for the element (if any) enumerated during stage s which satisfies both constraints.

We will also treat $W_{i}^{A}$ as the result of an enumeration of axioms $A_{s}^{i}$ and define an approximation $W_{i, s}^{A_{s}}$ that satisfies the following properties.
Property 2.

No axioms are enumerated into $A^{i}$ at even stages.

At any stage s there is at most one i and x such that an axiom enumerating some x into $W_{i}^{A}$ is enumerated and $i, x < s$ .

If an axiom enumerating x into $W_{i}^{A}$ is enumerated at stage s then x is enumerated dependent on $A_{s} ↾_{[l_{s}]}$ .

$W_{i, s}^{A_{s}}$ denotes the unique finite partial function with domain $ω ↾ l_{s}$ that is $A_{s}^{i}$ -supported.

$W_{i}^{A}$ is the set built by applying the axioms $A^{i}$ to the set A.

Property 2 c ensures that only axioms which agree with our current approximation $A_{s}$ to A are enumerated at stage s and are canceled by any change in $A_{s}$ . Note, these properties are only possible to meet, as we will now verify, because of Condition 1.
Lemma 3.3.
For all i there is an (uniformly specified) enumeration $A_{s}^{i}$ and an effective approximation $W_{i, s}^{A_{s}}$ satisfying Property 2 .
Proof.
We can assume we start with an enumeration of axioms $\hat{A_{s}^{i}}$ such that $x \in W_{i}^{A}$ iff $(\exists ⟨ σ \to x ⟩ \in A^{i}) (σ ≺ A)$ and satisfies the usual rules for the enumeration of an A- $r.e.$ set such as the enumeration of at most one element a stage etc. We now define $A_{s}^{i}$ in terms of the sets $A_{s - 1}^{i}$ , $i < s$ .

If s is even we do nothing. So assume s is odd and let $t < s$ be the minimal value such that we can find $i, y < s$ , $| σ | < s$ such that $⟨ σ \to y ⟩ \in \hat{A_{t}^{i}}$ , $σ ≺ A_{s - 1}$ and $W_{i, s - 1}^{A_{s - 1}} (y) = 0$ . If no such values can be found do nothing. If they are found enumerate the axiom $⟨ A_{s} \to y ⟩$ into $A_{s}^{i}$ . By construction, we clearly satisfy properties 2 a to 2 d. It remains to show that Property 2 e holds. By Condition 1 and Property 1 c we can assume that infinitely often we have an odd stage s with $A_{s - 1} ≺ A_{s} ≺ A$ , ensuring that eventually every element in $W_{i}^{A}$ gets an axiom enumerating it. □

We now give an overview of how each requirement operates.
3.1. Overview of $R_{j, e}$

The basic approach to meeting $R_{j, e}$ is to use the fact that A is $3 - REA$ to change our minds about the behavior of some initial segment of A more times than $X_{e}$ is able to track. We now give an informal description of the process which we depict graphically in Fig. 1. In the figure stages at which a well-behaved back and forth computation exists are indicated by shaded/hatched regions. The region of A which is either hatched or shaded indicates the use of a computation of the shaded region of $X_{e}$ , which in turn extends the use of a computation of the shaded region of A. We describe such computations as well-behaved when (at stage s) an s-supported region of A (hatched and shaded) computes (via $Φ_{j}$ ) $X_{e}$ on (at least) an s-supported region (shaded region) which in turn computes (via $Φ_{j}$ ) $A (⟨ 3, c ⟩)$ . We leave cells blank if empty – unless they’ve just been canceled by an enumeration into a prior column, in which case we place a 0 in the cell. Finally, we circle locations which conflict with a commitment made by $Φ_{j}$ at a prior stage.

Figure 1.

Meeting $*_{R}$ j,e.

We pick a value c at some stage $s_{- 1}$ which we hold out of $A^{[3]}$ . If we never see a stage $s_{0}$ and a well-behaved computation from A to $X_{e}$ and back then we are done. If we do see such a well-behaved computation then at stage $s_{0} + 1$ we enumerate c into $A^{[3]}$ dependent on some large value staying out of $A^{[2]}$ .

If at some stage $s_{1} > s_{0} + 1$ we again see a well-behaved back and forth computation (meaning $X_{e, s_{1}}$ disagrees with $X_{e, s_{0}}$ on the region shaded at stage $s_{0}$ ) we enumerate an element b into $A^{[2]}$ canceling c from $A_{s_{1} + 1}$ . This restores the computation from A to $X_{e}$ seen at stage $s_{0}$ . Note that the only way we can again see a well-behaved back and forth computation (given we restrain enumeration into A) is if our approximation to $X_{e}$ restores the (used part of the) state it had at $s_{0}$ by enumerating an element into $X_{e}^{[1]}$ to cancel any changes.

Now suppose that at some stage $s_{2}$ we again see a well-behaved back and forth computation. We respond by enumerating an element into $A^{[1]}$ at stage $s_{2} + 1$ canceling the enumeration made at stage $s_{1}$ into $A^{[2]}$ . This restores the computation from A to $X_{e}$ seen at stage $s_{1}$ . But now $X_{e}$ is unable to match this change as it can’t cancel the element enumerated into $X_{e}^{[1]}$ and, as we will prove in Section 3.1.1, the fact that A computed an s-supported approximation to $X_{e}$ at $s_{1}$ means this element was predicted by A to be out of $X_{e}$ at $s_{1}$ . This ensures that, provided we restrain modifications to A, we never again see a well-behaved $Φ_{j}$ computation from A to $X_{e}$ and back, guaranteeing that $R_{j, e}$ is satisfied.

We now formalize the argument made in this sketch and demonstrate that if the equivalence of A and $X_{e}$ is witnessed by $Φ_{j}$ then we will see infinitely many computations we’ve been calling well-behaved.

3.1.1. Positive change property

We now show that REA sets have the following positive change property. That is, the only way an approximation to an REA set can change is by enumerating a new element. We prove the results in this section for $n - REA$ sets for arbitrary n, as this result will help us understand the strategy used to satisfy $P_{i}$ .

Lemma 3.4.
Suppose χ, $χ^{'}$ are s, $s^{'}$ -supported approximations to an $n - REA (Z)$ set Y with $s < s^{'}$ and $dom χ^{'} \supseteq dom χ$ . If $χ (⟨ m, x ⟩) = 1$ but $χ^{'} (⟨ m, x ⟩) = 0$ then $χ |_{m - 1} χ^{'}$ . Moreover, there is a y and $m^{'} < m$ with $χ (⟨ m^{'}, y ⟩) = 0$ but $χ^{'} (⟨ m^{'}, y ⟩) = 1$ .
Proof.
To establish the first claim suppose that the hypotheses of the lemma are satisfied. By Definition 2.6 there is some axiom $⟨ σ \to y ⟩ \in A_{s} (Y)$ with $y = ⟨ m, x ⟩$ and $σ ≺ χ$ . As $dom σ \subset ω^{[m - 1]}$ if $χ^{'} / |_{m - 1} χ$ then $σ ≺ χ^{'}$ as $dom χ^{'} \supseteq dom χ$ . But then by Definition 2.6 we would have $χ^{'} (y) = 1$ , contrary to the assumptions of the lemma.

We now prove the second claim by induction. As $Y^{[1]}$ is $r.e.$ , the claim obviously holds for $m = 2$ . Now suppose the claim holds for any $m^{'} ⩽ m$ and that the hypotheses of the lemma are satisfied for $m + 1$ . Thus, $χ |_{m} χ^{'}$ . If there is some $y = ⟨ m^{'}, x ⟩$ with $m^{'} < m + 1$ and $χ (y) = 0$ and $χ^{'} (y) = 1$ , we are done. If not there must be a y with $χ (y) = 1$ and $χ^{'} (y) = 0$ . The result now follows by the inductive hypothesis applied to $y = ⟨ m^{'}, x ⟩$ . □

We now give a slightly modified version of the above lemma that is specifically phrased in terms of undoing a previous change.
Lemma 3.5.
Suppose χ, $χ^{'}$ , $χ^{″}$ are s, $s^{'}$ , $s^{″}$ -supported approximations to $J_{e}^{n} (Z)$ with $s < s^{'} < s^{″}$ , $χ^{″} ≻ χ$ and $χ^{'} |_{m} χ$ then $χ^{″} |_{m - 1} χ^{'}$ .
Proof.
Note that WLOG we may assume $dom χ^{″} \supset dom χ^{'}$ by restricting $χ^{'}$ to the domain of χ. With this assumption made, the pair χ, $χ^{'}$ satisfy the hypotheses of Lemma 3.4 or $χ^{'}$ , $χ^{″}$ do. As $χ^{″} ≻ χ$ whichever way we have $χ^{″} |_{m - 1} χ^{'}$ . □

We now define a predicate which holds at x, s if it appears that $A_{s}$ computes enough of $X_{e}$ for $X_{e}$ to correctly compute the value of $A_{s} (x)$ . Note that, in what follows, we will make use of an approximation $X_{e, s}$ to $X_{e}$ . However, somewhat surprisingly, all that matters about this approximation is that $X_{e, s}$ be s-supported and that, infinitely often, it’s domain includes any finite subset. As such, we can simply take $X_{e, s}$ to be the unique s-supported approximation such that $dom X_{e, s}^{[1]} = dom X_{e, s}^{[2]} = l_{s}$ even if this approximation isn’t even guaranteed to be (pointwise) infinitely often correct.
Definition 3.6.
We define $Ψ_{j, e} (x, s)$ (written $Ψ (x, s)$ when j, e is clear from context) to hold just when there is some s-supported approximation ξ to $X_{e}$ satisfying
$Φ_{j, s} (A_{s}) ≻ ξ$

$Φ_{j, s} (ξ) ≻ A_{s} ↾_{x + 1}$

We note that if $R_{j, e}$ fails we can always wait for a stage at which our approximation witnesses this failure.
Lemma 3.7.
If $Φ_{j} (A) = X_{e} \land Φ_{j} (X_{e}) = A$ , $A_{t} ≺ A$ then for any x there are infinitely many stages at which $Ψ (x, s)$ holds and is witnessed by $A_{s}$ , ξ where $A ≻ A_{s} ≻ A_{t}$ .
Proof.
Suppose $A_{t}$ is as in the lemma. We first note that it is enough to show one such $s > t$ exists, since further witnesses may be generated by applying this result. Moreover, we may presume that $x \in dom A_{t}$ since, as the approximation to A is infinitely often correct, we can simply wait for some later stage at which $x \in dom A_{t}$ and $A_{t} ≺ A$ then argue as below.

Since the reductions are total we can find ξ, χ such that $ξ ≺ X_{e}$ is an $A (X_{e})$ supported approximation to $X_{e}$ satisfying $(\forall y ⩽ x) (Φ_{j} (ξ; y) = A (y) = A_{t} (y))$ and χ is an A supported approximation to A satisfying $A ≻ χ ≻ A_{t}$ with $Φ_{j} (χ) ≻ ξ$ . Now let $t^{'} > t$ be large enough that every axiom needed to ensure ξ, χ are $A (X_{e})$ , A supported has been enumerated by stage $t^{'}$ , $Φ_{j, t^{'}} (ξ; x) = A (x) = A_{t} (x)$ , $Φ_{j, t^{'}} (χ) ≻ ξ$ and the domain of ξ is contained in ${⟨ l, x ⟩ | l, x ⩽ t^{'}}$ . Finally, choose $s > t^{'}$ so that $A_{s} ≺ A$ and $dom A_{s} \supseteq dom χ \cup dom A_{t}$ which guarantees $A_{s} ≻ χ$ . But now note that all the conjuncts in Definition 3.6 are satisfied so $Ψ (x, t)$ holds. □

Using this definition we can make precise the idea of an approximation changing its mind.
Definition 3.8.
An increasing sequence of $k + 1$ stages $s_{0}, s_{1}, \dots, s_{k}$ is k-flipflopping (for $Φ_{j}$ , $X_{e}$ ) at x denoted $Ψ_{j, e}^{k} (x, s_{0}, s_{1}, \dots, s_{k})$ just if
$(\forall l ⩽ k - 1) (A_{s_{l}} (x) \neq A_{s_{l + 1}} (x))$

$(\forall l ⩽ k - 1) (Ψ_{j, e} (x, s_{l}))$ is witnessed by some approximation $ξ_{l}$ to $X_{e}$ .

$(\forall l ⩽ k - 2) (A_{s_{l}} ≺ A_{s_{l + 2}})$

An element x is k-flipflopping at stage s (for $X_{e}$ , $Φ_{j}$ ), denoted $Ψ_{j, e}^{k} (x, s)$ just if there is an increasing sequence of stages $s_{0}, s_{1}, \dots, s_{k - 1}, s$ such that $Ψ^{k} (x, s_{0}, s_{1}, \dots, s_{k - 1}, s)$ .

When j, e are clear from context we will omit mentioning them.

We can now provide the framework for diagonalizing against $X_{e}$ .
Lemma 3.9.
If $Ψ_{j, e}^{3} (x, s)$ then $Ψ_{j, e} (x, s)$ fails to hold.
Proof.
Let $s_{3} = s$ and suppose, for a contradiction, that both $Ψ_{j, e}^{3} (x, s_{0}, s_{1}, s_{2}, s_{3})$ and $Ψ_{j, e} (x, s_{3})$ hold and are witnessed by the approximations $ξ_{l}, l < 4$ to $X_{e}$ . By part 3 of Definition 3.8 and Definition 3.6 it follows that $(\forall l ⩽ k - 2) (ξ_{l} ≺ ξ_{l + 2})$ .

As $A_{s_{0}} (x) ↓ \neq A_{s_{1}} (x) ↓$ we have $ξ_{0} |_{2} ξ_{1}$ by Lemma 3.5 we have $ξ_{2} |_{1} ξ_{1}$ and as $A_{s_{1}} (x) ↓ \neq A_{s_{2}} (x) ↓$ we can apply Lemma 3.5 again to infer that $ξ_{3} |_{0} ξ_{2}$ . But s-supported approximations to an $n - REA (Z)$ can’t disagree on column 0. Contradiction. □

With this in mind we can now reiterate the basic strategy we would use to meet $R_{j, e}$ if there were no other requirements. Choose some x and hold it out of $A^{[3]}$ until we observe a computation witnessing $Ψ (x, s)$ , i.e., a computation of an s-supported approximation ξ of $X_{e}$ which computes $x \notin A^{[3]}$ . This stage becomes $s_{0}$ in the lemma above and ξ becomes $ξ_{0}$ . Now enumerate x into $A^{[3]}$ dependent on a very large initial segment of $A^{[2]}$ and wait until we again see $Ψ (x, s)$ with a witness whose domain contains the domain of $ξ_{0}$ . This new stage becomes $s_{1}$ and this new witness becomes $ξ_{1}$ . Enumerate an element into $A^{[2]}$ depending on a large initial segment of $A^{[1]}$ canceling the enumeration of x and now wait until we again see $Ψ (x, s)$ with $A_{s} ≻ A_{s_{0}}$ and a witness whose domain extends that of $ξ_{1}$ . Repeat the cancellation one last time via an enumeration into $A^{[1]}$ for a guaranteed win. At each point at which we wait on a computation we restrain any elements from being enumerated into any initial segment appearing in a computation we’ve used in this process. The lemma above ensures that this process ends in a victory.
3.2. Overview of $P_{i}$

To meet $P_{i}$ we must construct sets $Y_{i}$ and functionals that witness $Y_{i} \oplus A \equiv_{T} A \oplus W_{i}^{A}$ . As we control the construction of the sets $Y_{i}$ we will simply settle on a particular way of coding $W_{i}^{A}$ into $Y_{i}$ so we can share a single functional Θ computing $W_{i}^{A}$ from $Y_{i}$ . As elements can both enter and leave (our approximation to) $W_{i}^{A}$ during the construction our coding mechanism must allow $Y_{i}$ to change it’s mind about the value of $W_{i}^{A} (x)$ .

To this end we use the x-th column of $Y_{i}^{[3]}$ to encode whether or not x is in $W_{i}^{A}$ . To guess that $x \in W_{i}^{A}$ we place $⟨ x, 0 ⟩$ into $Y_{i}^{[3]}$ , to revoke that guess we place $⟨ x, 1 ⟩$ into $Y_{i}^{[3]}$ , to guess x in $W_{i}^{A}$ we place $⟨ x, 2 ⟩$ into $Y_{i}^{[3]}$ and so on. To avoid any need to memorize the particular coding convention we define the following notation.

Definition 3.10.
$\begin{matrix} {[x]}_{i}^{s} = ⟨ x, k ⟩ where k is the least element of ω such that Y_{i, s - 1}^{[3]} (⟨ x, k ⟩) ↓ = 0 \end{matrix}$

When used without stage it indicates the least element of the form $⟨ x, k ⟩$ not yet enumerated into $Y_{i}^{[3]}$ .

On the other hand, as we don’t control the set $W_{i}^{A}$ , the only way we can take full advantage of any change in $W_{i}^{A}$ is to build functionals $Γ_{i}$ so that it always tries to map $A_{s} = A_{s} ↾_{l_{s}}$ to $Y_{i, s} ↾_{s}$ whenever $i < s$ but is reset whenever $P_{i}$ is reinitialized.
Definition 3.11.

$Θ_{s} (Z; x) = \{\begin{matrix} 1 & if max {k | Z (⟨ 3, ⟨ x, k ⟩ ⟩) ↓ = 1 \lor k = - 1} \equiv 0 (mod 2) \\ 0 & otherwise \end{matrix}$

Let $s^{'}$ be the last stage with $s^{'} ⩽ s$ at which $P_{i}$ is reinitialized (injured). Then $Γ_{i, s} (X \oplus Z; y) ↓ = Y_{i, t} (y)$ where t is the least stage satisfying $s ⩾ t ⩾ s^{'}$ , $t > y$ , $Y_{i, t} (y) ↓$ , $X ≻ A_{t}$ and $Z ≻ W_{i, t}^{A_{t}} ↾_{y + 1}$ . If there is no such t then $Γ_{i, s} (X \oplus Z; y) ↑$

Note that Condition 1 ensures that $Γ_{i} (A \oplus W_{i}^{A})$ is total as for every y there is a stage $s > y$ at which $A_{s} ≺ A$ and $W_{i, s + 1}^{A} ↾_{y + 1} = W_{i}^{A} ↾_{y + 1}$ . Also, observe that if $x > s$ then $Γ_{i}$ makes no commitments about x prior to stage s and thus any commitments made about x will be dependent on at least the initial $l_{s}$ elements of each column of A.

We build $Y_{i}$ by enumerating axioms much like we do for A but, remember it is only the columnwise sum $Y_{i} \overline{\oplus} A$ which we build to be $3 - REA$ not $Y_{i}$ itself (this merely saves us the trouble of copying every enumeration into A over to $Y_{i}$ ) Thus, the axioms enumerating elements into $Y_{i}$ can depend not only on prior columns of $Y_{i}$ but on prior columns of A as well. We omit the straightforward modifications to the definition of axiom to allow for this dependence. As with A we will simply indicate which elements we wish to enumerate into $Y_{i}$ and rely on the following properties to uniquely define what axiom is enumerated and how our approximation to $Y_{i}$ is affected.
Property 3.

$Y_{i, s}$ is the unique partial function with $dom Y_{i, s} = {⟨ k, x ⟩ | k < l_{s} + 4 \land x < l_{s}}$ such that $Y_{i, s} \overline{\oplus} A_{s}$ is an s-supported approximation (i.e., $A_{s} (Y_{i} \overline{\oplus} A)$ -supported) (hence, $k > 3$ , $k < l_{s} + 4$ , $x < l_{s} ⟹ Y_{i, s} (⟨ k, x ⟩) ↓ = 0$ ).

If x is enumerated into $Y_{i}^{[k]}$ at stage s then x is enumerated dependent on $A_{s}^{[k^{'}]}$ and $Y_{i, s}^{[k^{'}]}$ for $k^{'} < k$ (hence on prior columns of both A and $Y_{i}$ up to height $l_{s}$ ).

Our construction will ensure that the following condition is satisfied.
Condition 2.
For all s, $Θ_{s} (Y_{i, s}; x) = W_{i, s}^{A_{s}} (x)$ and $Γ_{i, s} (A_{s} \oplus W_{i, s}^{A_{s}}; x) = Y_{i, s} (x)$ whenever both sides are defined. Moreover, $Γ_{i}$ is well-defined.

To this end, unlike the functional $Γ_{i}$ , we don’t reset the set of axioms enumerated into $A (Y_{i})$ when the module implementing $P_{i}$ is reinitialized since $W_{i}^{A}$ isn’t reinitialized.
3.3. Requirement interaction

Note that we can regard $A \oplus W_{i}^{A}$ as (equivalent to) a $4 - REA$ set so the same considerations about an $n + 1 - REA$ set avoiding equivalence with an $n - REA$ from Section 3.1 apply but now it’s our job to ensure equivalence. Obviously, if we could leave $A^{[1]}$ empty (or even computable) then we could trivially meet $P_{i}$ simply by enumerating ${[x]}_{i}^{s}$ into $Y_{i}^{[3]}$ whenever we see z enter $W_{i}^{A}$ (as we could wait until $A^{[1]}$ had settled) and simply copying $A^{[2]}$ , $A^{[3]}$ into $Y_{i}^{[1]}$ and $Y_{i}^{[2]}$ respectively. However, meeting requirements of the form $R_{j, e}$ forces us to make (non-computable) enumerations into all three columns of A.

Specifically, an opponent building $W_{i}^{A}$ could try to duplicate the kind of argument we gave in Section 3.1. If such an opponent could arrange for the approximation to $A \oplus W_{i}^{A}$ to flip-flop on some value z 4 times (waiting for new $Γ_{i}$ , Θ computations each time) then we would have no way to change $Y_{i} \overline{\oplus} A$ to meet $P_{i}$ . This situation is loosely depicted in Fig. 2 where the shaded region is meant to represent the region below $l_{s}$ (and thus use and domain of Θ and $Γ_{i}$ ) while the hatched region in stage $t_{4}$ represents the use of the $Γ_{i}$ computation which disagrees with $Y_{i}$ .

Figure 2.

Piggybacking off $*_{R}$ j,e.

For instance, our opponent might start by reserving some value z to be kept out of $W_{i}^{A}$ . By waiting until we’ve committed to the behavior of our functionals on the appropriate initial segments our opponent could force a change to $Y_{i}$ by enumerating z into $W_{i}^{A}$ with some large use and wait until some stage at which our functionals again witness (enough of) the equivalence $A \oplus W_{i}^{A} \equiv_{T} Y_{i} \overline{\oplus} A$ . The proof of Theorem 1.3 from [2] shows that our opponent can ensure that sometimes we’re forced to enumerate some y into $Y_{i}^{[2]}$ (to cancel a previous enumeration into $Y_{i}^{[3]}$ ) in response to some requirement $R_{j, e}$ enumerating c into $A^{[3]}$ . That is, we can’t avoid getting to stage $t_{2}$ as depicted in Fig. 2.

3.4. Safety via agreement

If $P_{i}$ is of higher priority than $R_{j, e}$ we need to be able to meet $R_{j, e}$ in a way that doesn’t allow an opponent to force an injury to $P_{i}$ . Our strategy will be to modify the way (the module responsible for meeting) $R_{j, e}$ operates to ensure that when $R_{j, e}$ enumerates b into $A^{[2]}$ we aren’t forced to enumerate any element into $Y_{i}^{[1]}$ , i.e., we avoid ever reaching the stage labeled $t_{3}$ in Fig. 2. If we can arrange this, it removes our opponents 1 column advantage on us which will prevent $R_{j, e}$ from injuring $P_{i}$ (the final enumeration of a into $A^{[1]}$ will thus keep $A \overline{\oplus} Y_{i}$ and $A \oplus W_{i}^{A}$ in lock step).

The key idea here is that b’s entry into $A^{[2]}$ can only force us to enumerate an element into $Y_{i}^{[1]}$ if there is some (small) value y with $y \notin Y_{i, t_{1} - 1}$ but $y \in Y_{i, t_{3} - 1}$ . In other words we will wait to enumerate b until the second (and first) column of $Y_{i}$ are the same as they were immediately before c was enumerated.

As the enumeration of c into $A^{[3]}$ at stage $s_{0}$ will generally force a change in $Y_{i}^{[2]}$ and since we can’t control $W_{i}^{A}$ we can’t ensure this condition is met for any particular value c. Instead, we make multiple attempts to meet $R_{j, e}$ with the first attempt enumerating $c_{0}$ into $A^{[3]}$ , the second attempt $c_{1}$ and so on and argue that for some $c = c_{k}$ we either meet $R_{j, e}$ without canceling c or that we eventually see the agreement needed to allow safe enumeration of b into $A^{[2]}$ .

Specifically, at stage $s_{- 1}$ we initialize (the module for) $R_{j, e}$ choosing $c_{0}$ large and setting $c_{k} = c_{0} + k$ (in the full construction $A^{[3]}$ will be partitioned between the various requirements to avoid collision). At stages $t_{k} = s_{k} - 1$ we observe an active stage for $R_{j, e}$ and, if we haven’t yet found agreement (i.e. some $c_{n}$ which we can now cancel without changing the first two columns of any set $Y_{i}$ ), we respond at stage $s_{k}$ by enumerating (only) $c_{k}$ into $A^{[3]}$ .

There are two critical aspects of this strategy. First, we ensure that $c_{k + 1}$ is small relative to the stage at which $c_{k}$ is first enumerated so that each time we enumerate some $c_{k}$ we are extending the use of $Γ_{i}$ . Hence, commitments made about $Γ_{i}$ after stage $s_{- 1}$ are canceled when we enumerate any $c_{k}$ into $A^{[3]}$ . Second, the fact that we choose $c_{0}$ large means that if $z \in W_{i, s_{- 1}}^{A}$ then no enumeration of $c_{k}$ will cancel z (and thus no reason to change how $Y_{i}$ codes z’s membership in $W_{i}^{A}$ ). Note that it will also be the case that each time we enumerate some $c_{k}$ we will remove6

⁶
Remember, that we’ve used the fact that we will ensure $A_{s} ≺ A$ infinitely often to allow us to set the ‘use’ of a computation placing $z \in W_{i}^{A}$ at stage s to $l_{s}$ .

any z enumerated into

W_{i}^{A}

since stage

s_{- 1}

. Thus, the only real constraint prior commitments impose on us while trying to produce the desired agreement is that we must remove

{[z]}_{i}^{s_{- 1}}

from

Y_{i}^{[3]}

if present whenever we enumerate any

c_{k}

into

A^{[3]}

The main difficulty in the construction will be to argue that we can always arrange our enumerations into $Y_{i}$ during the intervals $(s_{k - 1}, s_{k})$ so that we eventually find some $c_{n}$ we can cancel without changing the first two columns of any $Y_{i}$ . Stated in terms of the following definition we need to show that we can find $k^{'}$ , k such that $s_{k^{'}} - 1 \approx s_{k} - 1$ . That is, there are active stages for $R_{j, e}$ (or there are only finitely many such stages) $s_{k^{'}} - 1 < s_{k} - 1$ such that canceling $c_{k^{'}}$ by enumerating $b_{k^{'}}$ at stage7

⁷

Note that in full construction we assume that no elements enter any $W_{i}^{A}$ at stages $s_{k}$ so we need not worry about changes between $s_{k} - 1$ and $s_{k}$ .

s_{k}

(which requires us to return all

Y_{i}

to a state compatible with that at

s_{k^{'}} - 1

) won’t require changes in the first two columns of

Y_{i}

(the third column is returned to it’s earlier state for free by the enumeration of

b_{k^{'}}

Definition 3.12.

We define $\begin{array}{l} s \approx^{i} t & \overset{def}{⟺} Y_{i, s}^{[⩽ 2]} ↾_{l_{s}} / | Y_{i, t}^{[⩽ 2]} ↾_{l_{t}} \\ s \approx t & \overset{def}{⟺} (\forall i) (s \approx^{i} t) \end{array}$ We say that s, tagree just when $s \approx t$ .

For future use we also adopt the following terminology (reflecting the fact that if t is accessible at stage s then there is some possible enumeration of elements into the sets $Y_{i}$ that would allow some later stage $s^{'} > s$ to satisfy $t \approx s^{'}$ ).

Definition 3.13.

A stage t is accessible at a stage $s ⩾ t$ just if for all i $\begin{matrix} Y_{i, s}^{[⩽ 1]} ↾_{l_{s}} ≻ Y_{i, t}^{[⩽ 1]} ↾_{l_{t}} \end{matrix}$

A stage is (i-canceled) canceled just if it isn’t (i-accessible) accessible.

We also adopt the definition below. Note that active stages are the stages at which $R_{j, e}$ takes action in response to seeing a longer $Φ_{j}$ back and forth computation on it’s own accord rather than merely responding to some enumeration into $W_{i}^{A}$ . Definition 3.14.

A stage $s_{m}$ at which $R_{j, e}$ enumerates an element into $A^{[3]}$ or $A^{[2]}$ is a ( $R_{j, e}$ ) active stage. A stage $t_{k}$ is called a ( $R_{j, e}$ ) preactive stage just if $t_{k} + 1$ is an active stage.

3.5. Simplified agreement

Let’s consider how (the module for) $R_{j, e}$ might enact this strategy with respect to a single requirement $P_{i}$ assuming only a single value z enters or leaves $W_{i}^{A}$ . On this assumption, we’ll describe a winning strategy for $R_{j, e}$ that enumerates at most two elements $c_{0}$ , $c_{1}$ into $A^{[3]}$ . This strategy is visualized in Figs 3 and 4. Note that, while the figures depict $c_{0}$ and ${[z]}_{i}^{s_{- 1}}$ as being on the same level but in reality ${[z]}_{i}^{s_{- 1}}$ is smaller than $c_{0}$ which is why we shade a larger region of $Y_{i}$ (where the shaded region indicates the region below $l_{s}$ at the given stage).

Figure 3.

Satisfying $R_{j, e}$ respecting $P_{i}$ on z.

If z doesn’t enter $W_{i}^{A}$ in the interval $[s_{- 1}, s_{0})$ when we enumerate $c_{0}$ we get $s_{0} - 1 \approx^{i} s_{1} - 1$ for free since there was never any need to cancel any element in $Y_{i}^{[3]}$ (this case isn’t depicted).

Figure 4.

Alternate behavior after stage $s_{0}$ .

In Fig. 3 we see that z enters $W_{i}^{A}$ by stage $s_{0} - 1$ forcing us to cancel ${[z]}_{i}^{s_{- 1}}$ at stage $s_{0}$ . Note that when z first enters $W_{i}^{A}$ we become free to code that entry into $Y_{i}$ since the enumeration changes $W_{i}^{A}$ on the use of $Γ_{i} (A \oplus W_{i}^{A}; {[z]}_{i}^{s_{- 1}})$ . However, in the figure z isn’t enumerated into $W_{i}^{A}$ during $[s_{0}, s_{1})$ . We’ve circled the value which blocks agreement at stage $s_{1} - 1$ with the earlier stage $s_{0} - 1$ . But now observe that at stage $s_{2} - 1$ agreement is achieved for free since we had no need to cancel any elements at stage $s_{1}$ (with $c_{1}$ playing the role of c). As we will see later, even if we’d had other intervening stages as long as they didn’t enumerate any elements into $Y_{i}^{[1]}$ small at stage $s_{1} - 1$ we could cancel their contributions. Note that when we enumerate $b_{1}$ into $A^{[2]}$ it automatically removes ${[z]}_{i}^{s_{- 1}}$ from $Y_{i}^{[3]}$ as this was enumerated during the interval $(s_{1}, s_{2})$ (remember $A \overline{\oplus} Y_{i}$ is $3 - REA$ not $Y_{i}$ ).

In Fig. 4 we depict the case where z is enumerated into $W_{i}^{A}$ at some stage $s_{0}^{'} \in (s_{0}, s_{1})$ . At stage $s_{0}^{'}$ (we can’t wait until $s_{1} - 1$ ) we are faced with a choice. We could simply enumerate ${[z]}_{i}^{s_{- 1}}$ into $Y_{i}^{[3]}$ again but then the value we enumerated into $Y_{i}^{[2]}$ at stage $s_{0}$ would prevent us from achieving agreement between stages $s_{0} - 1$ and $s_{1} - 1$ . So instead we choose to cancel the value enumerated into $Y_{i}^{[2]}$ and restore the state of $Y_{i}$ at stage $s_{0} - 1$ producing agreement.

So far our examples have always shown z entering $W_{i}^{A}$ before the enumeration of $c_{0}$ as this is the most challenging case to achieve agreement. However, it’s useful to consider the case to illustrate two important points. First, to demonstrate why it’s only agreement in the first two columns of $Y_{i}$ which matters not agreement about $z \in W_{i}^{A}$ and why later enumeration into $W_{i}^{A}$ doesn’t threaten agreement once it’s been achieved. This situation is depicted in Fig. 5.

Figure 5.

Satisfying $R_{j, e}$ , $P_{i}$ when $b_{0}$ removes z from $W_{i}^{A}$ .

In this scenario z doesn’t enter $W_{i}^{A}$ before, at $s_{0}$ , we enumerate $c_{0}$ into $A^{[3]}$ . As such, we don’t enumerate ${[z]}_{i}^{s_{- 1}} = {[z]}_{i}^{s_{0}}$ before $s_{0}$ either so it need not be canceled at stage $s_{0}$ . Hence, at stage $s_{0}$ we already have agreement with stage $s_{0} - 1$ , i.e., $s_{0} \approx^{i} s_{0} - 1$ . However, we may have to wait to see a $R_{j, e}$ expansionary stage and during that time we may see z enter $W_{i}^{A}$ . But, note that, once we’ve achieved agreement we can always respond to such an entry by enumerating ${[z]}_{i}$ (labeled above as ${[z]}_{i}^{s_{- 1}}$ ) into $Y_{i}^{[3]}$ without jeopardizing that agreement. Thus, at stage $s_{1} - 1$ when we finally see a $R_{j, e}$ expansionary stage we have $s_{1} - 1 \approx^{i} s_{0} - 1$ .

Now, remember, that it’s not actually $Y_{i}$ that we’ve committed to building as a $3 - REA$ set but $A \overline{\oplus} Y_{i}$ (the columwise sum). Hence, the enumeration of $b_{0}$ into $A^{[2]}$ doesn’t just cancel $c_{0}$ but also ${[z]}_{i}^{s_{- 1}}$ (in Fig. 4 we glossed over need to reenumerate this element when $b_{0}$ was enumerated). Thus, at $s_{1}$ we comply with the commitments made for $P_{i}$ at $s_{0} - 1$ . Of course, z could still decide to finally enter $W_{i}^{A}$ at this point but, since z wasn’t in $W_{i}^{A}$ at stage $s_{0} - 1$ , we are no longer committed to keeping ${[z]}_{i}^{s_{- 1}}$ out of $Y_{i}^{[3]}$ allowing us to preserve the computation required by $P_{i}$ . Finally, if we enumerate a, we again rely on the fact that it’s $A \overline{\oplus} Y_{i}$ that’s $3 - REA$ to allow a to cancel both ${[z]}_{i}^{s_{- 1}}$ and $b_{0}$ returning both sides to stages compatible with those they had at stage $s_{1} - 1$ . Note that if, instead, z had been out of $W_{i}^{A}$ at stage $s_{1} - 1$ and then entered $W_{i}^{A}$ after the enumeration of a we could respond by enumerating ${[z]}_{i}^{s_{- 1}}$ just as we did when z entered $W_{i}^{A}$ after the enumeration of $b_{0}$ but before a.

3.6. General agreement

In Section 3.5 we demonstrated how to meet $R_{j, e}$ without injuring a single requirement $P_{i}$ on the assumption that only a single value z ever enters or leaves $W_{i}^{A}$ . However, in the general case we must meet $R_{j, e}$ without injuring any of the finitely many higher priority requirements $P_{i_{0}}$ , $P_{i_{1}}$ , $P_{i_{2}}$ , …. We must also accommodate arbitrarily many elements entering and leaving the sets $W_{i_{n}}^{A}$ .

3.6.1. Multiple elements entering some $W_{i_{0}}^{A}$

First we explain the relatively easy task of dealing with multiple elements entering and leaving the sets $W_{i_{n}}^{A}$ . By the discussion in Section 3.4 the enumeration of $c_{k}$ cancels any commitments we’ve made about $Γ_{i}$ after stage $s_{- 1}$ . Hence, if $z ⩾ s_{- 1}$ then Definition 3.11 means that at $s_{- 1}$ we’ve yet to make any commitment about z (i.e. about the value of $Γ_{i}$ on ${[z]}_{i}^{t}$ ). This leaves us with finitely many values we must be concerned with entering or leaving any $W_{i}^{A}$ when trying to achieve agreement. Note that if we ever see $z < z^{'}$ enter $W_{i}^{A}$ after stage $s_{- 1}$ this cancels any commitments we’ve made regarding $z^{'}$ allowing us to freely code changes in $W_{i}^{A} (z^{'})$ by enumerating elements into $Y_{i}^{[3]}$ . Morally speaking, this means it’s only the least value of z entering $W_{i}^{A}$ in the interval $[s_{k}, s_{k + 1} - 1]$ which matters so we need only tweak the strategy above to deal with multiple values entering/leaving some $W_{i}^{A}$ .

More specifically, we eventually find $k^{'} < k$ such that the least $z \notin W_{i, s_{- 1}}^{A}$ which is in some $W_{i, s_{k^{″}} - 1}^{A}, k^{'} ⩽ k^{″} < k$ also is in $W_{i, s_{k} - 1}^{A}$ or eventually all $z \notin W_{i, s_{- 1}}^{A}$ aren’t in $W_{i, s_{k} - 1}^{A}$ . In the later case we have $s_{k} - 1 \approx^{i} s_{k + 1} - 1$ as we are in the same situation depicted in Fig. 3. In the former case, as in Fig. 4, we ensure $s_{k^{'}} - 1 \approx^{i} s_{k} - 1$ by making enumerations into $Y_{i}^{[1]}$ when we see a new least $z \notin W_{i, s_{- 1}}^{A}$ enter $W_{i}^{A}$ that cancels all changes since the last stage $s_{k^{″}} - 1$ with $z \in W_{i, s_{k^{″}} - 1}^{A}$ and making whatever corrections needed to code the state of $z^{'} > z$ by enumeration into $Y_{i}^{[3]}$ . Note that no problem is introduced if, in response to the entry of $z^{'}$ into $W_{i}^{A}$ at stage $s \in (s_{k - 1}, s_{k})$ we make an enumeration into $Y_{i}^{[1]}$ to cancel all changes between $s_{k^{'}} - 1$ and s. Such enumerations may prevent ever achieving agreement with some $s_{k^{″}} - 1, k^{'} < k^{″} < k$ (as we can never remove an element from $Y_{i}^{[1]}$ ) but that’s not a problem since the canceled stages are ones in which no $z^{″} < z$ enters $W_{i}^{A}$ .

3.6.2. Multiple $P_{i}$ requirements

This leaves us with the harder problem of dealing with multiple requirements $P_{0}$ , $P_{1}$ , …, $P_{⟨ j, e ⟩}$ at the same time.

Unlike the case with multiple values entering a single set, $W_{i}^{A}$ here entry into $W_{i}^{A}$ doesn’t cancel any commitments made about $Γ_{i^{'}}$ , $i^{'} \neq i$ . Thus, when we see z enter $W_{i}^{A}$ we must immediately decide how to code this change in $Y_{i}$ (by enumerating into $Y_{i}^{[3]}$ or cancelling a removal from it by enumerating into $Y_{i}^{[1]}$ ) without yet knowing what elements may later enter some $W_{i^{'}}^{A}$ . We now describe how we handle this problem under the simplifying assumption that there is only a single value z which may enter any set $W_{i}^{A}$ and $z \notin W_{i, s_{- 1}}^{A}$ 8

⁸
If $z \in W_{i, s_{- 1}}^{A}$ then z won’t leave $W_{i}^{A}$ as a result of any enumeration we make in trying to meet $R_{j, e}$ ensuring that coding the status of z isn’t in tension with our attempt to meet $R_{j, e}$ .

where

i ⩽ ⟨ j, e ⟩

. As there is only a single value of z in play we will only ever need to make use of a single location

{[z]}_{i}

to code whether or not

z \in W_{i}^{A}

(i.e. if we see z leave

W_{i}^{A}

we always remove

{[z]}_{i}

from

Y_{i}^{[3]}

) and WLOG we can assume that value is independent of i and just write

[z]

We formulate the problem slightly more generally as trying to meet $R_{j, e}$ while respecting the $n + 1$ requirements $P_{i_{0}}$ , $P_{i_{1}}$ , …, $P_{i_{n}}$ (i.e., assuming that agreement is automatic for i not in ${i_{0}, \dots i_{n}}$ ) and then argue that we can reduce this to the problem of respecting n requirements. Since we’ve assumed that $z \notin W_{i_{j, s_{- 1}}}^{A}, j ⩽ n$ at each stage $s_{k}$ where we enumerate $c_{k}$ into $A^{[3]}$ this has the effect of removing z from $W_{i_{j, s_{k}}}^{A}, j ⩽ n$ . To ensure that the sets $Y_{i_{j}}$ reflect this we enumerate $l_{t}$ into $Y_{i_{j}}^{[2]}$ if $z \in W_{i_{j, s_{k} - 1}}^{A_{s_{k} - 1}}$ where t is the stage at which $[z]$ entered $Y_{i_{j}}^{[1]}$ in the interval $(s_{k - 1}, s_{k})$ . Thus, at each stage $s_{k}$ z isn’t in any of the sets $W_{i_{j}}^{A}$ nor are the elements $[z]$ . Note that, in the case where $z \notin W_{i_{j, s_{k} - 1}}^{A_{s_{k} - 1}}$ for all $j ⩽ n$ we don’t enumerate any elements into $Y_{i_{j}}$ at stage $s_{k}$ meaning that we automatically have $s_{k} - 1 \approx s_{k}$ and, by the remarks at the end of Section 3.5, once established we can maintain this agreement until stage $s_{k + 1} - 1$ as we only need to enumerate elements into the third column of the sets $Y_{i_{j}}$ to respect the requirements $P_{i_{0}}$ , $P_{i_{1}}$ , …, $P_{i_{n}}$ .

What we must do is describe a strategy for reacting to the enumeration of z into $W_{i_{j}}^{A}$ during the interval $(s_{k}, s_{k + 1})$ (the interval between $c_{k}$ and $c_{k + 1}$ entering $A^{[3]}$ ) that ensures we will eventually produce agreement. The key factor that determines how we act to try and produce agreement during the interval $(s_{k}, s_{k + 1})$ is which of the sets $W_{i_{0}}^{A}, W_{i_{1}}^{A}, \dots, W_{i_{n}}^{A}$ we see z enter first. To this end, define $u_{m}^{j}$ so that $(s_{u_{m}^{j}}, s_{u_{m}^{j} + 1}$ is the m-th interval on which z first enters $W_{i_{j}}^{A}$ .

Our argument is essentially a priority argument in which we give highest priority to producing agreement between intervals $(s_{k}, s_{k + 1})$ in which the first set z enters is $W_{i_{0}}^{A}$ . We give second highest priority to producing agreement between intervals in which z first enters $W_{i_{1}}^{A}$ and so on. Specifically, during the interval $(s_{u_{m}^{0}}, s_{u_{m}^{0} + 1})$ we will attempt to produce agreement with the stages $s_{u_{0}^{0} + 1} - 1, s_{u_{1}^{0} + 1} - 1, \dots, s_{u_{m - 1}^{0} + 1} - 1$ ignoring any intervening intervals in which z first entered some other $r.e.$ set in our list. However, as when we service a higher priority requirement in a finite injury argument, when we first see z enter $W_{i_{0}}^{A}$ we abandon our attempts to produce agreement on intervals where z first enters some other $r.e.$ set. Thus, during the interval $(s_{u_{m}^{1}}, s_{u_{m}^{1} + 1})$ we will only attempt to produce agreement with the stages $s_{u_{m^{'}}^{1} + 1} - 1, s_{u_{m^{'} + 1}^{1} + 1} - 1, \dots, s_{u_{m - 1}^{1} + 1} - 1$ where $m^{'}$ is the least value such that there is no k with $s_{u_{m^{'}}^{1} + 1} - 1 < s_{u_{k}^{0}} < s_{u_{m - 1}^{1} + 1} - 1$ . Similarly, in the interval $(s_{u_{m}^{2}}, s_{u_{m}^{2} + 1}$ we only try to produce agreement with the stages $s_{u_{m^{″}}^{2} + 1} - 1$ which have occurred since the last interval in which z first entered $W_{i_{0}}^{A}$ or $W_{i_{1}}^{A}$ and so on. Of course, if we already have agreement with some earlier stage $s_{k} - 1$ (e.g. because z didn’t enter any of our $r.e.$ sets in the previous interval) we simply maintain it regardless of which set is entered first.

Thus, if s is the first stage in $(s_{k}, s_{k + 1})$ at which we see z enter some $W_{i_{j}}^{A}$ with there is a (potentially empty) list of earlier stages9

⁹

For instance, if z first enters $W_{i_{0}}^{A}$ and $(s_{k}, s_{k + 1}) = (s_{u_{m}^{0}}, s_{u_{m}^{0} + 1})$ then $k_{q}^{s} = u_{q}^{0}$ , $q < m$ and if z first enters $W_{i_{1}}^{A}$ and $(s_{k}, s_{k + 1}) = (s_{u_{m}^{1}}, s_{u_{m}^{1} + 1})$ then $k_{q}^{s} = u_{m^{'} + q}^{1}$ , $m^{'} + q < m$ .

s_{k_{0}^{s} + 1} - 1, \dots s_{k_{r}^{s} + 1} - 1

which we will try to produce agreement with. If this list is non-empty then we immediately10

¹⁰

Stage $s + 1$ since we interleave stages at which enumeration into A and sets $r.e.$ in A are seen.

and enumerate

l_{t}, t = s_{k_{r}^{s} + 1}

into

Y_{i_{j}}^{[1]}

to cancel all elements enumerated into

Y_{i_{j}}

at intervening stages. This enumeration also cancels the element enumerated into

Y_{i_{j}}^{[2]}

at stage t and thus returns

[z]

into

Y_{i_{j}}^{[3]}

This has the effect of ensuring that $s_{k_{0}^{s} + 1} - 1 \approx^{i_{j}} s_{k_{1}^{s} + 1} - 1 \approx^{i_{j}} \dots \approx^{i_{j}} s_{k_{r}^{s} + 1} - 1 \approx^{i_{j}} s$ . Note that if we are only trying to respect a single requirement $P_{i_{0}}$ this strategy ensures we always achieve agreement. Either z doesn’t enter $W_{i_{0}}^{A}$ during the interval $(s_{- 1}, s_{0})$ in which case we achieve the free win mentioned above or during the interval $(s_{0}, s_{1})$ then the list of prior stages we are attempting to agree with is non-empty ensuring that $s_{0} - 1 \approx s_{1} - 1$ .

Now we notice that the argument we just gave depends only on having a sequence of intervals $(t_{q}^{'}, t_{q})$ with $t_{q - 1} ⩽ t_{q}^{'} ⩽ t_{q}$ such that at every stage $t_{q}$ we have $z \notin W_{i_{j}}^{A}, j ⩽ n$ , $[z] \notin Y_{i_{j}}^{[3]}$ , all elements enumerated into $Y_{i_{j}}$ between $t_{q}$ and $t_{q + 1}^{'}$ are larger $l_{t_{q}}$ and that, if z enters $W_{i_{j}}^{A}$ in $(t_{q}^{'}, t_{q})$ for some $j ⩽ n$ then enumerating $l_{t_{q}}$ into $Y_{i_{j}}^{[1]}$ restores $Y_{i_{j}} ↾_{[l_{t_{q} - 1}]}$ to the state it had at stage $t_{q} - 1$ . Finally, we observe that if $(t_{q}^{'}, t_{q}), q ⩽ m$ is such that $t_{q} = u_{q + m^{'}}^{j}$ , $q + m^{'} ⩽ m$ where, as above, z doesn’t first enter any $W_{i_{e}}^{A}, e < j$ during any interval between $u_{m^{'}}^{j}$ and $u_{m}^{j}$ and $t_{q}^{'}$ is the stage at which z enters $W_{i_{j}}^{A}$ in the interval ending at stage $t_{q}$ satisfies these properties. That is, $t_{q} - 1, q < m - m^{'}$ is the sequence of stages that we try to achieve agreement with when we see z first enter $W_{i_{j}}^{A}$ during the interval ending with $t_{m - m^{'}}$ . Thus, when see z first enter $W_{i_{j}}^{A}$ in an interval we can then run the same strategy on the indexes in ${i_{0}, \dots, i_{n}} - {i_{j}}$ on these reduced intervals.

Figure 6.

Agreement respecting $P_{i_{0}}$ and $P_{i_{1}}$ .

Figure 7.

Alternative agreements respecting $P_{i_{0}}$ and $P_{i_{1}}$ .

The notation gets a bit heavy in that last discussion so to make this concrete consider Fig. 6 where we give an example of trying to produce agreement while respecting the two requirements $P_{i_{0}}$ and $P_{i_{1}}$ . In the figure we’ve only shown the final stage of intervals and we’ve boxed (including the double box) the stages which correspond to intervals in which z first enters $W_{i_{0}}^{A}$ . Note that, on the intervals ending at stage $s_{1}$ , $s_{2}$ where z first enters $W_{i_{1}}^{A}$ we have $s_{1} - 1 \approx^{i_{1}} s_{2} - 1$ and the behavior of $Y_{i_{0}}$ looks just like the strategy we would follow if we were dealing with only the requirement $P_{i_{0}}$ . However, when we hit the interval ending at $s_{3}$ in which z first enters $W_{i_{0}}^{A}$ this attempt is injured so in the interval ending $s_{4}$ , $Y_{i_{1}}$ starts afresh and doesn’t try to create agreement with stage $s_{2} - 1$ .

Furthermore, note that at the boxed stages (the last stages of intervals at which z first enters $W_{i_{0}}^{A}$ ) agreement works as if the unboxed stages don’t exist. Thus, since we have $s_{0} - 1 \approx^{i_{0}} s_{3} - 1 \approx^{i_{0}} s_{5} - 1$ just as in the case where we dealt with only a single requirement $P_{i_{1}}$ we eventually achieve agreement on that index as well ensuring $s_{3} - 1 \approx s_{5} - 1$ . Note that in Fig. 7 we give two alternate ways that the interval ending at stage $s_{3}$ could have played out. On the left we see that if we had a long enough consecutive sequence of intervals in which z first entered $Y_{i_{1}}$ that too would have produced agreement while, on the right, we see how we would have achieved agreement between the double boxed stages had z entered $Y_{i_{1}}$ during the interval $(s_{2}, s_{3})$ after z entered $Y_{i_{0}}$ .

Finally, one might wonder how, even though a smaller value of z entering $W_{i_{j}}^{A}$ subsumes larger values entering the same set how we can handle the case where we first see the larger values enter $W_{i_{j}}^{A}$ when we don’t yet know if the smaller value will later enter. We can handle this the same way we do with multiple sets where seeing 0 enter $W_{i_{0}}^{A}$ first can injure seeing 1 first enter $W_{i_{0}}^{A}$ and so forth. Though, by the discussion above, we need not worry about the case where the larger number enters during an interval after the smaller number.

Now that we’ve outlined the general approach we give the full construction. The complexity involved in this construction largely reflects the difficulty involved in doing accurate bookkeeping for the approach described in this section in the case where we must deal both with achieving agreement with respect to multiple values of i and multiple elements entering and leaving the associated $r.e.$ sets.

4. Full construction

4.1. General framework

The construction takes the form of a finite injury argument with the module $P_{i}$ tasked with meeting $P_{i}$ having priority $2 i$ and the module $R_{j, e}$ tasked with meeting $R_{j, e}$ having priority $2 ⟨ j, e ⟩ + 1$ . Modules of the form $P_{i}$ merely define $Γ_{i}$ as specified in Definition 3.11 and thus have no direct effect on any set or module. In contrast, any time the module $R_{j, e}$ acts all lower priority modules are reinitialized.

At any even stage s at most one requirement of the form $R_{j, e}$ with priority at most $2 s - 1$ acts while (at most one per stage) enumerations into $W_{i}^{A}$ occur only at odd stages. In response to an enumeration into $W_{i}^{A}$ we give each requirement (in decreasing order of priority) the chance to act and claim the enumeration (injuring lower priority requirements) and enumerate elements into $Y_{i}$ in response. We apply the following rule for unclaimed enumerations.

Rule 4.1.
If an axiom enumerates z into $W_{i}^{A}$ at stage s but z goes unclaimed then we enumerate ${[z]}_{i}^{s}$ into $Y_{i}^{[3]}$ .
4.2. Module $R_{j, e}$

We break up the description of the module $R_{j, e}$ into two parts. First, we describe the behavior of the module $R_{j, e}$ at even stages when it may act of it’s own volition to modify A and possibly the sets $Y_{i}$ . Then, later, we describe action of the module $R_{j, e}$ at odd stages in response to an enumeration into a set $W_{i}^{A}$ .

4.2.1. Even stages

The module $R_{j, e}$ tasked with meeting $R_{j, e}$ has four 4 states, $↑, 0, 1, 2, 3$ where ↑ indicates $R_{j, e}$ has yet to execute after (re)initialization and the later numbers (roughly) indicate the number of times we’ve changed our mind about whether $c \in A^{[3]}$ . We denote the state of the module $R_{j, e}$ at the end of stage s by $S_{s} (R_{j, e})$ and assume that the state remains the same at stage $s + 1$ unless otherwise noted. Note that, in state 1 we’ve enumerated at least one potential value for $c_{k}$ for c into $A^{[3]}$ but we may not yet have enumerated the ultimate value c takes into $A^{[3]}$ . If $R_{j, e}$ is injured at stage s we set $S_{s} (R_{j, e}) = ↑$ .

We describe the behavior $R_{j, e}$ at stage s where we may assume that the following all hold.

s is even, $⟨ j, e ⟩ < s$ and no higher priority requirement has chosen to act (injuring $R_{j, e}$ ) at stage s, i.e., we execute this module at stage s.

$s_{- 1} ⩽ s$ is the first even stage after the most recent reinitialization of $R_{j, e}$ .

The element $c_{k}, k > 0$ is defined to be $⟨ ⟨ j, e ⟩, v + k ⟩$ if $c_{0} = ⟨ ⟨ j, e ⟩, v ⟩$ .

$c_{k}$ is enumerated into $A^{[3]}$ at stage $s_{k} = t_{k} + 1 > s_{- 1}$ and m is the smallest value for which $s_{m}$ is undefined and less than s (thus $c_{m}$ is the next element waiting to be enumerated into $A^{[3]}$ ).

$b_{k}, k < m$ are values chosen large at stage $s_{k}$ satisfying $b_{k} \notin A_{s_{k}}^{[n]}$ and $b_{k} \notin Y_{i}^{[n]}$ for any i and $n ⩽ 2$ . Note that this implies $l_{s_{k} - 1} < b_{k} < l_{s_{k}}$ .

Procedure 1 (Even Stages of $R_{j, e}$ ).

Case $S_{s - 1} (R_{j, e}) = ↑$ :

We act by choosing $c_{0} = ⟨ ⟨ j, e ⟩, v ⟩$ where v is chosen large and setting $S_{s} (R_{j, e}) = 0$ .

Case

S_{s - 1} (R_{j, e}) = 0

If $Ψ (c_{0}, s - 1)$ holds then we act by enumerating $c_{0}$ into $A^{[3]}$ , executing Procedure 2 and setting $S_{s} (R_{j, e}) = 1$

Case

S_{s - 1} (R_{j, e}) = 1

We execute the following steps.

If $Ψ (c_{m}, s - 1)$ fails to hold end the stage without acting. Otherwise the module acts by executing the subsequent steps.

If there is $k < m$ with $s_{k} - 1 \approx s - 1$ perform the following steps and end the stage.

Choose $a \notin A^{[1]}$ large.

Set $c = c_{k}$ , $b = b_{k}$ , ${\hat{s}}_{0} = s_{k} - 1$ , ${\hat{s}}_{1} = s - 1$ .

Enumerate b into $A^{[2]}$ and set $S_{s} (R_{j, e}) = 2$

If there is no such k we instead enumerate $c_{m}$ into $A^{[3]}$ and execute Procedure 2

Case

S_{s - 1} (R_{j, e}) = 2

If $Ψ (c, s - 1)$ the module acts by enumerating a into $A^{[1]}$ and setting $S_{s - 1} (R_{j, e}) = 3$ , ${\hat{s}}_{2} = s - 1$ .

Case

S_{s - 1} (R_{j, e}) = 3

Once in state 3 the module never acts again.

We now specify the procedure we referenced above when we enumerated $c_{k}$ . As we want to maintain Condition 2 (correctness of our functionals) at all active stages we must return $Y_{i}$ , by potentially enumerating an element into $Y_{i}^{[2]}$ , to a state compatible with $Y_{i, s_{- 1}}$ . However, what, if any, element must be enumerated into $Y_{i}^{[2]}$ at $s_{k}$ is determined by how we choose to respond to enumerations into $W_{i}^{A}$ so we hand that task of keeping track of that value to the machinery which responds to those enumerations. Specifically, for each $i \in ω$ we define (relative to $R_{j, e}$ ) a marker $b_{i} \in ω \cup {↑}$ with initial value $b_{i, s_{- 1} - 1} = ↑$ . At active stages we’ll just trust that we’ve placed this marker on the right value and do the following.

Procedure 2 (Resetting $Y_{i}$ ).

Execute the following steps when called:

For every $i < ⟨ j, e ⟩ + 1$ enumerate $b_{i}$ into $Y_{i}^{[2]}$ if $b_{i} ↓$ and update $b_{i}$ to ↑.

If $i > ⟨ j, e ⟩$ or $x ⩾ s_{- 1}$ then at the end of the stage enumerate ${[x]}_{i}^{s}$ into $Y_{i}^{[3]}$ if we would otherwise have $Θ (Y_{i, s}; x) ↓ \neq W_{i, s}^{A_{s}} (x) ↓$ .

Note that unless $i, x < s$ no elements have ever been enumerated into $W_{i}^{A}$ so we need take no action to maintain agreement between $W_{i, s}^{A_{s}}$ and $Θ (Y_{i, s})$ .

4.2.2. Odd stages

It’s now our task to ensure that there are two preactive stages t, $t^{'}$ that agree in the sense $t \approx t^{'}$ . Since we may injure lower priority modules we have no obligation to undo enumerations into $Y_{i}, i ⩾ ⟨ j, e ⟩ + 1$ at active stages as we do with $Y_{i}, i < ⟨ j, e ⟩ + 1$ . Thus, we can simply leave enumerations into $Y_{i}, i ⩾ ⟨ j, e ⟩ + 1$ to lower priority modules (or leave them unclaimed) without concern they will block us from achieving the desired agreement. On the other hand, if $z > s_{- 1}$ then the use of $Γ_{i}$ for any element coding the status of z is large enough that we can redefine it every time some $c_{m}$ is enumerated into $A^{[3]}$ by $R_{j, e}$ . Finally, once $R_{j, e}$ enters state 2 we are too far along in the process for changes in $Y_{i}^{[3]}$ to migrate all the way to the first column in time to cause a problem. We only claim those finitely many enumerations which don’t fall into these easy cases.

Rule 4.2.
If $z ↘_{s} W_{i}^{A_{s}}$ , $i < ⟨ j, e ⟩ + 1$ then $R_{j, e}$ claims z just if $S_{s - 1} (R_{j, e}) \in {0, 1}$ and $z < s_{- 1}$ .

Our active management in these cases is complicated by the fact that we may only modify the elements in $Y_{i}$ coding the status of $z < s_{- 1}$ immediately in response to the enumeration of z. Our basic approach to deal with this problem is to use the order in which elements are enumerated into the sets $W_{i}^{A}$ during an interval $[s_{k}, s_{k + 1} - 1]$ to determine our response. However, our approach is only easily described in a recursive fashion. To that end we abstract away from the particular rule we will use to respond to enumeration and define the notion of a strategy. A strategy is a procedure with persistent state (i.e., a coroutine) that tells us how best to respond to an enumeration of z into the set $W_{i}^{A}$ given some finite set S of stages we are trying to produce agreement with (or force future agreement).

We now define the notion of a procedure whose task is to tell us how to respond to an enumeration of z into $W_{i}^{A}$ at stage s.
Definition 4.1.
A strategy $S$ is a computable function $S (s, z, i)$ (subroutine) with persistent state which enumerates a finite set of elements for entry into $Y_{i}$ and recommends an update to $b_{i}$ . The persistent state of $S (s, z, i)$ consists of a number of variables which $S (s, z, i)$ updates and whose values persist across calls. In addition to the explicitly given arguments and persistent state we also assume that $S (s, z, i)$ has access to a complete history of enumerations/recommendations made11
¹¹
Including enumerations/updates that some calling strategy has already committed to recommending but haven’t yet been made.

prior to it’s execution.

We will describe the behavior of a strategy by giving a procedure by which it updates it’s persistent internal variables (initially set to ↑) and leave it to the pedantic reader to translate such a description into a fully formal object. We also need terminology for the stage (if any) in the intervals $(s_{k - 1}, s_{k})$ at which control is first passed to a particular strategy as follow.
Definition 4.2.
A stage s is an initial enumeration for $S$ (relative to $R_{j, e}$ ) if $S$ is executed at stage s in response to the enumeration of z into $W_{i}^{A}$ and if there is some k such that $s_{k - 1} < s < s_{k}$ and $S$ was not executed during the interval $(s_{k - 1}, s)$ . In such cases we also say that the initial enumeration for $S$ during the interval $(s_{k - 1}, s_{k})$ was into $W_{i}^{A}$ .

Our goal is to prove that, given any value of $s_{- 1}$ we can effectively produce a strategy $S$ which, if followed whenever any $z < s_{- 1}$ enters some $W_{i}^{A}, i ⩽ ⟨ j, e ⟩$ , guarantees that after some finite number of preactive stages we’ll succeed in producing agreement.

Specifically, we’ll show that for any $h : ω \mapsto ω$ with compact support there is a strategy $S^{h}$ such that $S^{h}$ is capable of producing agreement while respecting the requirements $P_{i}$ for $i \in supp h$ provided that the only elements z entering or leaving $W_{i}^{A}$ satisfy $h (i) > z$ . We will then argue that if for every $h^{'}$ with $\int h^{'} < \int h$ (relative to the counting measure) $S^{h^{'}}$ is guaranteed to win then so is $S^{h}$ . As when h is the zero function, there are no values of i, z with $h (i) > z$ , $S^{0}$ clearly satisfies the above assumption. The desired result will follow by induction on $\int h$ .

First, however, we describe the procedure $S^{h}$ . In this description, we style variables which persist across calls in Fraktur, e.g., $r$ , and adopt the computer science convention that we specify temporary values via ‘let’ while we update a variable in the strategy’s internal state with ‘set’.
Definition 4.3.
The strategy $S^{h}$ for $h \in ω^{ω}$ with $supp h = I = {i_{0}, \dots, i_{N - 1}}$ is defined to be the strategy with the following persistent internal variables (all of which are initialized to ↑) which executes Procedure 3 when called as12
¹²
That is, $S^{{arg}_{0}} ({arg}_{1}, {arg}_{2}, {arg}_{3})$ follows the steps in Procedure 3 with $h = {arg}_{0}$ , $s = {arg}_{1}$ , $z = {arg}_{2}$ , $i_{p} = {arg}_{3}$ .

$S^{h} (s, z, i_{p})$ .
$m_{r}^{h} \in ω$ , $r < N$ which records the greatest non-canceled (i.e. accessible) preactive stage $t_{k}$ at which initial enumeration for $S^{h}$ was made into $W_{i_{r}}^{A}$ . Note that we may assume that $m_{r}$ actually records the value of k rather than $t_{k}$ behind the seems and uses k to return $t_{k}$ so that we may assign $t_{m + 1}$ to $m_{r}$ even when that stage hasn’t yet happened.

$S_{r}^{h}, r < N$ holds the current state of the substrategy tasked with producing agreement in response to initial enumerations made into $W_{i_{r}}^{A}$ .

$b_{i_{r}}^{h}$ , $r < N$ identifies the value, if any, needed to cancel the values in $Y_{i_{r}}$ coding the status of $h (i_{r}) - 1$ (the only value $S^{h}$ is directly responsible for) at the next active stage. $S^{h}$ will recommend that $b_{i}$ be set to the least of $b_{i}^{h}$ and the recommendations of any sub-strategies.

In what follows we drop the superscript h from persistent variables when clear from context.
Procedure 3.
Suppose that,
$h \in ω^{ω} \land supp h = I = {i_{0} < i_{1} < \dots < i_{N}}$ .

m is largest with $t_{m} + 1 = s_{m} < s$ .

$z < h (i_{p})$ , $p ⩽ N$

$z ↘_{s} W_{i_{p}}^{A}$
then $S^{h} (s, z, i_{p})$ behaves as follows when executed at stage s. Note that $S^{h} (s, z, i_{p})$ always returns the current value of $b_{i_{p}}$ when it ceases execution as it’s recommendation for $b_{i_{p}}$ .

Enumerate ${[z]}_{i_{p}}^{s}$ into $Y_{i_{p}}$ and exit any strategy (even parent strategies calling this one). There is no need to recommend an update to $b_{i_{p}}$ since we are guaranteed agreement.

¹³
Projecting on the (valid) assumption that all recommendations for enumeration committed to by strategies executing before this one during stage s will be made.

set $b_{i_{r}}, r < N$ to be undefined and execute the following steps:

Set $r = p$ and for all r, $N > r > p$ set $m_{r}$ and $S_{r}$ to ↑.

Let n be such that $t_{n} = m_{p}$ and set $m_{p}$ equal to $t_{m + 1}$ (yes, in the future). For all $r < p$ , if $m_{r} = ↑$ , set $m_{r} = t_{m + 1}$ .

If $S_{p}$ is undefined set $S_{p} = S^{h_{p}}$ with all persistent variables initialized to ↑ where $\begin{matrix} (3) & h_{p} (i) \overset{def}{=} \{\begin{matrix} h (i) - 1 & if i = i_{p} \\ h (i) & otherwise. \end{matrix} \end{matrix}$

then do the following. If $z = h (i_{p}) - 1$ mark ${[z]}_{i_{p}}^{s}$ for enumeration into $Y_{i_{p}}$ and set $b_{i_{p}}$ to a large value returning that as our recommendation for $b_{i_{p}}$ . If $z < h (i_{p}) - 1$ then execute $S_{p} (s, z, i_{p}) = S^{h_{p}} (s, z, i_{p})$ and let our recommendation for $b_{i_{p}}$ be whatever was returned by $S_{p} (s, z, i_{p})$ . In either case, cease all further execution and return to caller.

Only if both $S_{p}$ and $m_{p}$ were defined at the start of execution will we pass beyond this point.

Enumerate the least $q \notin Y_{i_{p}}^{[1]}$ satisfying $l_{t_{n}} < q < l_{t_{n} + 1}$ into $Y_{i_{p}}^{[1]}$ . This has the effect of returning $Y_{i_{p}}$ to the state it was in at stage $m_{p}$ .

Note that, if we’ve previously enumerated a $q^{'} \in (l_{t_{n}}, l_{t_{n} + 1})$ at some stage $t ⩾ t_{n} + 1$ it is enough to enumerate $q < l_{t}$ so we need not worry about running out of values but for simplicity we’ll assume14
¹⁴
An assumption that will be vindicated by the calculation of an explicit bound on the number of preactive stages before agreement and thus on the total number of strategy executions which in turn gives us an explicit bound on the number of values we may need to enumerate between $l_{t_{n}}$ and $l_{t_{n} + 1}$ .

that we always have $l_{t_{n}} < q < l_{t_{n} + 1}$ .

place $b_{i_{p}, t_{n}}$ into $Y_{i_{p}}^{[2]}$ .

This has the effect of canceling (as if we were the active stage $s_{n}$ ) the elements in $Y_{i_{p}}^{[3]}$ which code the membership of those $x < h (i_{p}) - 1$ . Note that this enumeration may be canceled by a sub-strategy at this very stage.

set $b_{i_{p}}^{h}$ to $b_{i_{p}, t_{n}}^{h}$ as at the next active stage $s_{m + 1}$ we must be prepared to cancel the enumerations into $Y_{i_{p}}^{[2]}$ we restored by the enumeration of q.

Execute $S_{r} (z, i_{p})$ (updating the internal state) and pass on the set of elements to be enumerated unmodified. Let b be the recommendation for $b_{i_{p}}$ returned by the sub-strategy just executed.

Let $V = {⟨ σ_{0} \to ⟨ 3, y_{0} ⟩ ⟩, ⟨ σ_{1} \to ⟨ 3, y_{1} ⟩ ⟩, \dots}$ be the set of axioms projected to be active at the end of stage s such that $y_{k}$ has the form $⟨ h (i_{p}) - 1, x ⟩$ but $y_{k} \notin Y_{i, s_{- 1}}^{[3]}$ . If V is empty then set $b_{i_{p}}^{h}$ to ↑. Otherwise, let t be the least stage at which one these axioms is enumerated and $t_{p}$ the least preactive stage after t. If there is no such $t_{p}$ , i.e., $t_{p} = t_{m + 1}$ , then leave $b_{i_{p}}^{h}$ unchanged. Otherwise, set $b_{i_{p}}^{h}$ to $b_{i_{p}, t_{p}}^{h}$ .

Check if, absent this step we are on track to have $Θ (Y_{i_{p}, s}; h (i_{p}) - 1) ↓ \neq W_{i_{p, s}^{A_{s}}} (h (i_{p}) - 1) ↓$ . If not enumerate ${[h (i_{p}) - 1]}_{i_{p}}^{s}$ into $Y_{i_{p}}$ and if $b_{i_{p}}^{h}$ is undefined set $b_{i_{p}}^{h}$ to be large.

Return to caller with recommendation for $b_{i_{p}}$ equal to the minimum of b and $b_{i_{p}}^{h}$ (always passing through any requests for enumeration).

We can now give the rule for responding to a claimed enumeration using the following specification $\begin{matrix} h^{j, e} (i) \overset{def}{=} \{\begin{matrix} s_{- 1} & if i < ⟨ j, e ⟩ + 1 \\ 0 & otherwise \end{matrix} \end{matrix}$

We presume that we initialize a strategy of the form $S^{h^{j, e}}$ at stage $s_{- 1}$ and adopt the following rule.
Rule 4.3.
If $z ↘_{s} W_{i}^{A_{s}}$ , and $R_{j, e}$ claims z then execute $S^{h^{j, e}} (s, z, i)$ and follow it’s recommendations.

Note that, whenever we say things like “execute $S^{h^{j, e}} (S, z, i)$ ” there is an ambiguity between the procedure, which might be instantiated multiple times, and the particular instance. However, we’ll see in part 4 of Lemma 5.3 that in any context each strategy will only ever be instantiated once so there is no risk of confusion.
5. Verification

We now demonstrate that the construction given above satisfies the requirements. In what follows we will frequently prove results about the strategy $S^{h}$ by either via induction or descent on strategies so we remind the reader that relation between strategies which holds whenever $S^{h}$ calls a strategy $S^{h_{r}}$ is a well-founded relation. To see this note that under the counting measure on ω, the integral is a functional from $ω^{ω}$ to ω and for each r we have $\int h > \int h_{r}$ .

To facilitate these arguments we’ve defined $S^{h}$ so that when we initially execute $S^{h_{r}}$ the configuration $S^{h_{r}}$ sees (i.e., $Y_{i}$ ) resembles that seen by $S^{h}$ (and indeed present at stage $s_{- 1}$ ). However, to make use of this we need yet more notation.

Definition 5.1.
If the strategy $S$ is executed at stage s then let $Y_{i, s}^{S -}$ denote the state of $Y_{i}$ at the start of execution of $S$ (including any enumerations scheduled by strategies prior to this point) and let $Y_{i, s}^{S}$ denote the state of $Y_{i}$ at the end of execution of $S$ . When $S$ instantiates $S^{h}$ , we also denote the values $Y_{i, s}^{S -}$ and $Y_{i, s}^{S}$ by $Y_{i, s}^{h -}$ and $Y_{i, s}^{h}$ respectively.

Note that we’ll continue to use notation like $t_{k}$ which is defined relative to a requirement $R_{j, e}$ without making the dependence on j, e explicit when it is obvious from context which requirement $R_{j, e}$ is relevant.
5.1. Correct computations

Our main goal in this section is to prove that Condition 2 holds. However, we first must prove that $Y_{i, s_{k}} ≻ Y_{i, s_{- 1} ↾_{[s_{- 1}]}}$ . But we need a number of utility results first, some of which depend on the very fact to be proved. We therefore present the lemma below but hold off on a proof until we can gather up all the inductive hypotheses needed.

Lemma 5.2.
Suppose that $R_{j, e}$ isn’t initialized between $s_{- 1}$ and $s_{k}$ and $S_{s_{k}} (R_{j, e}) < 2$ then
If $i ⩽ ⟨ j, e ⟩$ and $x < s_{- 1}$ we have $Y_{i, s_{- 1}}^{[3] [x]} ≺ Y_{i, s_{k}}^{[3] [x]}$ .

If $s_{k}$ is the greatest active stage less than s and $Y_{i, s}^{'}$ is the result of enumerating $b_{i, s}$ into $Y_{i, s}$ , $i ⩽ ⟨ j, e ⟩$ , $x < s_{- 1}$ then $Y_{i, s}^{'}^{[3] [x]} ≻ Y_{i, s - 1}^{[3] [x]}$ .

We now prove our utility results, some of which assume that Lemma 5.2 holds at earlier stages.
Lemma 5.3.
Suppose that $S$ instantiates $S^{h}$ and receives an initial enumeration of z into $W_{i}^{A}$ at stage $t \in (s_{k}, s_{k + 1})$ (note that $s_{k + 1}$ is possibility infinite) then
If x is enumerated into $W_{i^{'}}^{A}$ at stage $s \in (s_{k}, s_{k + 1})$ then $S$ is executed to handle this enumeration iff $x < h (i^{'})$ .

At no stage in $(s_{k}, s_{k + 1})$ does any strategy other than $S$ enumerate elements into $Y_{i}^{[3] [h (i) - 1]}$ .

At no stage in $(s_{k}, s_{k + 1})$ does any strategy not called from $S$ enumerate elements into $Y_{i}^{[3] [z]}$ .

No other strategy implementing $S^{h}$ executes during $(s_{k}, s_{k + 1})$ .

If $S$ executes stage Step 2e enumerating q with $l_{t_{n}} < q < l_{t_{n} + 1}$ into $Y_{i}^{[1]}$ then no $q^{'} < l_{t_{n}}$ has been enumerated since stage $t_{n}$ .
If we further assume that Lemma 5.2 holds for $s_{k^{'}}, k^{'} ⩽ k$ and $x < h (i^{'})$ then we may also conclude.
For all $k^{'} ⩽ k$ , $x < s_{- 1}$ and $s \in (s_{k^{'}}, s_{k^{'} + 1})$ if $(\forall x^{'} ⩽ x) (x^{'} \notin W_{i^{'}, s}^{A} ∖ W_{i^{'}, s_{- 1}}^{A})$ then $Y_{i^{'}, s_{- 1}}^{[3] [x]} ≺ Y_{i^{'}, s}^{[3] [x]}$ .

For all $i^{'}$ , x if $x < h (i^{'})$ then $Y_{i^{'}, s_{- 1}}^{[3] [x]} ≺ Y_{i^{'}, t}^{h -}^{[3] [x]}$ . In other words, initial enumerations to strategies start with a blank slate.

Proof.
We prove these claims by descent. For claims 1, 2, 3 and 4 we observe they clearly hold for $h = h^{j, e}$ and we now prove that these claims also hold for the strategies $S_{r} = S^{h_{r}}$ called from $S$ .

To see that 1 holds note that the only time $S$ doesn’t pass on z is when $z = h (i) - 1$ and that by eq. (3) this is the only element which isn’t below $h_{r}$ . To see that 2 (and, thus, 3) holds note that only Step 5 ever enumerates elements and then only if $z = h (i_{p}) - 1$ . $S_{r}$ is passed any element $x < h_{r} (i^{'})$ as the only time x received by $S$ and $S$ only enumerates into $Y_{i}^{[⩽ 2]}$ before executing $S_{r}$ for the first time.

To see that 5 holds it is enough to observe that if the first time after reinitialization that $S$ runs is $s \in (s_{k^{'}}, s_{k^{'} + 1})$ (with $s_{k^{'} + 1}$ possibly infinite) then neither $S$ nor any strategy called from it will enumerate elements below $l_{s_{k^{'}}}$ . Then observe that if we ever run $S_{r}$ with $r < p$ we reinitialize $S_{r}$ so that if we had run some strategy that wasn’t called by $S$ but enumerated a value below $l_{t_{n}}$ we would have reinitialized $S$ after $t_{n}$ contradicting the choice of q. The conclusion follows by observing that, after stage $t_{n}$ , the first time $S$ is run it enumerates q before any sub-strategy it calls enumerates anything.

To prove 6 note that the base case holds by the assumption of Lemma 5.2 and we can ignore any stages at which no enumeration into $W_{i^{'}}^{A}$ is claimed by $R_{j, e}$ . If $S^{h^{'}} (s, y, i^{'})$ is executed at s then $h^{'} (i^{'}) - 1 ⩾ y > x$ so direct enumeration can’t cause disagreement. This leaves only enumeration into $Y_{i^{'}}^{[⩽ 2]}$ as a threat. However, when this happens Step 2e restores the state as of $t_{n}$ and by the inductive assumption (with $t_{n}$ replacing s and $s_{n - 1}$ replacing $s_{k^{'}}$ ) we can conclude that if no $x^{'} ⩽ x$ are in $W_{i^{'}, s}^{A} ∖ W_{i^{'}, s_{- 1}}^{A}$ then $Y_{i^{'}, s_{- 1}}^{[3] [x]} ≺ Y_{i^{'}, s}^{[3] [x]}$ . Conversely, if there is such an $x^{'}$ then Step 2f enumerates $b_{i^{'}, t_{n}}$ into $Y_{i^{'}}^{[2]}$ which, by 5 ensures that $Y_{i^{'}, s_{- 1}}^{[3] [x]} ≺ Y_{i^{'}, s}^{[3] [x]}$ by the assumption of Lemma 5.2.

With item 6 established we can now proceed to prove 7 in exactly the same manner. Note that 7 clearly holds if $h = h^{j, e}$ by our assumption that Lemma 5.2 holds at $s_{k}$ . For the inductive case we need merely replace the assumption that no $x^{'} ⩽ x$ are in $W_{i^{'}, s}^{A} ∖ W_{i^{'}, s_{- 1}}^{A}$ with the assumption that $S^{h^{'}}$ is executing before the initial enumeration for $S^{h}$ noting that by 1 if $S^{h^{'}} (s, y, i^{'})$ executes before the initial enumeration for $S^{h}$ in $(s_{k}, s_{k + 1})$ then $h^{'} (i^{'}) - 1 > x$ . □

We now return and provide the promised proof.
Lemma 5.2.
Suppose that $R_{j, e}$ isn’t initialized between $s_{- 1}$ and $s_{k}$ and $S_{s_{k}} (R_{j, e}) < 2$ then
If $i ⩽ ⟨ j, e ⟩$ and $x < s_{- 1}$ we have $Y_{i, s_{- 1}}^{[3] [x]} ≺ Y_{i, s_{k}}^{[3] [x]}$ .

If $s_{k}$ is the greatest active stage less than s and $Y_{i, s}^{'}$ is the result of enumerating $b_{i, s}$ into $Y_{i, s}$ , $i ⩽ ⟨ j, e ⟩$ , $x < s_{- 1}$ then $Y_{i, s}^{'}^{[3] [x]} ≻ Y_{i, s - 1}^{[3] [x]}$ .

Proof.
We first prove 2 on the assumption that 1 holds at each $s_{k^{'}}, k^{'} ⩽ k$ .

By Lemma 5.3 it is enough to argue that if $z = h (i) - 1$ then $b^{h} i, s$ (and thus $b_{i, s} ⩽ b^{h} i, s$ ) cancels any changes made by $S^{h} (s, z^{'}, i)$ , $z^{'} ⩽ z$ to $Y_{i, s}^{'}^{[3] [z]}$ . After all, item 7 ensures that the claim holds true at all stages prior to such an enumeration, item 7 ensures that it is true when $S^{h}$ receives it’s initial enumeration, stages at which enumeration occurs into some $W_{i^{'}}^{A}, i^{'} \neq i$ don’t alter $Y_{i, s}^{'}^{[3]}, b_{i}^{h}$ or $b_{i}$ . But the combination of Steps 4, 5 and out assumption that 1 holds at all $s_{k^{'}}, k^{'} ⩽ k$ ensure that $b^{h} i, s$ is small enough to cancel any active axioms causing $Y_{i, s}^{'}^{[3]}^{[z]}$ to disagree with $Y_{i, s_{- 1}}^{[3]}^{[z]}$ or Step 2d when it is an initial enumeration and $m_{i}$ is undefined.

We now note that 2 is trivial if $k = - 1$ and otherwise follows by induction on k by application of 2 and the fact that Procedure 1 executes Procedure 2 when it enumerates $c_{k}$ . □

We are now in a position to prove Condition 2 holds. We break the proof up into two lemmas.
Lemma 5.4.
For all s, i, $Θ (Y_{i, s})$ is compatible with $W_{i, s}^{A_{s}}$ . Moreover, if $W_{i, s}^{A_{s}} (x) ↑$ then $Θ (Y_{i, s}; x) = 0$ .
Proof.
The moreover claim is trivial since, if $x > l_{s}$ , then we’ve taken no action regarding x at or before stage s. We let i be arbitrary and proceed by induction to prove the main claim. Trivially, the claim holds if $s = 0$ so we assume that the claim holds for all stages prior to s and argue the holds at s. If no enumeration happens at s into either A or $W_{i}^{A}$ the result is immediate. So we consider the following (disjoint) cases. Case $x ↘_{s} W_{i}^{A}$ :
This case can be broken into two subcases.

Case x is claimed by some $R_{j, e}$ :
In this case, there is some $S^{h}$ executing at s such that $h (i) - 1 = x$ . Step 5 plus the fact that no elements are enumerated into either $Y_{i}^{[⩽ 2]}$ or $Y_{i}^{[3]}^{[x]}$ after Step 5 during stage s establish the claim.
Case x is unclaimed:
In this case, the result follows immediately by Rule 4.1.

Case $c_{k} ↘_{s} A^{[3]}$ :
Suppose $R_{j, e}$ is responsible for the numeration of $c_{k}$ and consider the following subcases.

Case $x \in W_{i, s_{- 1}}^{A_{s_{- 1}}}$ :
In this case, $x \in W_{i, s}^{A_{s}}$ as any enumeration below $l_{s_{- 1}}$ would have injured $R_{j, e}$ . Similarly, $Y_{i, s_{- 1}}^{[3]}^{[x]} \subset Y_{i, s}^{[3]}^{[x]}$ . But as we only enumerate elements into $Y_{i}^{[3]}^{[x]}$ when it appears that the lemma would fail no such elements are ever enumerated at or after $s_{- 1}$ so the claim holds by virtue of the inductive hypothesis applied at stage $s_{- 1}$ .
Case $x \notin W_{i, s_{- 1}}^{A_{s_{- 1}}}$ :
Note that if $x ⩾ s_{- 1} \lor i > ⟨ j, e ⟩$ then the claim follows immediately via the action of Step 2. So assume $x < s_{- 1} \land i ⩽ ⟨ j, e ⟩$ . Since x is enumerated into $W_{i}^{A}$ after stage $s_{- 1}$ , x is (by induction) enumerated dependent on $A^{[3]} (c_{k}) = 0$ . Thus, $x \notin W_{i, s}^{A_{s}}$ and the desired result follows by Lemma 5.2.

Case $b = b_{k} ↘_{s} A^{[2]}$ :
Suppose $R_{j, e}$ is responsible for the numeration of b. Step 2 ensures that there is some k with $s_{k} < s$ such that $s_{k} - 1 \approx s - 1$ . But the enumeration of b (chosen large at stage $s_{k}$ ) cancels all enumerations into $Y_{i}^{[3]}$ after stage $s_{k} - 1$ and as $s_{k} - 1 \approx s - 1$ this ensures that $Y_{i, s} ≻ Y_{i, s_{k}}$ . As the enumeration of b also cancels any enumeration of x into $W_{i}^{A}$ after stage $s_{k} - 1$ the result follows from the application of the inductive hypothesis to stage $s_{k}$ .
Case $a ↘_{s} A^{[1]}$ :
Suppose $R_{j, e}$ is responsible for the numeration of a. The enumeration of a cancels all enumerations into $Y_{i}^{[3]}$ since the stage t at which b was enumerated as well as any enumeration of x into $W_{i}^{A}$ after stage $t - 1$ . As no enumerations were made into $Y_{i}^{[⩽ 2]} ↾_{[l_{t}]}$ since stage $t - 1$ the state at stage $t - 1$ is restored and the claim follows from the inductive hypothesis applied at stage $t - 1$ .
□

Now to prove the corresponding claim for $Γ_{i}$ .
Lemma 5.5.
For all s, i, $Γ_{i} (A_{s} \oplus W_{i, s}^{A_{s}}) ≺ Y_{i, s}$ and $Γ_{i}$ is well-defined.

Note that, here $Γ_{i}$ really refers to whatever version of the functional is left uninjured at the end of stage s since we will reinitialize each $Γ_{i}$ finitely many times.
Proof.
By Definition 3.11 it is evident that $Γ_{i}$ is well-defined. To prove the remainder of the claim it is enough to show that if $t < s$ and $P_{i}$ is not injured during the interval $(t, s]$ then $\begin{array}{l} (4a) & A_{s} \oplus W_{i, s}^{A_{s}} ≻ & A_{t} \oplus W_{i, t}^{A_{t}} \\ (4b) & ⟹ Y_{i, t} ↾_{t} ≺ Y_{i, s} \end{array}$

The claim is trivial if $t = s$ so we assume the claim holds for all $s^{'}$ with $t ⩽ s^{'} < s$ and prove it also holds at s. This is evident if no axioms placing an element into A or $W_{i}^{A}$ are enumerated at stage s. So, suppose, for contradiction, that some element is enumerated at stage s and $P_{i}$ is not injured during the interval $(t, s]$ but that eq. (4) fails. We consider the following cases. Case $z ↘_{s} W_{i}^{A}$ and $A_{s - 1} ≺ A_{s}$ :
For the claim to fail we must have z in (our approximation to) $W_{i}^{A}$ at stages t and $z < t$ but not $s - 1$ . Thus, we must have some $q < l_{t}$ in $A_{s - 1} ≺ A_{s}$ but not $A_{t}$ rendering eq. (4a) false.
Case $q ↘_{s} A$ :
Suppose that $R_{j, e}$ enumerates q. Note that if $i > ⟨ j, e ⟩$ and $R_{j, e}$ takes any action then $P_{i}$ is injured giving us the desired conclusion trivially. Thus, we can assume $i ⩽ ⟨ j, e ⟩$ and consider the following subcases.

Case $q = c_{k} ↘_{s} A^{[3]}$ :
We must have $t < s_{- 1}$ or $c_{k^{'}}$ makes eq. (4a) false where $s_{k^{'}}$ is the least active stage greater than t. If $A_{t} \oplus W_{i, t}^{A_{t}} ⊀ A_{s_{- 1}} \oplus W_{i, s_{- 1}}^{A_{s_{- 1}}}$ then that disagreement would persist until stage s making eq. (4a) false. But Lemma 5.2 lets us conclude that $Y_{i, s_{- 1}} ↾_{t} ≺ Y_{i, s}$ so $Y_{i, t} ↾_{t} ≺ Y_{i, s}$ .
Case $q ↘_{s} A^{[⩽ 2]}$ :
This follows from the inductive assumption plus Lemma 5.2 which ensures that if $t < s_{- 1}$ then eq. (4b) holds. If $t ⩾ s_{- 1}$ then the enumeration of some $c_{k}$ or q itself renders eq. (4a) false.

□

We can now prove the desired proposition. Proposition 5.6.
Condition 2 is satisfied, i.e., Θ and $Γ_{i}$ are well-defined and correct at every stage.
Proof.
Immediate from lemmas 5.4 and 5.5 □

5.2. Winning strategies

In this section we seek to show that $R_{j, e}$ only acts finitely many times. To prove this we need to show that our strategies eventually guarantee we find agreement between stages. But the strategy $S^{h}$ doesn’t execute $S^{h_{r}}$ on consecutive intervals $[s_{k}, s_{k + 1}]$ . It may, instead, skip a number of active stages during which $S^{h}$ executes some other sub-strategy only to return to $S^{h_{r}}$ much later so we need some way to talk about intervals which behave as if we had run $S^{h_{r}}$ on consecutive intervals.

To this end, we make the following definitions (these are implicitly relative to a particular module $R_{j, e}$ ).

Definition 5.7.
Say that t is an h successor of $s < t$ (relative to the module $R_{j, e}$ ), just if t is an initial enumeration for $S^{h}$ and letting ${\hat{Y}}_{i} = Y_{i, s}^{h -}$ we have $\begin{matrix} (\forall i ⩽ ⟨ j, e ⟩) (\forall x < h (i)) (Y_{i, s}^{[⩽ 2]} ↾_{[s]} ≺ {\hat{Y}}_{i}^{[⩽ 2]} \land Y_{i, s}^{[3]}^{[x]} ≺ {\hat{Y}}_{i}^{[3]}^{[x]}) \end{matrix}$

Informally speaking, t is an h successor of s just if for all $i ⩽ ⟨ j, e ⟩$ the state of $Y_{i}$ when $S^{h}$ receives it’s initial enumeration during t agrees with that of $Y_{i, s}$ excepting only elements $S^{h}$ can ignore as too large for it’s concern. Using this notion we can now define a notion of a sequence of intervals that look as if they are consecutive as far as $S^{h}$ is concerned.
Definition 5.8.
Say that a sequence $[{\hat{t}}_{0}, {\hat{s}}_{0}], [{\hat{t}}_{1}, {\hat{s}}_{1}] \dots, [{\hat{t}}_{n}, {\hat{s}}_{n}]$ of intervals is $S^{h}$ -virtually consecutive (or just h-virtually consecutive) if
$S^{h}$ is not reinitialized during $({\hat{t}}_{0}, {\hat{s}}_{n})$

At stage ${\hat{t}}_{0}$ $S^{h}$ is in it’s initialized state, i.e., hasn’t been executed since it was last reinitialized.

${\hat{s}}_{k}$ is the least active stage greater than ${\hat{t}}_{k}$

For all $k < n$ , either ${\hat{t}}_{k + 1}$ is an h-successor of ${\hat{s}}_{k}$ or ${\hat{t}}_{k + 1} = {\hat{s}}_{k + 1}$ and no elements are enumerated during the interval ending at ${\hat{s}}_{k + 1}$ and started at the prior active stage.

Every interval ${\hat{t}}_{k}$ , ${\hat{s}}_{k}$ satisfying the above between ${\hat{t}}_{0}$ and ${\hat{s}}_{n}$ appears in the above list.

Note that if the sequence is genuinely consecutive, i.e., ${\hat{t}}_{k + 1} = {\hat{s}}_{k} + 1$ for all k, then it is trivially h-virtually consecutive. Now let’s define what it means for a strategy to be successful.
Definition 5.9.
Say that the strategy $S^{h}$ is a winning strategy if there is a number $N_{h}$ (the winning number for h) such that if $[{\hat{t}}_{0}, {\hat{s}}_{0}], \dots, [{\hat{t}}_{N_{h} - 1}, {\hat{s}}_{N_{h} - 1}]$ is an h virtually consecutive sequence of intervals of length $N_{h}$ then, for any acceptable enumeration of elements into the sets $W_{i}^{A}, i \in supp h$ satisfying $x < h (i)$ there are distinct $k, k^{'} < N_{h}$ if the recommendations of $S^{h}$ are followed we have ${\hat{s}}_{k} - 1 \approx {\hat{s}}_{k^{'}} - 1$ .

We leave the task of formalizing the notion of relative to any acceptable enumeration to the pedantic reader but take the intended content to be clear. In particular, a winning strategy is guaranteed to produce agreement in a bounded number of intervals even if we permute the indices to $r.e.$ sets. With this notion in place we can finally demonstrate that our strategies are winning strategies.
Lemma 5.10.
Suppose that for all $h_{r}$ , $r < | supp h |$ the strategy $S^{h_{r}}$ is a winning strategy with winning number $N_{h_{r}}$ then $S^{h}$ is a winning strategy.
Proof.
Suppose that $[{\hat{t}}_{0}, {\hat{s}}_{0}], [{\hat{t}}_{1}, {\hat{s}}_{1}] \dots, [{\hat{t}}_{N - 1}, {\hat{s}}_{N - 1}]$ is a sequence of h virtually consecutive intervals with $N = \prod_{r < | supp h |} (N_{h_{r}} + 2)$ with $z_{k} ↘_{{\hat{t}}_{k}} W_{i_{k}}^{A}$ We argue there are $k, k^{'} < N$ with ${\hat{t}}_{k} \approx {\hat{t}}_{k^{'}}$ .

We now note that there must be a subsequence of length at least $N_{h_{r}} + 2$ on which we always execute the same substrategy but never reinitialize that strategy. Specifically, we observe that there is an $\hat{i} \in supp h$ and a subsequence ${\hat{t}}_{n_{k}}, k < N_{h_{r}} + 2$ such that $i_{n_{k}} = \hat{i}$ and for all $n^{'}$ with $n_{k} < n^{'} < n_{k + 1}$ we have $i_{n^{'}} > \hat{i}$ . This follows since if this isn’t witnessed by $i_{0}$ then there must be a subsequence of length at least $N = \prod_{1 < r < | supp h |} (N_{h_{r}} + 2)$ .

As the support of h is finite we must eventually find such a subsequence. Call this a good $\hat{i}$ subsequence and let $\hat{r} = | {y \in supp h \land y < \hat{i}} |$ , i.e., $S^{h_{\hat{r}}}$ is the strategy called (if necessary) by $S^{h}$ in an interval in which the initial enumeration was into $W_{\hat{i}}^{A}$ . Thinking of this in terms of a finite injury construction this subsequence represents the stages at which the $\hat{i}$ strategy gets attention without intervening injury.

Suppose that for some $k < N_{h_{r^{'}}} + 1$ we fail to enumerate any $x < h (i) - δ_{\hat{i}} (i)$ into $W_{i}^{A}$ during $({\hat{t}}_{n_{k}}, {\hat{s}}_{n_{k}})$ . We claim that ${\hat{s}}_{n_{k}} - 1 \approx {\hat{s}}_{n_{k} + 1} - 1$ . By h-virtual connectivity when $S^{h}$ begins execution at stage ${\hat{t}}_{n_{k + 1}}$ , $Y_{i}^{[⩽ 2]}$ is compatible with it’s state at stage ${\hat{s}}_{n_{k}} - 1$ . Note that, by Definition 5.9, we may assume that only $x < h (i)$ are enumerated into any $W_{i}^{A}$ . Thus, in any interval the first element is enumerated at stage ${\hat{t}}_{k}$ . When $S^{h}$ executes at stage ${\hat{t}}_{n_{k + 1}}$ the action of Step 2e cancels any elements enumerated both at stage ${\hat{s}}_{n_{k}}$ and by any ancestor strategies executing Step 2f (which must occur earlier in that stage).

As no $x < h (i) - δ_{\hat{i}} (i)$ was enumerated during the interval $({\hat{t}}_{n_{k}}, {\hat{s}}_{n_{k}})$ , Step 2f never enumerates any elements and as no parent strategy enumerates any elements into the first two columns of $Y_{i}$ after executing it’s child that agreement persists until the end of stage, and, indeed, the end of stage ${\hat{s}}_{n_{k} + 1} - 1$ .

Thus, we can assume that we have a subsequence of length $[{\hat{t}}_{n_{k}}, {\hat{s}}_{n_{k}}], k < N_{h_{r^{'}}} + 1$ with $r_{n_{k}} = r^{'}$ of length $N_{h_{r^{'}}} + 1$ during which we never reinitialize $S_{r^{'}}$ and during each interval $[{\hat{t}}_{n_{k}}, {\hat{s}}_{n_{k}})$ there is a ${\hat{t}}_{n_{k}}^{'}$ at which we execute $S^{h_{r^{'}}}$ . To verify the claim we first show that the sequence $[{\hat{t}}_{n_{k}}^{'}, {\hat{s}}_{n_{k}}], k < N_{h_{r^{'}}}$ is $h_{r^{'}}$ virtually consecutive. Note that, $i_{r^{'}} = \hat{i}$ here and that we may presume that this is the first such subsequence, i.e., ${\hat{t}}_{n_{0}}$ is the first execution of $S^{h_{r^{'}}}$ since last reinitialization.

This leaves only part 4 of Definition 5.8 to be verified but this follows by Lemma 5.2. Now suppose that for some k the only element enumerated during the interval $[{\hat{t}}_{n_{k}}, {\hat{s}}_{n_{k}})$ with $k < N_{h_{r^{'}}}$ into $W_{\hat{i}}^{A}$ . By the same reasoning above we’ll see agreement at ${\hat{s}}_{n_{k + 1}}$ since this means that for $\hat{i}$ we behave as above and the inductive hypothesis handles enumeration into $W_{i}^{A}, i \neq \hat{i}$ . Thus, we can assume that in each interval $[{\hat{t}}_{n_{k}}, {\hat{s}}_{n_{k}})$ we see some $x < h (\hat{i})$ enumerated into $W_{\hat{i}}^{A}$ . In this case, when that x is enumerated the operation of Step 2e by $S^{h_{r^{'}}}$ cancels any element enumerated at stage ${\hat{t}}_{n_{k}}$ during Step 2f. Thus, the situation with respect to the first two columns of the sets $Y_{i}$ is no different than if enumeration was restricted only to those x entering $W_{i}^{A}$ where $x < h_{r^{'}} (i)$ . □

We can now prove our desired result. Proposition 5.11.
$R_{j, e}$ acts only finitely many times.
Proof.
Suppose not. The only possibility is that some module $R_{j, e}$ is initialized at some stage $s_{- 1}$ and never subsequently reinitialized by the action of any higher priority module. But this can only happen if at all active stages $s_{k}, k > 0$ we have $S_{s_{k}} (R_{j, e}) = 1$ .

But, by Lemma 5.10 we have that $S^{h^{j, e}}$ is a winning strategy. Consider the sequence $[{\hat{t}}_{k}, s_{k}]$ where ${\hat{t}}_{k}$ is the first stage subsequent to $s_{k}$ at which $R_{j, e}$ claims an enumeration. As enumerations that go unclaimed or are claimed by modules with lower priority don’t enumerate elements that are small relative to the last stage at which $R_{j, e}$ acts into the first two columns of any $Y_{i}$ it is trivial that this sequence is $h^{j, e}$ virtually contiguous. It thus follows that there are k, $k^{'}$ with $s_{k} - 1 \approx s_{k^{'}} - 1$ and thus at stage $s_{k^{'}}$ we have $S_{s_{k^{'}}} (R_{j, e}) = 2$ contrary to our assumption. Hence every module acts only finitely often. □

5.3. Putting it together

Lemma 5.12.

Every requirement of the form $R_{j, e}$ is satisfied.

Proof.

Assume, for a contradiction, $R_{j, e}$ isn’t satisfied (i.e., $Φ_{j} (A) = X_{e} \land Φ_{j} (X_{e}) = A$ ) and that $t_{0}$ is the last stage at which the module $R_{j, e}$ acts. If $s > t_{0}$ then $S_{t_{0}} (R_{j, e}) = S_{s} (R_{j, e})$ and $A_{t_{0}} ≺ A_{s}$ since such a change would require $R_{j, e}$ act at that stage. Hence, $A_{t_{0}} ≺ A$ .

If the variable c is defined for the $R_{j, e}$ at stage $t_{0}$ (i.e., if $S_{t_{0}} (R_{j, e}) ⩾ 2$ ) we leave that value in place but if not set $c = c_{m}$ where $c_{m}$ is the least m such that $c_{m}$ hasn’t been enumerated into $A^{[3]}$ . Note that $c_{0}$ must be defined at $t_{0}$ since if $S_{t_{0}} (R_{j, e}) = ↑$ then $R_{j, e}$ acts at stage $t_{0} + 1$

By Lemma 3.7 let $s > t_{0}$ be a stage at which $Ψ (c, s)$ holds. But if $S_{s} (R_{j, e}) < 3$ then we have $R_{j, e}$ acts at stage $s + 1$ . On the other hand if $S_{s} (R_{j, e}) = 3$ then we have $Ψ^{3} (c, {\hat{s}}_{0}, {\hat{s}}_{1}, {\hat{s}}_{2}, s)$ . However, this is exactly what Lemma 3.9 denies. Contradiction! □

Before we can complete the proof of our main theorem we must fulfill the commitment we made in Condition 1 and verify that $Γ_{i} (A \oplus W_{i}^{A})$ is total.

Lemma 5.13.

There are infinitely many stages s such that $A_{s} ≺ A_{t}$ for all $t > s$ and thus $A_{s} ≺ A$ . Thus, Condition 1 hold and $Γ_{i} (A \oplus W_{i}^{A})$ is total.

Note that, this result entails that A is $Δ_{2}^{0}$ .

Proof.

To verify the primary claim note that if $R_{j, e}$ acts at stage s it injures lower priority modules and when reinitialized those modules never enumerate an element into any column of A below $l_{s + 1}$ . Thus, if $s_{k}$ is last stage that any module with priority $⩽ k$ acts we have $A_{t} ≻ A_{s_{k}}$ for all $t > s_{k}$ and $A_{s_{k}} ≺ A$ .

Condition 1 follows immediately and the totality of $Γ_{i} (A \oplus W_{i}^{A})$ was observed to follow from this fact in the discussion immediately following Definition 3.11. □

We can now easily complete the proof of our main theorem.

Theorem 1.4.

There is a properly $3 - REA$ set A which can’t be extended to a properly $4 - REA$ set. The set A can also be taken to be $Δ_{2}^{0}$ .

Proof.

By Lemma 5.12 to show that A is properly $3 - REA$ but can’t be expanded to a $4 - REA$ set it is enough to verify that the requirements of the form $P_{i}$ is satisfied. Clearly $Θ (Y_{i})$ is total for all i and $Γ_{i} (A \oplus W_{i}^{A})$ is total by Lemma 5.13. Hence, it’s enough to show that these functionals are correct at every stage. But by proposition 5.6 this holds as long as no module for $P_{i}$ is injured infinitely many times. However, as only modules of the form $R_{j, e}$ are responsible for injuries this is immediate from proposition 5.11.

The fact that A can be taken to be $Δ_{2}^{0}$ follows from Lemma 5.13. □

References

G.J.

Carl and

R.A.

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

P.A.

Cholak and

P.G.

Hinman, Iterated relative recursive enumerability, Archive for Mathematical Logic 33(5) (1994), 321–346. doi:10.1007/BF01278463.

Odifreddi, Classical Recursion Theory: The Theory of Functions and Sets of Natural Numbers , Vol. 1, Elsevier, 1992.

Rogers, Theory of Recursive Functions and Effective Computability , MIT Press, Cambridge, Mass, 1987.

R.I.

Soare and

Stob, Relative recursive enumerability, in: Studies in Logic and the Foundations of Mathematics , Vol. 107, Elsevier, 1982, pp. 299–324.

Extending properly n - REA sets 1

Abstract

Keywords

1. Introduction

2.1. Notational conventions

3 That is, A ⊕ B = def { y ∣ y = 2 x ∧ x ∈ A ∨ y = 2 x + 1 ∧ x ∈ B } and ⨁ n ∈ S X n = def { ⟨ n , x ⟩ | n ∈ S ∧ x ∈ X n } .

6 Remember, that we’ve used the fact that we will ensure A s ≺ A infinitely often to allow us to set the ‘use’ of a computation placing z ∈ W i A at stage s to l s .

3.6.1. Multiple elements entering some W i 0 A

3.6.2. Multiple P i requirements

8 If z ∈ W i , s − 1 A then z won’t leave W i A as a result of any enumeration we make in trying to meet R j , e ensuring that coding the status of z isn’t in tension with our attempt to meet R j , e .

4.1. General framework

Rule 4.1. If an axiom enumerates z into W i A at stage s but z goes unclaimed then we enumerate [ z ] i s into Y i [ 3 ] . 4.2. Module R j , e

4.2.1. Even stages

Procedure 1 (Even Stages of R j , e ).

Procedure 2 (Resetting Y i ).

4.2.2. Odd stages

References

³
That is, $A \oplus B \overset{def}{=} {y ∣ y = 2 x \land x \in A \lor y = 2 x + 1 \land x \in B}$ and $⨁_{n \in S} X_{n} \overset{def}{=} {⟨ n, x ⟩ | n \in S \land x \in X_{n}}$ .

⁶
Remember, that we’ve used the fact that we will ensure $A_{s} ≺ A$ infinitely often to allow us to set the ‘use’ of a computation placing $z \in W_{i}^{A}$ at stage s to $l_{s}$ .

3.6.1. Multiple elements entering some $W_{i_{0}}^{A}$

3.6.2. Multiple $P_{i}$ requirements

⁸
If $z \in W_{i, s_{- 1}}^{A}$ then z won’t leave $W_{i}^{A}$ as a result of any enumeration we make in trying to meet $R_{j, e}$ ensuring that coding the status of z isn’t in tension with our attempt to meet $R_{j, e}$ .

Rule 4.1.
If an axiom enumerates z into $W_{i}^{A}$ at stage s but z goes unclaimed then we enumerate ${[z]}_{i}^{s}$ into $Y_{i}^{[3]}$ .
4.2. Module $R_{j, e}$

Procedure 1 (Even Stages of $R_{j, e}$ ).

Procedure 2 (Resetting $Y_{i}$ ).