Relation between $\eta$ and $\omega^L_1$

Question

I posted this question on MSE (link: Eventual Writability (general)) about 10 days ago. The current version of this question is a highly abridged version of the one posted there. Let's write "accidentally writable" and "eventually writable" as AW and EW respectively. See definition-3.10 (page-8) here for the definitions. So we have the notions of: (i) AW-real (ii) Sup of AW-ordinal (iii) EW-real (iv) Sup of EW-ordinals. Let's simply use $AW$ and $EW$ to denote (i) and (iii) respectively. Let's use the symbols $\mathcal{A}$ and $\eta$ for the ordinals in (ii) and (iv) respectively.

Short Version:

Why can't we set a variable whose value stablizes to $\omega^L_1$ (never to be changed again). And, in that case, then why can't we set a variable whose value stablizes to $\eta$ itself?

Long Version:

For the rest of the post I use $\omega_1$ to mean $\omega^L_1$. For the rest of the question "code for $\alpha$" simply means "well-order of $\mathbb{N}$ (in suitably encoded form) with order-type $\alpha$". We assume the access to an onto function $f:Ord \rightarrow AW$. That is, we have a program which when given any arbitrary input $x$ will halt and return a real that belongs to $AW$. Essentially, $f(x)$ corresponds to the "$x$-th time" an AW-real appears on the output (for a program that enumerates all elements of $AW$).

This outline might make it easier to understand what I am trying to say (in what follows). $\eta$ must be countable. But let's try to analyze this in a bit of detail. Because we have $\mathcal{A}=\omega_1$ there exists a variable which eventually settles to a value $\omega_1$ (and never changes after that). Setting-up such a variable (let's call it $v$) in a program isn't difficult. Initially set $v:=\omega$. Then go through $range(f)$ while waiting for code of $\omega$ to appear. Once it appears the command $v:=v+1$ is triggered. But this is also true in general. If, at any point, we have $v$ equal to $\alpha<\omega_1$, then go through $range(f)$ while waiting for code of $\alpha$ to appear. Once again this triggers the command $v:=v+1$.

