Corollary. Not all algorithms producing eventually writable reals stabilize in time $\omega_1^L$.
Corollary. Not all eventually writable reals stabilize in time $\omega_1^L$.
Corollary. Not all algorithms producing eventually writable reals stabilize in time $\omega_1^L$.
Let me assume that you are concerned with ordinal time Turing machines machines, using a tape of order type Ord.
My first observation is that the accidentally writable reals are exactly exactly the constructible reals.
Theorem. The OTM accidentally writable reals are exactly the constructible constructible reals, that is, the reals in $\mathbb{R}^L$.
Proof. The forward inclusion holds because all the OTM computations computations can be undertaken inside $L$, and so whatever it is that that appears on the tape at any moment for them will necessarily be in in $L$. So every accidentally writable real is in $L$.
Conversely, we use the fact that the machines are able to simulate the the constructibility hierarchy. With a suitable choice of finitely many many ordinal parameters, the machines can construct a code for any desired desired level of the $L_\alpha$ hierarchy and pick out the code for any any particular constructible set. In particular, with suitable parameters parameters, one can produce any given constructible real on the tape tape. And now the point is that we can design a program that systematically systematically does this for all possible choice of ordinal parameters parameters. The universal algorithm will simply iteratively increase increase a master ordinal, interpreting it as a code for a finite tuple tuple of ordinals, and carry out the construction that far. So every every particular constructible real will appear on the tape during this this universal procedure. $\Box$
In particular, the supremum of the OTM accidentally writable reals will will be exactly $\omega_1^L$.
Meanwhile, there are only countably-in-$L$ many programs and therefore therefore only countably many eventually writable reals, since each one one can be associated with the program giving rise to it. So $\eta<\omega_1^L$.
If I understand the thrust of theThe rest of your question, you are proposing appears to design andconcern an algorithm that will try 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 stabilizestore 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 $\eta$$\alpha$ on the tape is eventually markable if there is an algorithm that eventually places a $1$ at position $\alpha$, whichfollowed by a certain unique finite pattern of course would violatemarks, which eventually does not appear anywhere else on the definitiontape. 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 $\eta$$\omega_1^L$ is eventually markable. I believe that
Proof. The ordinal $\omega_1^L$ is the answerleast ordinal that is never coded by any real in $L$. So we can simply search for an ordinal that you are not paying attention to the factwill pass that test. We gradually consider ordinal positions in turn. For every ordinal, we are talking abouttemporarily place a red check mark at it, until we find a real codes for ordinalscoding 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, rather than ordinalsthen we move on to the next ordinal, erasing the previous red mark and placing the next one. At limit stageslimits of these stages, we perform the limit operationhead will be in a position at the supremum of the machines previous red marks. And so we will eventually place a red mark at $\omega_1^L$, whichnever afterward to change it. So $\omega_1^L$ is not eventually markable. $\Box$
The next part of your algorithm is to look at the same as takingeventually 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 of the ordinals coded by the reals. So when we try to that stabilize atin time $\eta$$\alpha$ is eventually writable.
Proof. Consider the program that eventually marks $\alpha$. At each stage, what happens insteadthis 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 certain limit stages whereany moment, the red check mark changes, then we become unbounded instart completely over with the new $\eta$$\alpha_0$. Eventually, $\alpha_0$ will be $\alpha$ itself, and we will stabilize on a real coding the limitsupremum of the codes is noteventually-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$ but some much smaller ordinal or is.
In particular, it follows from what we've said so far that eventually writable reals do not even coding an ordinal atstabilize in time $\omega_1^L$.
Corollary. Not all eventually writable reals stabilize in time $\omega_1^L$.
(Some of your remarks suggest But actually, it is a bit easier to see that youthere are thinking of a register machine modelcomputations whose first $\omega$ cells eventually stabilize, instead ofbut not by any stage before $\omega_1^L$. To see this, consider the tape modelalgorithm that is eventually marking position $\omega_1^L$. Do not write on the first $\omega$ many cells, whichexcept when you mention in part of your postchange the red check mark, and so I am not actually sure what you have in mindthen flash a $1$ and then $0$ on the first cell. This algorithm will eventually stabilize with some of your remarksits 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$.
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$.
If I understand the thrust of the rest of your question, you are proposing to design and algorithm that will try to stabilize on $\eta$, which of course would violate the definition of $\eta$. I believe that the answer is that you are not paying attention to the fact that we are talking about real codes for ordinals, rather than ordinals. At limit stages, we perform the limit operation of the machines, which is not the same as taking the supremum of the ordinals coded by the reals. So when we try to stabilize at $\eta$, what happens instead is that at certain limit stages where we become unbounded in $\eta$, the limit of the codes is not coding $\eta$ but some much smaller ordinal or is not even coding an ordinal at all.
(Some of your remarks suggest that you are thinking of a register machine model, instead of the tape model, which you mention in part of your post, and so I am not actually sure what you have in mind with some of your remarks.)
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 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$.
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$.
If I understand the thrust of the rest of your question, you are proposing to design and algorithm that will try to stabilize on $\eta$, which of course would violate the definition of $\eta$. I believe that the answer is that you are not paying attention to the fact that we are talking about real codes for ordinals, rather than ordinals. At limit stages, we perform the limit operation of the machines, which is not the same as taking the supremum of the ordinals coded by the reals. So when we try to stabilize at $\eta$, what happens instead is that at certain limit stages where we become unbounded in $\eta$, the limit of the codes is not coding $\eta$ but some much smaller ordinal or is not even coding an ordinal at all.
(Some of your remarks suggest that you are thinking of a register machine model, instead of the tape model, which you mention in part of your post, and so I am not actually sure what you have in mind with some of your remarks.)
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$.
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$.
If I understand the thrust of the rest of your question, you are proposing to design and algorithm that will try to stabilize on $\eta$, which of course would violate the definition of $\eta$. I believe that the answer is that you are not paying attention to the fact that we are talking about real codes for ordinals, rather than ordinals. At limit stages, we perform the limit operation of the machines, which is not the same as taking the supremum of the ordinals coded by the reals. So when we try to stabilize at $\eta$, what happens instead is that at certain limit stages where we become unbounded in $\eta$, the limit of the codes is not coding $\eta$ but some much smaller ordinal or is not even coding an ordinal at all.
(Some of your remarks suggest that you are thinking of a register machine model, instead of the tape model, which you mention in part of your post, and so I am not actually sure what you have in mind with some of your remarks.)
Loading