Googological Open Problems on OCFs

There are open problems on OCFs in googology.

1. Create an OCF which goes beyond UNOCF under the assumption that the ill-definedness of UNOCF is successfully resolved.
2. Create an OCF which goes beyond TSS (Trio Sequence System).
3. Create an OCF which goes beyond reflections.
4. Create an OCF which goes beyond TON.
5. Create ordinal notations associated to the OCFs used in googology.

I explain why they are important.

Beyond UNOCF

UNOCF is a well-known but ill-defined notation system, which is not an OCF at all. I conjecture that the creator did not know what an OCF actually means, and wrote down "expansion rules" immitating those for non-standard forms of ordinal notation systems associated to valid OCFs as if they were standard forms. That is why it is difficult to formalise UNOCF as an OCF.

Unfortunately, its definition is not formalised, and hence we can just argue on finitely many examples of "the desired expansion". Therefore the well-foundedness of UNOCF is not verified. It means that analyses based on UNOCF does not ensure that the target is actually well-defined.

Further, it is impossible for us to create an OCF such that it is formally provable to go beyond UNOCF. Then the precise aim should be to create an OCF such that googologists who believe that UNOCF works well can realise that it goes beyond UNOCF.

Suppose that you have created such an OCF. One powerful result is that UNOCF will turn out to be well-founded for googologists who believe that UNOCF works well. Of course, you do not have to care about UNOCF anymore, because you can use your OCF instead of UNOCF in analyses.

This open problem is not so easy as one might think first. Actually, there are many googologists who tried to formalise UNOCF as an OCF, an ordinal notation, or a notation system with a recursive system of fundamental sequences, but the mission has not been completed. As far as I know, the most successful trial is given by Nayuta Ito here. It formalises UNOCF as a notation system with a recursive system of fundamental sequences up to \(\psi_0(\Omega_{\omega})\) with respect to Buchholz's OCF.

Beyond TSS

TSS is a subsystem of BMS (Bashicu Matrix System) extending PSS (Pair Sequence System). The termination of TSS is not verified, while that of PSS is originally verified by me here in Japanese. In order to verify the termination of a given system, we usually need an OCF beyond it. For example, I used Buchholz's OCF in the proof of the terminiation of PSS.

Therefore in order to verify the termination of TSS, we need an OCF beyond TSS. Such an OCF is not known, and hence we need to create a new OCF for this purpose. I note that it is not sufficient to create just a strong OCF, because the difference of the systems of fundamental sequences causes heavy tiresome awful arguments on the order-preserving property of a given conversion from terms to ordinals. Actually, the reason why I costed much time in the proof is because I used Buchholz's OCF, whose system of fundamental sequences is completely different from that of PSS. I heard that PsiCubed2 also created another OCF which is useful to estimate PSS. Similarly, there might be a strong OCF which is useful to estimate TSS. (I note that if TSS is not well-founded, then such an OCF does not exists.)

Be careful that arguments on BMS often contain mistakes or misleadings. For example, Bubby3 often talks as if the termination of PSS could be easily verified when he states analysis on TSS, while he has never verified it. Ecl1psed276 often states that his notations, which have not been completely defined yet, go beyond subsystems of BMS as if they were obviously well-founded, while the well-foundedness is still open. Traditionally, "professional" googologists here often state something even if they actually do not understand notions appearing in their statements or assumptions. Therefore beginners need to be very careful when they hear statements by such "professional" googologists.

Beyond Reflections

There are OCFs collapsing large cardinals or large non-recursive ordinals. I guess that the strongest OCF ever defined is the one with reflections or stability by expert mathematicians (maybe Stegert, Rathjen, or Arai). Sorry if I am incorrect.

Creating a stronger actual OCF (not an ill-defined notation like UNOCF) is very important by the following reasons:

1. It can name all countable ordinals below a new large ordinal beyond the limit of existing OCFs without skipping. It helps us to analyse other googological systems.
2. If the \(\in\)-relation of such countable ordinals can be interpreted in a primitive recursive way, then it yields an ordinal notation. It helps us to create a new computable large number.

Concerning the first reason, "avoiding skipping" is very important for the purpose of analysis. For example, we can talk about the name "\(\textrm{PTO}(\textrm{ZFC})\)", but we do not have a recursive algorithm naming all ordinals below it. Concerning the second reason, the condition of the primitive interpretation is not easy to check.

For example, papers on OCFs spend half of their bodies for the argument on how to create an ordinal notation, i.e. a primitive recursive interpretation of the \(\in\)-relation. Therefore creating an OCF does not ensure that it automatically yields a computable large number. If I understand correctly, hyp cos tried to create OCFs with rich structures, but has not completely defined ordinal notations associated to them yet. Since hyp cos is one of the greatest googologists using OCFs, it implies how difficult creating ordinal notations associated to OCFs are. See also section for ordinal notations.

Beyond TON

In order to create an ordinal notation system, we usually need an OCF, because it is absolutely difficut to directly ensure the well-foundedness of the primitive recursive strict total ordering in general. For the difference of the terminology of an ordinal notation and an OCF, see this survey.

TON is one of very rare examples of an ordinal notation system created by a direct method without an OCF. Therefore the well-foundedness is only proved for subsystems, under large cardinal axioms. In order to ensure the well-foundedness of TON itself, we need an OCF which goes beyond the limit of TON. (I note that if TON is not well-founded, then such an OCF does not exists.)

Ordinal Notation

First of all, if you do not know what an ordinal notation means, see See also this article. Large numbers defined by FGH and OCFs are not necessarily computable. In order to ensure the computability, we need to construct ordinal notations associated to the OCFs. For example, many of large numbers in the higher computable googology defined by FGH and OCFs are expected to be computable but are not known to be computable, because there are no known explicit algorithm to compute them. Namely, we do not even know the computability of large numbers which are expected to be candidates of the highest computable googology. Therefore this is a serious issue in computable googology.