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$.

  • 2
    $\begingroup$ Your question is much too long and rambling. Can you edit to focus it on the main point? $\endgroup$ Nov 1 '19 at 20:58
  • $\begingroup$ You already answered part-(A) in first-half of your answer (meaning its answer should be in positive given your answer). Whatever is under the heading part-(B) specifically, it isn't that long I think (about 700 words or so). $\endgroup$
    – SSequence
    Nov 1 '19 at 23:33
  • $\begingroup$ @JoelDavidHamkins To add some further clarity, I think I will edit the question (most likely within a day) and upload a document which illustrates the basic structure of what I wrote under the heading (B) (that is, using informal program-like language). This should only be 20--30 lines or so and would make, what I wrote, easier to follow. In particular, it would be easier to follow that the behaviour of $u$ and output cells (due to alterations) on limits shouldn't matter. $\endgroup$
    – SSequence
    Nov 2 '19 at 5:46
  • 2
    $\begingroup$ Your question will get a much better reception if you edit it, severely, for length. Currently, the post is a confusing mess. You've got part (A), then long part (A), part (B), etc., and in the middle of part (B), you say you've come to your "main question" and make a statement in bold type, but this is not even a question. I stopped reading part way through and just tried to guess what you were asking. Less is more. $\endgroup$ Nov 2 '19 at 13:44
  • 1
    $\begingroup$ Thanks for your edits, which have improved the question. I have posted an updated answer, which I think gets at the issue you want. $\endgroup$ Nov 3 '19 at 9:26

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$.

  • $\begingroup$ Thanks, I have taken a brief look only, but this seems quite related to the question. One brief question before I take a detailed look. Are you saying that the comment (on MSE): "OK, so you are asking for the supremum of what is usually called the "stabilization times". All stabilization times are countable and in fact, their supremum is again $\eta$" has a mistake? [you can find it just below the answer given on MSE thread] $\endgroup$
    – SSequence
    Nov 3 '19 at 9:56
  • $\begingroup$ Because that would go against what you have written: "In particular, it follows from what we've said so far that eventually writable reals do not stabilize in time $\omega^L_1$." $\endgroup$
    – SSequence
    Nov 3 '19 at 10:00
  • 1
    $\begingroup$ The supremum of the stabilization times, it seems to me, must be the first 2-stable ordinal, the first ordinal $\alpha$ with $L_\alpha\prec_{\Sigma_2} L$. If my thinking is correct, this is uncountable in $L$, precisely because $\omega_1^L$ is the least ordinal not seen as countable in $L$, which is a $\forall\exists$ property. This is a much stronger property than that mentioned by Merlin Carl, namely, merely of having the right $\forall\exists$ theory. $\endgroup$ Nov 3 '19 at 22:51
  • 2
    $\begingroup$ It will be much larger than $\aleph_\omega^L$, since the existence of each $\aleph_n^L$ is $\exists\forall$ expressible: "there exists a finite sequence of $n$ limit ordinals, such that there is no function collapsing one of them to the previous." And yes, it will be admissible for similar reasons. $\endgroup$ Nov 3 '19 at 23:03
  • 1
    $\begingroup$ @SSequence More generally, using a class of ordinals $S$ as an oracle, the writable reals are the ones in $Δ_{1,S}^{L[S]}$, the eventually writable reals are the ones in $Δ_{2,S}^{L[S]}$, and the accidentally writable reals are the ones in $L[S]$. (Also, in place of reals, one can use sets of ordinals if the formula complexity is for equality rather than membership.) If $S=∅$, the supremum of stabilization times for eventually writable reals is the least $L$-cardinal $δ$ such that $L_δ$ has the right $Σ_2^L$ theory. This is a large $L$-cardinal, but below the least $δ$ with $L_δ ≺_{Σ_2} L$. $\endgroup$ Nov 12 '19 at 18:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.