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:

- 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; - 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:

- 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;
- If $\alpha$ is a successor ordinal, the corresponding function is based on the fact that $\alpha$-th-order machines are equipped with particular oracles;
- 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.

justthe accidentally writable ordinals, but that doesn't seem to be a requirement in your question. $\endgroup$ – Wojowu Jan 11 at 7:04writablewith a fixed oracle. Just the index of an ITTM which halts with the desired output when ran with oracle $0^\blacktriangledown$. $\endgroup$ – Wojowu Jan 11 at 8:12