Is it possible to construct a formal language that allows to refer to specific real numbers that encode ordinals accidentally writable by an ITTM?

Let $$A$$ denote a particular (fixed) algorithm to encode ordinals as real numbers. The exact technical description of $$A$$ is irrelevant for this question: it can be any algorithm that is mathematically correct.

All I want is to have a relatively simple (or as simple as possible) and unambiguous formal language $$L$$ that allows to refer to specific real numbers that encode (by the algorithm $$A$$) a specific ordinal $$\alpha$$, assuming that $$\alpha$$ can be any ordinal accidentally writable by an Infinite Time Turing Machine (ITTM).

I need to explain what I mean by the term “unambiguous formal language”. The language is unambiguous if it satisfies the following properties:

1. If we want to extract a real accidentally writable by an ITTM, it is required to specify a particular ordinal $$\beta$$ that denotes the stage at which the content of the output tape should be extracted;
2. If a machine $$m_i$$ halts, then there exists a particular ordinal $$\beta_1$$ which is clockable by $$m_i$$. And if we want to extract the ordinal writable by $$m_i$$ (that is, the content of the output tape after the halting transition), it is required to specify a particular ordinal $$\beta_2$$ which is expected to be clockable by $$m_i$$. But if the ordinal $$\beta_2$$ is not equal to $$\beta_1$$, then the formula outputs $$0$$ (an infinite sequence of zero bits) or we can simply assume that such formulas are not valid.

The reasoning here is that, given a natural number $$i$$, it is not enough (for me) to assume that if an $$i$$-th ITTM halts, then it halts at stage $$\beta$$ (where $$\beta$$ is some unknown abstract ordinal) and writes some real $$x$$. It’s ambiguous (for me) because if we don’t refer to a particular stage, then we assume that an ITTM halts at some unspecified stage. That is, we expect a program to halt, but we don’t point at a particular ordinal $$\beta$$ that denotes the stage when an ITTM is expected to halt! This situation seems unacceptable to me, and it is what I call “ambiguity” here (maybe the word “incompleteness” is more suitable).

Here is my understanding of how to start to approach the problem.

The first step relies on the fact that, given an index $$i$$ of any standard Turing machine, it is possible to assume that there exist a specific real that corresponds to $$i$$. For example, if an $$i$$-th machine does not halt given a natural number $$n$$ as the input, then the $$n$$-th bit of the corresponding real is $$0$$; if the machine halts, then the head will stop over a cell that contains a particular symbol $$b$$, so the $$n$$-th bit of the corresponding real is $$b$$.

Thus we can introduce the following family of terms in $$L$$:

$$g(i).$$

Here $$g$$ denotes the name of the function. The output of this function is a real number, and we can note that for any computable ordinal $$\alpha$$, there exists the corresponding natural number $$i$$ such that $$g(i)$$ encodes $$\alpha$$ (according to the algorithm $$A$$).

The second step is to assume that if I want to refer to a particular ordinal $$\alpha$$, then the formula in $$L$$ would contain the term $$f(n, x),$$

where $$f$$ denotes the name of the function, $$n$$ denotes the index of a corresponding ITTM and $$x$$ denotes a real number that encodes (by the algorithm $$A$$) some ordinal $$\beta$$ such that if we take a “snapshot” of the output tape at stage $$\beta$$, then the tape is expected to contain a real number that encodes $$\alpha$$ (by the algorithm $$A$$). That is, the output of the function $$f$$ is a real number that encodes (by the algorithm $$A$$) the accidentally writable ordinal $$\alpha$$. Obviously, it is possible that a real number on the output tape at stage $$\beta$$ does not encode any ordinal (according to the algorithm $$A$$); in this case, the output of the function $$f$$ is just a real number that lacks any “interesting” properties.

Maybe the next step is to define families of $$\alpha$$-th-order functions:

1. If $$\alpha$$ is $$0$$ (the least ordinal), the corresponding function is based on the fact that $$0$$-th-order machines are standard machines with no oracles;
2. If $$\alpha$$ is a successor ordinal, the corresponding function is based on the fact that $$\alpha$$-th-order machines are equipped with particular oracles;
3. If $$\alpha$$ is a limit ordinal, the corresponding function outputs the supremum of all ordinals that can be encoded by all $$\beta$$-th-order functions (where $$\beta$$ is any ordinal less than $$\alpha$$).

But I don’t know how to proceed from here.

Question: is it possible to construct a language $$L$$ such that if an ordinal $$\alpha$$ is accidentally writable by an Infinite Time Turing Machine, then there exists a finite formula in $$L$$ that corresponds to a specific real number encoding $$\alpha$$ (by the algorithm $$A$$)? If yes, I would want to see an example of such language.

• You can use the fact that accidentally writable reals are writable from $0^\blacktriangledown$. This won't give you just the accidentally writable ordinals, but that doesn't seem to be a requirement in your question. – Wojowu Jan 11 at 7:04
• @Wojowu: Yes, I thought about various oracles, but I will still need to refer to specific reals to denote a particular stage when the needed ordinal is written by a corresponding oracle ITTM. So the question stays the same. – lyrically wicked Jan 11 at 7:33
• You don't need to refer to a stage for reals writable with a fixed oracle. Just the index of an ITTM which halts with the desired output when ran with oracle $0^\blacktriangledown$. – Wojowu Jan 11 at 8:12
• I don't understand what you mean. Every (halting) ITTM has a unique halting time. I don't see how that would be in any way ambiguous. – Wojowu Jan 11 at 8:40
• Thank you for the clarification. The ordinals we can write in time $\omega$ are smaller $\omega_1^\mathrm{CK}$. But it turns out that this is also the bound for all ordinals writable in time strictly smaller than the CK ordinal are, again, smaller than the CK ordinal. Thus in that way we cannot recover ordinals larger than CK. That is, at least, without an oracle. I am unsure what we can do with $0^\blacktriangledown$ at this moment, but I think it might be possible to get all ordinals up to $\Sigma$. When I figure it out I will post an answer. – Wojowu Jan 12 at 10:00