An infinite r.e. subset of $\mathbb{N}$ is simple, if it is coinfinite and it intersects every infinite r.e. subset of $\mathbb{N}$
I have been used to the proof of existence of a simple set by the finite injury priority method, and this one is quite clear to me. However, I do have a problem with understanding a certain thing about Post's original proof (as it is given in the books of R. Soare or in the handbook by P. Odifreddi).
The proof goes as follows: we construct a simple set $A = \bigcup_{s \in \mathbb{N}} A_s$ by stages such that for every $e \in \mathbb{N}$ we wish to meet the requirement:
$$ |W_e| = \infty \: \: \Rightarrow \: \: W_e \cap A \neq \emptyset.$$
Stage $s = 0$: let $A_0 = \emptyset$.
Stage $s+1$: given $A_s$, we search through $e < s$ and check if $W_{e,s} \cap A_s = \emptyset$. If not, it means we have already enumerated an element of $W_e$ into $A$. If yes, then we are suuposed to search for the minimal $n > 2e$ such that $n \in W_{e,s}$.
The condition $n > 2e$ is to guarantee that our set $A$ is coinfinite, and this part is clear.
But, I do have a question about computability of the condition: $$ \exists n > 2e \: n \in W_{e,s}.$$
This condition does not seem to be recursive. Fix $s$, and fix $e$. We do not know if $W_e$ is finite (or if $W_{e,s}$) is finite) and we cannot recursively decide it (since the index set $Fin$ is not even r.e.), and it might happen that there are no $n>2e$ such that the $e$-th Turing Machine halts on $n$ within $\leq s$ steps.
What I would like to understand, is how does the dovetailing come in play here?
It seems to me that even if for a fixed $s$ we check if $1 \in W_{0,s}$, $3 \in W_{1,s}$, ..., $2e+1 \in W_{e,s}$, ..., $2s-1 \in W_{s-1, s}$, and then continue with higher and higher numbers (i.e. we check if $2 \in W_{0,s}$, $3 \in W_{0,s}$, ..., $n \in W_{0,s}$, etc., it still might happen that $W_{0,s} = \{0\}$, $W_{1,s} = \{2\}$, ..., $W_{e,s} = \{2e\}$, etc. (i.e. that within $s$ steps these first $s$ Turing Machines halt only on these malicious singletons), and we will never find the necessary $n$'s.
Can we e.g. put an upper bound for these $n's$ when we are at the stage $s$ of the construction? But it does not seem to solve the problem, since the unfortunate case described above might still happen.
Or does the solution somehow follow from the fact that there are inifnitely many infinite r.e. sets? If so, how?
Edit: an additional comment - what we're trying to construct is a certain subset of a set: $$ S:= \{n: \exists e \: n \in W_e \: \wedge \: n > 2e \}.$$
The set $S$ is r.e. Therefore, since it is nonempty, it is a range of some total recursive function $f$.
The condition that carves out $A$ from $S$ is given by stages, i.e. at the stage $s$, the constraint is: $$ e < s \: \wedge \: W_{e,s} \cap A_s = \emptyset $$ (why do we need to bound $W_e$? IS it the case that we do not just require that $W_e \cap A_s = \emptyset$ since such a condition would not be recursive?)
Now, since $f$ is recursive, is it the case that we can think of what is happening at the stage $s$ of the construction as follows: Compute all $f(k)$'s (from $f(0)$ up to $f(s)$) and check if $$\exists e < s \: f(k) \in W_{e,s} \: \wedge W_{e,s} \cap A_s = \emptyset,$$ and if yes, enumerate the smallest $f(k)$ into $A$, and if not proceed to the next stage (and the construction will guarantee that we will meet every $W_e$)?
This goes back to the definition of $W_{e,s}$. I don't have Soare on hand, but the usual trick here is to make the convention that $W_{e,s}\subseteq s$, that is, "large" numbers aren't enumerated "early" (intuitively, the motivation here is that a computation has to scan its input before halting). This is a convention similar in spirit to the one that at most one number enters at each stage, that is, $\vert W_{e, s+1}\setminus W_{e,s}\vert\le 1$. With this convention, the condition is indeed recursive. My memory is that Soare actually makes this condition explicit early on in the text, but perhaps easy to overlook.
EDIT: OK fine I have Soare on hand. Referring to the old book, it looks like this convention might be ultimately Exercise 3.11 on page 17; specifically, property (3.1). In particular, note the parenthetical remark - "(In Convention II.2.6 and from then on we assume that Exercise 3.11 rather than Definition 3.8 has been used to define $\varphi_{e,s}$ and $W_{e,s}$" so (3.3) holds for $W_{e,s}$)" - inside that very exercise!
It's not hard to show that this is "benign" (or "without loss of generality," but that doesn't seem totally accurate) in the following precise sense (compare with the "hat trick" used when priority arguments are introduced): taking $(\varphi_i)_{i\in\mathbb{N}}$ to be the usual effective enumeration of partial computable functions, there is a computable total function $f(x,y,z)$ such that
$f$ has range $\{0,1\}$ and is nondecreasing.
For each $e$ and $n$, we have $n\in dom(\varphi_e)$ iff for some (equiv., for all sufficiently large) $s$ we have $f(e,n,s)=1$.
$f(e,n,k)=0$ whenever $n\ge k$.
We could now think of "$n\in W_{e,s}$" as being slang for "$f(e,n,s)=1$," and we could think of the $W_e$s as representing "nice" r.e. sets. The construction/verification of $f$ as above lets us easily prove a "conversion" result, saying that simplicity in this limited sense is equivalent to actual simplicity; that is, restricting attention to enumerations satisfying the convention above doesn't affect anything.