One thing in last paragraph is that the value of $v$ is only ever increased. And because we have $\mathcal{A}=\omega_1$, the value of $v$ should stabilize to $\omega_1$, never to change again. Now we want another variable (let's call it $u$), which we want to stabilize to $\eta$ (and never changing again). Let's try to see how we can do that.

Let's denote $O_e(t)$ to mean that output of program with index $e \in \mathbb{N}$ at a time $t \in Ord$. Note that because we are talking about a program that starts from blank state, we can talk about a natural number as an index. Suppose at some point we had $v:=V$. We want to calculate the value of $u$ corresponding to the given value of $v$. Roughly speaking, for any time, the variable $u$ tries to "guess" $\eta$ in a local sense based on the current value of $v$. First, we wish to calculate a subset of ordinals, say $X$.

For all indexes $e \in \mathbb{N}$ we check whether there exists a value $x<V$ such that for all $x \leq y \leq V$ we have $O_e(x)=O_e(y)$. In-case this happens to be true check $O_e(V)$. If it happens that this contains a code for ordinal, then that ordinal belongs to $X$. Once we repeat this process for all indexes (and not just $e$), we have the set $X$. We can set the value of $u$ as the smallest ordinal not in $X$. We can also set the output to contain a code for the current value of $u$.

Finally let's try to observe what happens when $v:=\omega_1$. We have a combination of programs that do and do not stabilize permanently (that is, not just in limit $\omega_1$ but in actuality). Based on what was mentioned by MCarl in comments below the answer (in the MSE version of the question), all programs that do stabilize happen to do so in countable time. This is an important observation (generally speaking too but more so in the context of the current question). Because that would mean that when $v:=\omega_1$ we will be able to set $u$ as some value $\geq \eta$. Based on what is mentioned in last paragraph, we can also set the output to contain a code for the current value of $u$.

Answer 1

Let me assume that you are concerned with ordinal time Turing machines, using a tape of order type Ord.

My first observation is that the accidentally writable reals are exactly the constructible reals.

Theorem. The OTM accidentally writable reals are exactly the constructible reals, that is, the reals in $\mathbb{R}^L$.

Proof. The forward inclusion holds because all the OTM computations can be undertaken inside $L$, and so whatever it is that appears on the tape at any moment for them will necessarily be in $L$. So every accidentally writable real is in $L$.

Conversely, we use the fact that the machines are able to simulate the constructibility hierarchy. With a suitable choice of finitely many ordinal parameters, the machines can construct a code for any desired level of the $L_\alpha$ hierarchy and pick out the code for any particular constructible set. In particular, with suitable parameters, one can produce any given constructible real on the tape. And now the point is that we can design a program that systematically does this for all possible choice of ordinal parameters. The universal algorithm will simply iteratively increase a master ordinal, interpreting it as a code for a finite tuple of ordinals, and carry out the construction that far. So every particular constructible real will appear on the tape during this universal procedure. $\Box$

In particular, the supremum of the OTM accidentally writable reals will be exactly $\omega_1^L$.

Meanwhile, there are only countably-in-$L$ many programs and therefore only countably many eventually writable reals, since each one can be associated with the program giving rise to it. So $\eta<\omega_1^L$.

The rest of your question appears to concern an algorithm that will in part somehow store the value of $\omega_1^L$. Let us discuss how this can be done. Since this is a machine model with only a tape and no registers to store the value in, let me assume that you intend to place a special mark at position $\omega_1^L$ on the tape, in such a way that you can recognized that it has been so marked. Let us say that position $\alpha$ on the tape is eventually markable if there is an algorithm that eventually places a $1$ at position $\alpha$, followed by a certain unique finite pattern of marks, which eventually does not appear anywhere else on the tape. If our tape allows a bigger alphabet, we could say more simply that $\alpha$ is eventually markable if there is an algorithm that (on empty input) eventually stabilizes with a red check mark on position $\alpha$ and no other red check marks. Or we can think of the special finite pattern as the red check mark.

Theorem. The ordinal $\omega_1^L$ is eventually markable.

Proof. The ordinal $\omega_1^L$ is the least ordinal that is never coded by any real in $L$. So we can simply search for an ordinal that will pass that test. We gradually consider ordinal positions in turn. For every ordinal, we temporarily place a red check mark at it, until we find a real coding it (this uses the count-through algorithm to count to the position coded by any relation coded with a real). When an ordinal is revealed as countable in this way, then we move on to the next ordinal, erasing the previous red mark and placing the next one. At limits of these stages, the head will be in a position at the supremum of the previous red marks. And so we will eventually place a red mark at $\omega_1^L$, never afterward to change it. So $\omega_1^L$ is eventually markable. $\Box$

The next part of your algorithm is to look at the eventually writable reals that stabilize in time $\omega_1^L$, by using simulations that proceed up to that red mark. This seems right to me. More generally:

Theorem. If $\alpha$ is eventually markable, then the supremum of the ordinals coded by reals that stabilize in time $\alpha$ is eventually writable.

Proof. Consider the program that eventually marks $\alpha$. At each stage, this algorithm is giving us a putative copy $\alpha_0$ of $\alpha$, which is eventually correct. For each $\alpha_0$ that appears during the computation, let us run a simulation of all programs on empty input, running them for $\alpha_0$ many steps. We can arrange to inspect this computation to see if the output had stabilized before $\alpha_0$, and in this way, we can compute a list of all the reals that are eventually-in-time-$\alpha_0$-writable. We can then check which code a well-order, and then write down a real coding the supremum of these ordinals. If at any moment, the red check mark changes, then we start completely over with the new $\alpha_0$. Eventually, $\alpha_0$ will be $\alpha$ itself, and we will stabilize on a real coding the supremum of the eventually-in-time-$\alpha$-writable ordinals, as desired. $\Box$

In particular, if we use $\alpha=\omega_1^L$, then we will eventually write a real coding the supremum of the ordinals coded by an eventually-in-time-$\omega_1^L$-writable real. It seems to me that ultimately, the algorithm you are proposing is writing down exactly the supremum of the eventually-in-time-$\omega_1^L$-writable ordinals, and this is strictly less than $\eta$.

In particular, it follows from what we've said so far that eventually writable reals do not stabilize in time $\omega_1^L$.

Corollary. Not all algorithms producing eventually writable reals stabilize in time $\omega_1^L$.

But actually, it is a bit easier to see that there are computations whose first $\omega$ cells eventually stabilize, but not by any stage before $\omega_1^L$. To see this, consider the algorithm that is eventually marking position $\omega_1^L$. Do not write on the first $\omega$ many cells, except when you change the red check mark, and then flash a $1$ and then $0$ on the first cell. This algorithm will eventually stabilize with its red check mark at position $\omega_1^L$, after which time it will no longer flash anything in the first $\omega$ cells. So this is an algorithm that writes an eventually writable real, but it does not stabilize before time $\omega_1^L$.