New Googological Ruler

There are several googological rulers such as Psi Level, which are helpful for beginners to understand their levels. On the other hand, I do not know a googological ruler which actually scales the level respecting restrictions such as computability. For example, it is much harder to create a computable large function beyond countable collapses of cardinals with respect to OCFs than to create an uncomputable large function beyond the busy beaver function. Therefore I would like to make a new googological ruler which scales not only the size but also restrictions.

Ruler

Here is the ruler. I will explain the precise meaning of this ruler later.

Level＼Regulation	Computable	Uncomputable I	Uncomputable II
\(0\)	ill-defined numbers	ill-defined numbers	ill-defined numbers
\(1\)	\(0 \sim 10^{100}\)	\(0 \sim\) "\(\textrm{Proof}(n,\perp)\)"	\(0 \sim\) Rayo's Number
\(2\)	\(\sim f_2(10^{100})\)	\(\sim \textrm{BusyBeaver}(10^{100})\)	\(\sim\) Fish number 7
\(3\)	\(\sim f_3(10^{100})\)	\(\sim \Sigma_2(10^{100})\)	\(\sim \textrm{Rayo}_{\textrm{MK}}(10^{100})\)
\(4\)	\(\sim f_{\omega}(10^{100})\)	\(\sim \Sigma_{10^{100}}(10^{100})\)	\(\sim \textrm{Rayo}_{\textrm{ZFC} + \textrm{I}0}(10^{100})\)
\(5\)	\(\sim f_{\omega + 2}(10^{100})\)	\(\sim f_{\omega_1^{\textrm{CK}}}(10^{100})\)
\(6\)	\(\sim f_{\omega \times 2}(10^{100})\)	\(\sim f_{\omega_{\omega}^{\textrm{CK}}}(10^{100})\)
\(7\)	\(\sim f_{\omega^2}(10^{100})\)	\(\sim \Sigma_{\infty}(10^{100})\)
\(8\)	\(\sim f_{\omega^{\omega}}(10^{100})\)	\(\sim\) "\(\aleph_n = \aleph\)"
\(9\)	\(\sim f_{\omega^{\omega^{\omega}}}(10^{100})\)	\(\sim \textrm{Rayo}_{\Sigma_1}(10^{100})\)
\(10\)	\(\sim f_{\varepsilon_0}(10^{100})\)	\(\sim \textrm{Rayo}_{\Sigma_{100}}(10^{100})\)
\(11\)	\(\sim f_{\varphi(\omega,0)}(10^{100})\)
\(12\)	\(\sim f_{\Gamma_0}(10^{100})\)
\(13\)	\(\sim f_{\psi_0(\Omega_2)}(10^{100})\)
\(14\)	\(\sim f_{\psi_0(\Omega_{\omega})}(10^{100})\)
\(15\)	\(\sim f_{\psi_0(\Omega_{\Omega})}(10^{100})\)
\(16\)	\(\sim f_{\psi_0(\Omega_{\Omega_{\Omega_{\cdot_{\cdot_{\cdot}}}}})}(10^{100})\)
\(17\)	\(\sim f_{\psi_{\Omega_1}(\psi_I(0))}(10^{100})\)
\(18\)	\(\sim f_{\psi_{\Omega_1}(I)}(10^{100})\)
\(19\)	\(\sim f_{\psi_{\Omega_1}(\Lambda_0)}(10^{100})\)
\(20\)	\(\sim f_{\psi_{\Omega_1}(\psi_{\chi_{\varepsilon_{M+1}}(0)}(0))}(10^{100})\)
\(21\)	\(\sim f_{\psi_{\Omega_1}^0(\varepsilon_{K+1})}(10^{100})\)
\(22\)	\(\sim f_{\textrm{ot}(T(\Xi),<)}(10^{100})\)
\(23\)	\(\sim f_{\textrm{ot}(T(\Upsilon),<)}(10^{100})\)
\(24\)	\(\sim\) The least transcendental integer
\(25\)	\(\sim f_{\textrm{PTO}(\textrm{ZFC})}(10^{100})\)

Aims

One aim is to provide googologists a possible choice of googological strategies to learn next. For example, if you can create a computable large number of level \(9\), then it is good for you to study \(\varepsilon_0\) in order to reach level \(10\). This ruler just focussing on how to go beyond the current level, therefore it does not mean there were no significant levels between \(9\) and \(10\). At least, I set the levels so that for each level, there seems to be at least one currently active googologist who is actually working on that level.

Another aim is to construct scaling for which googologists can determine the level of a given large number in an effective way based on classical analysis. For this purpose, it should be a well-defined scaling. When googologists create a new ruler which covers OCF levels, then they tend to include stuffs which are undefined or ill-defined such as unspecified extensions of BEAF, UNOCF, \(f_{\textrm{PTO}(\textrm{ZFC} + \textrm{I}0)}\), BIG FOOT, and Utter Oblivion, and stuffs which are not verified to be well-defined such as DAN, BM2.3, and \(q\)-function associated to Laver table. Instead, I defined the ruler only using well-defined large numbers.

Regulations

There are several regulations in googology. For example, I usually enjoy the following regulations:

1. Computable Googology
   1. Inline Large Number
   2. Elementary Large Number
   3. Large Number in \(\textrm{ZFC}\)
   4. Large Number in extensions of \(\textrm{ZFC}\)
2. Uncomputable Googology
   1. Large Function in \(\textrm{ZFC}\)
   2. Large Function in extensions of \(\textrm{ZFC}\)
   3. Other Regulations

In order to keep the googological ruler being simple, I deal only with 1-3, 2-1, and 2-2 this time, and call them "Computable", "Uncomputable I", and "Uncomputable II" respectively. I explain these three regulations in the following subsections.

Computable

This regulation allows computable large numbers in \(\textrm{ZFC}\) set theory. More precisely, it only allows large numbers defined in \(\textrm{ZFC}\) set theory as the values of computable functions whose computation rules are precisely described by the authors and whose inputs can be explicitly described as meta-theoretic natural numbers.

In the ruler, I only scale the sizes of computable large numbers.

For a positive integer \(i\), let \(a_i\) denote the uncomputable large number such that the string "\(\sim a_i\)" is written at level \(i\) in the ruler. Then the sequence \((a_1, a_2, \ldots)\) is perhaps strictly increasing. In order to ensure the well-definedness of the ruler, I technically declare that an \(n \in \mathbb{N}\) is classified as a large number of level \(i\) in the ruler if and only if \(i-1 + \sum_{k=1}^{i-1} a_k \leq n < i + \sum_{k=1}^{i} a_k\). Therefore strictly speaking, \(a_i\) itself might not be of level \(i\). If you do not mind the possibility that \((a_1,a_2,\ldots)\) fails to be strictly increasing, you can roughly interpret the definition into the alternative one that an \(n \in \mathbb{N}\) is classified as a large number of level \(i\) in the ruler if and only if \(a_{i-1} < n \leq a_i\).

Uncomputable I

This regulation allows uncomputable large numbers in \(\textrm{ZFC}\) set theory. More precisely, it only allows large numbers defined in \(\textrm{ZFC}\) set theory by explicit formulae formally written down by the authors.

In the ruler, I only scale the size of large numbers. Although the comparison of uncomputable large numbers itself can be independent of the axiom of \(\textrm{ZFC}\), it does not mean the ruler will be ill-defined. It just means that where to place a given uncomputable large number can be independent of \(\textrm{ZFC}\).

For a positive integer \(i\), let \(a_i\) denote the uncomputable large number such that the string "\(\sim a_i\)" is written at level \(i\) in the ruler. Please be careful that it does not mean that the sequence \((a_1, a_2, \ldots)\) is strictly increasing. I just intend a similar inequality to Computable.

Uncomputable II

This regulation allows uncomputable large numbers in extensions of \(\textrm{ZFC}\) set theory. More precisely, it only allows large numbers defined in extensions of \(\textrm{ZFC}\) set theory such that it is reasonable to believe their consistency by explicit formulae recursively defined by explicit formulae in the meta-theory formally written down by the authors.

In the ruler, I scale not only the size of large numbers but also the definability of the base theories. Since uncomputable large numbers defined in distinct base theories are not necessarily comparable to each other by the reason explained here, I will take the size into account only when the comparability is obvious.

As a result, the ruler becomes unfortunately informal. I just prepared this regulation in order to explain how lawless uncomputable googology beyond \(\textrm{ZFC}\) set theory is.

Conventions

I explain several notations in the ruler.

OCFs

The OCF \(\psi\) at level \(13 \sim 14\) is Buchholz's OCF, and the OCF \(\psi\) at level \(15 \sim 16\) is extended Buchholz's OCF.

The OCF \(\psi\) at level \(17 \sim 20\) is Rathjen's standard OCF based on a weakly Mahlo cardinal, and the OCF \(\psi\) at level \(21\) is Rathjen's standard OCF based on a weakly compact cardinal. The function \(\chi\) at level \(20\) is the Rathjen's ordinal function collapsing the rank of the weak inaccessibility of regular cardinals, and the cardinal \(\Lambda_0\) at level \(19\) is the singular cardinal \(\chi_{\chi_{\chi_{\cdot_{\cdot_{\cdot}}}(0)}(0)}(0) = \psi_{\chi_M(0)}(0)\). Although those functions are not definable in \(\textrm{ZFC}\) set theory under the assumption of its consistency, the resulting FGH makes sense in \(\textrm{ZFC}\) set theory by the reason partially explained here.

Ordinal Notations

The ordinal notations \((T(\Xi),<)\) and \((T(\Upsilon),<)\) at level \(22 \sim 23\) are Stegert's ordinal notations, and \(\textrm{ot}\) denotes the ordinal type.

Transcendental Integer System

I denote by \(\textrm{TransInt}(n)\) the computable function which assigns to each \(n \in \mathbb{N}\) the least natural number greater than or equal to the halting times of Turing machines with input \(0\) whose terminations admit formal proofs of length \(\leq n\) under the axiom of \(\textrm{ZFC}\). In particular, \(\textrm{TransInt}(2^{1000})\) is the least transcendental integer. The precise value depends on the way to formalise \(\textrm{ZFC}\) set theory, but the difference does not make significant variation of the growth rate restricted to the domain, which includes all meta-theoretic natural numbers. In order to specify the definition, I use the formalisation here (in Japanese).

The ordinal \(\textrm{PTO}(\textrm{ZFC})\) is the supremum of the ordinal types of all provably well-founded primitive recursive total orderings on \(\mathbb{N}\) under the axiom of \(\textrm{ZFC}\). As \(f_{\omega_1^{\textrm{CK}}}(n)\) with respect to a non-pathological system of fundamental sequences is expected to grow much faster than \(\textrm{BusyBeaver}(n)\), \(f_{\textrm{PTO}(\textrm{ZFC})}(n)\) is expected to grow much faster than \(\textrm{TransInt}(n)\). (I note that \(\textrm{BusyBeaver}(n)\) outgrows \(f_{\alpha}(n)\) for any \(\alpha < \omega_1^{\textrm{CK}}\) with respect to a recursive system of fundamental sequences, and hence is frequently identified with \(f_{\omega_1^{\textrm{CK}}}(n)\) by many googologists. Similarly, \(\textrm{TransInt}(n)\) outgrows \(f_{\alpha}(n)\) for any \(\alpha < \textrm{PTO}(\textrm{ZFC})\) with respect to a recursive system of fundamental systems whose basic properties can be provable, and hence might be identified with \(f_{\textrm{PTO}(\textrm{ZFC})}(n)\) by them. At least, I regard \(f_{\omega_1^{\textrm{CK}}}(n)\) and \(f_{\textrm{PTO}(\textrm{ZFC})}(n)\) as significant functions because they admit canonical computation structures based on notations of ordinals unlike \(\textrm{BusyBeaver}(n)\) and \(\textrm{TransInt}(n)\).)

FGH

For an ordinal \(\alpha\), \(f_{\alpha}\) denotes the FGH with respect to a certain reasonable choice of a system of fundamental sequences. In order to have the ruler strictly well-defined, the systems of fundamental sequences are given in the following way:

1. At level \(1 \sim 10\) in Computable, the recursive system of fundamental sequences is the standard one associated to Cantor normal form.
2. At level \(11 \sim 12\), the recursive system of fundamental sequences is given by the standard one associated to Veblen function.
3. At level \(13 \sim 14\), the recursive system of fundamental sequences is given by the standard one associated to Buchholz's ordinal notation \((OT,<)\).
4. At level \(15 \sim 16\), the recursive system of fundamental sequences is given by the standard one associated to extended Buchholz's OCF.
5. At level \(17 \sim 20\), the recursive system of fundamental sequences is given by the one defined by the length of the normal form expression in Rathjen's standard ordinal notation based on a weakly Mahlo cardinal.
6. At level \(21\), the recursive system of fundamental sequences is given by the one defined by the length of the normal form expression in Rathjen's standard ordinal notation based on a weakly compact cardinal.
7. At level \(22 \sim 23\), the recursive systems of fundamental sequences are given by the ones defined by the length of a term.
8. At level \(25\), the recursive system of fundamental sequences is the one defined here.
9. At level \(5\) in Uncomputable I, the non-recursive system of fundamental sequences is defined in the following way:
   1. Let \(\mathcal{O}\) denote Kleene's \(\mathcal{O}\) associated to the enumeration \((A_n)_{n \in \mathbb{N}}\) of code arrays, which is the Turing complete computation model introduced here defined in the following way:
      1. Let \((p_m)_{m \in \mathbb{N}}\) denote the sequence enumerating prime numbers.
      2. Let \(n \in \mathbb{N}\). Put \(m_n = \max \{m \in \mathbb{N} \mid p_m^{-1}(n+1) \in \mathbb{N}\}\). For each \(i \in \mathbb{N}\) smaller than \(m_n\), put \(e_{n,i} = \max \{d \in \mathbb{N} \mid p_i^{-d}(n+1) \in \mathbb{N}\}\) and \(A_{n,i} = ((\max \{d \in \mathbb{N} \mid p_{3k+j}^{-d} e_{n,i} \in \mathbb{N}\})_{j=0}^{2})_{k=0}^{2}\). Set \(A_n = (A_{n,i})_{i=0}^{m_n-1}\).
   2. Define a sequence \((a_m)_{m \in \mathbb{N}}\) in the following inductive way:
      1. If \(m = 0\), then \(a_m = 0\).
      2. If \(m > 0\), then \(a_m = \min \{a \in \mathbb{N} \mid a_{m-1} < a \land a_{m-1} <_{\mathcal{O}} a\}\).
   3. Let \([ \ ]_{\mathcal{O}}\) denote the operator assigning the fundamental sequence for a given notation in \(\mathcal{O}\).
   4. Let \(\alpha\) be an ordinal smaller than or equal to \(\omega_1^{\textrm{CK}}\).
   5. Let \(n \in \mathbb{N}\).
   6. If \(\alpha = 0\), then set \(\alpha[n] = 0\).
   7. If \(\alpha\) is a successor ordinal, then set \(\alpha[n] = \max \alpha\).
   8. If \(\alpha = \omega_1^{\textrm{CK}}\), then set \(\alpha[n] = \mathcal{O}(a_n)\).
   9. Suppose that \(\alpha\) is a non-zero limit ordinal smaller than \(\omega_1^{\textrm{CK}}\).
      1. Define an \((N_{\alpha,i})_{i=0}^{\infty}\) and a \((b_{\alpha,i})_{i=0}^{\infty}\) in the following inductive way:
         1. Suppose \(i = 0\).
            1. Put \(b_{\alpha,i} = \min \{m \in \mathbb{N} \mid \alpha \leq \omega_1^{\textrm{CK}}[m]\}\).
            2. Put \(N_{\alpha,i} = a_{b_{\alpha,i}}\).
         2. Suppose \(i > 0\).
            1. Suppose \(\alpha \in \mathcal{O}(N_{\alpha,i-1})\).
               1. Put \(b_{\alpha,i} = \min \{m \in \mathbb{N} \mid \alpha \leq \mathcal{O}(N_{\alpha,i})[m]\}\).
               2. Put \(N_{\alpha,i} = N_{\alpha,i-1}[b_{\alpha,i}]_{\mathcal{O}}\).
            2. Suppose \(\alpha \notin \mathcal{O}(N_{\alpha,i-1})\)
               1. Put \(b_{\alpha,i} = 0\).
               2. Put \(N_{\alpha,i} = 0\).
      2. Put \(\ell_{\alpha} = \min \{i \in \mathbb{N} \mid \mathcal{O}(N_{\alpha,i}) = \alpha\}\).
      3. Set \(\alpha[n] = \mathcal{O}(N_{\alpha,\ell_{\alpha}}[n]_{\mathcal{O}})\).
10. At level \(6\) in Uncomputable I, the non-recursive system of fundamental sequences is given by the standard one associated to the notation system given by replacing the enumerated set of total recursive functions in the construction of Kleene's \(\mathcal{O}\) by the set of maps \(\mathbb{N} \to \mathbb{N}\) in \(L_{\omega_{\omega}^{\textrm{CK}}}\) enumerated in the follwoing way:
    1. For an \(m \in \mathbb{N}\), define the notion of an \(m\)-th oracle code array and its enumeration \((A_{m,n})_{n \in \mathbb{B}}\) in the following way
       1. \(A_{m,n}\) is the pair of \(m\) and the \(n\)-th code array.
       2. If \(m = 0\), then the computation process of \(A_{m,n}\) is the same as the \(n\)-th code array.
       3. If \(m \neq 0\), then the computation process of \(A_{m,n}\) is the same as the \(n\)-th code array except that each code matrix \(M\) corresponds to the following computation step:
          1. Let \(n_0\) and \(x_0\) be the first and the second values respectively in the memory.
          2. If \(A_{m-1,n_0}\) halts with input \(x_0\), then denote by \(M'\) the code matrix obtained by replacing each entry \(e\) of \(M\) by \(\max \{d \in \mathbb{N} \mid 2^{-d}(e+1) \in \mathbb{N}\}\).
          3. If \(A_{m-1,n_0}\) does not halt with input \(x_0\), then denote by \(M'\) the code matrix obtained by replacing each entry \(e\) of \(M\) by \(\max \{d \in \mathbb{N} \mid 3^{-d}(e+1) \in \mathbb{N}\}\).
          4. Execute the computation step corresponding to \(M'\) with respect to the computation process for a code array.
    2. Let \(((M_n,I_n))_{n \in \mathbb{N}}\) denote the enumeration of \(\mathbb{N}^2\) given by the well-ordering \((m_0,i_0) \leq (m_1,i_1) \Leftrightarrow 2^{m_0}(2i_0+1) \leq 2^{m_1}(2i_1+1)\) of the ordinal type \(\omega\).
    3. Enumerate maps \(\mathbb{N} \to \mathbb{N}\) in \(L_{\omega_{\omega}^{\textrm{CK}}}\) by assigning to each \(n \in \mathbb{N}\) the map corresponding to \(A_{M_n,I_n}\).

If you are just interested in googological approximation which does not care about the variation of the growth rate due to the difference of reasonable system of fundamental sequences, then please use any reasonable systems of fundamental sequences which you prefer. The reasonability is intuitive, and not formalised in mathematics. For example, the fundamental sequence \(\omega[n] = \textrm{BusyBeaver}(n)\) is not reasonable because the associated FGH \(f_{\omega}(n)\) goes beyond \(\textrm{BusyBeaver}(n)\).

I note that FGH itself yields an uncomputable function whose imput is a pair \((\alpha,n)\) of a countable ordinal \(\alpha\) with a fixed system of fundamental sequences and a natural number \(n\). However, we can safely regard the segments of FGH appearing in Computable as computable large functions, because I use the recursive systems of fundamental sequences associated to those on the fixed ordinal notations, as I will explained above. Namely, all the segments of FGH appearing in Computable can be replaced by the FGH-like computable functions associated to ordinal notations equipped with recursive systems of fundamental sequences.

Least Proof of Contradiction

The natural number "\(\textrm{Proof}(n,\perp)\)" is defined as the unique \(n \in \mathbb{N}\) satisfying the following formula: \begin{eqnarray*} \forall X, (X = \{k \in \mathbb{N} \mid \textrm{Proof}(k,\ulcorner 0 = 1\urcorner)\}) \to ((X = \emptyset \to n = 0) \land (X \neq \emptyset \to n = \min_{k \in X} k)) \end{eqnarray*} Here, \(\textrm{Proof}(k,m)\) is the binary relation on \(\mathbb{N}\) defined as the sentence "\(k\) is the Goedel number of a formal proof in \(\textrm{ZFC}\) set theory of the formula whose Goedel number is \(m\)". In particular, \(\textrm{ZFC} + \textrm{Con}(\textrm{ZFC})\) implies that "\(\textrm{Proof}(n,\perp)\)" coincides with \(0\). It does not mean that "\(\textrm{Proof}(n,\perp)\)" coincides with \(0\) in \(\textrm{ZFC}\) set theory even if we assume its consistency. Since "\(\textrm{Proof}(n,\perp)\)" is computable by the oracle machine, it is easier to go beyond this constant than to go beyond large numbers defined by \(\textrm{BusyBeaver}\). On the other hand, it is difficult to go beyond this constant if one does not understand why it is well-defined. Namely, this gives an exercise to understand the axiom of comprehension, which does not explicitly appear in computable googology.

Busy Beaver Function

The function \(\textrm{BusyBeaver}(n)\) denotes the busy beaver function \(\Sigma(n)\). By the definition, it goes beyond any total computable function.

For an \(k \in \mathbb{N}\), the function \(\Sigma_k(n)\) denotes the \(k\)-th order busy beaver function, i.e. the function given by replacing Turing machines by \(k\)-th order oracle Turing machine. Here, the \(0\)-th order oracle Turing machine just means a Turing machine. For a \(k \in \mathbb{N}\), a \(k+1\)-st order oracle Turing machine is the computation model given by replacing the domain of the transition map in the definition of a Turing machine by a map with an additional boolean variable referring to whether the \(k\)-th order oracle Turing Machine which corresponds to the first variable in the tape with respect to the enumeration defined later with input \(0\) terminates or not. Each \(m \in \mathbb{N}\) corresponds to the \(1+m\)-th element in the set of \(k\)-th order oracle Turing machine in \(L\) with respect to the enumeration given by the canonical well-ordering of \(L\). If you are just interested in googological approximation which does not care about the variation of the growth rate due to the difference of reasonable enumerations of higher order oracle Turing machines, then please use any reasonable enumerations which you prefer.

Similarly, \(\Sigma_{\infty}(n)\) denotes the ITTM busy beaver function.

Aleph

The natural number "\(\aleph_n = \aleph\)" is defined as the unique \(n \in \mathbb{N}\) satisfying the following formula: \begin{eqnarray*} n = \sup \{x \in \mathbb{N} \mid \aleph_x = \aleph\} \end{eqnarray*} Namely, it is \(0\) if \(\aleph_{\omega} \leq \aleph\), and satisfies \(\aleph_n = \aleph\) otherwise. It is not necessarily large, but behaves randomly depending on models. Therefore it is very difficult to go beyond its value in \(V\) without naive reference to \(\aleph\) itself. At least, it is namable by the short formula above, it is smaller than Rayo's number.

Rayo's Function

I denote by \(\textrm{Rayo}(n)\) Rayo's function. Since Rayo's function is not definable in \(\textrm{ZFC}\) set theory, it appears in Uncomputable II.

For a \(k \in \mathbb{N}\), \(\textrm{Rayo}_{\Sigma_k}(n)\) denotes the computable large function given by replacing the truth predicate \(\textrm{Sat}\) in the definition of \(\textrm{Rayo}(n)\) by Levy's truth predicate on \(\Sigma_k\)-formulae, which is definable in \(\textrm{ZFC}\) set theory. Therefore it appears in Uncomputable I. I note that for the case \(k = 0\), the predicate is given by the usual satisfaction, and hence includes the halting problem. The truth predicate itself is a \(\Sigma_k\)-formula, and hence it is very difficult to explicitly write down the formula for the case where \(k\) is not so small, say \(k > 100\). Since I restricted Uncomputable I to the regulation in which we are only allowed to write down explicit defining formula, displaying a meta-theoretic recursion to define a formula in the base theory is not allowed. That is why I used \(\textrm{Rayo}_{\Sigma_{100}}(n)\) instead of \(\textrm{Rayo}_{\Sigma_{10^{100}}}(n)\) in order to be fair.

The natural number \(\textrm{Rayo}_{\textrm{MK}}(10^{100})\) is the uncomputable large number in \(\textrm{MK}\) set theory without sorts given by replacing the truth predicate \(\textrm{Sat}\) in the definition of \(\textrm{Rayo}(10^{100})\) by the truth predicate for \(\Sigma_{10^{100}}\)-formulae. Since it is defined in \(\textrm{MK}\) set theory, which is an extension of \(\textrm{ZFC}\) set theory, it appears in Uncomputable II. Formulae in \(\textrm{ZFC}\) set theory corresponds to a formulae in \(\textrm{MK}\)-set theory in which all quantifiers are bounded by \(V\), which are \(\Sigma_2\)-formulae because \(V\) is defined by the \(\Pi_1\)-formula \(\forall x, \forall y, (x \in y \to x \in V)\). In particular, the truth predicate for \(\Sigma_{10^{100}}\)-formulae is applicable to any formulae in \(\textrm{ZFC}\) set theory. Although it is essentially impossible to explicitly write down the formula of the truth predicate for \(\Sigma_{10^{100}}\)-formulae, it is definable in the meta-theoretic recursion, which is allowed in Uncomputable II. I note that \(\textrm{Rayo}_{\textrm{MK}}(10^{100})\) is not defined as a value of some function \(\textrm{Rayo}_{\textrm{MK}}(n)\), because the correspondence assigning to each \(n \in \mathbb{N}\) the truth predicate for \(\Sigma_n\)-formulae is just given in the meta-theory and is not formalisable in the base theory.

The function \(\textrm{Rayo}_{\textrm{ZFC} + \textrm{I}0}(10^{100})\) is the uncomputable function in \(\textrm{ZFC}\) set theory with constant terms \(\alpha_0,\alpha_1,\ldots\) augmented by the axiom \(\textrm{I}0\) of the existence of rank-into-rank cardinal and the axiom schema \((\exists x_0, \varphi) \to (\forall x_0, (\varphi \to x_0 = \alpha_{\ulcorner \varphi \urcorner}))\) indexed by formulae \(\varphi\) of length \(\leq 10^{100}\) without constant terms given by replacing the truth predicate \(\textrm{Sat}\) in the definition of \(\textrm{Rayo}(10^{100})\) by the alternative predicate obtained by connecting all formulae of the form \(\varphi \to (x_0 = \ulcorner \varphi \urcorner)\) by \(\land\), where \(x_0\) is a variable of a natural number and \(\varphi\) runs through all formulae of length \(\leq 10^{100}\) in which any variable term belongs to \(\{x_0,x_1,\ldots,x_{10^{100}}\}\) and any constant term is of the form \(\alpha_{\ulcorner \varphi \urcorner}\) for some formula \(\varphi\) of length \(\leq 10^{100}\). Since it is defined in that extension of \(\textrm{ZFC}\) set theory, it appears in Uncomputable II. It is not a truth predicate any more, but plays a similar role when we only consider such formulae \(\varphi\). By the same reason as \(\textrm{Rayo}_{\textrm{MK}}(10^{100})\), \(\textrm{Rayo}_{\textrm{ZFC} + \textrm{I}0}(10^{100})\) is not defined as a value of some function \(\textrm{Rayo}_{\textrm{ZFC} + \textrm{I}0}(n)\). I do not have a significant reason why I assumed \(\textrm{I}0\), because for any defining formula \(\varphi(x_0)\) in \(\textrm{ZFC}\) set theory augmented by \(\textrm{I}0\), \((\textrm{I}0 \to \varphi(x_0)) \land (\neg \textrm{I}0 \to x_0 = 0)\) is also a defining formula in \(\textrm{ZFC}\) set theory. I chose it only because it looks strong.

Examples

I show the levels of famous named large numbers. I do not know all of their precise values, and hence just referred to the descriotions in this wiki. Therefore the following might be wrong. I appreciate any corrections and suggestions.

Large Number in Computable	Level
Meameamealokkapoowa oompa	\(0\)
フラン数第四形態改二	\(1\)
Googol	\(1\)
Tritri	\(3\)
Graham's number	\(5\)
Fish number 1	\(8\)
Fish number 2	\(8\)
Threegold	\(8\)
Fish number 3	\(9\)
\(\textrm{Worm}(100)\)	\(10\)
Primitive sequence number	\(11\)
Fish number 5	\(11\)
フラン数第四形態改三	\(11\)
Fish number 6	\(11\)
TREE(3)	Unknown (\(13 \sim 14\)?)
SCG(13)	Unknown (\(14 \sim 15\)?)
Pair sequence number	\(15\)
Laver table	Unknown (\(0\) or \(5 \sim\)?)
Bashicu matrix number	Unknown (\(0\) or \(21 \sim 24\)?)
Loader's number	Unknown (\(15 \sim 24\)?)
Tarintar	Unknown (\(0\) or \(18 \sim 24\)?)
The least transcendental integer	\(25\)

Large Number in Uncomputable I	Level
\(\textrm{BusyBeaver}(10^{100})\)	\(2\)
\(\Xi(10^6)\)	Unknown (\(4 \sim 5\)?)
Fish number 4	\(5\)

Large Number in Uncomputable II	Level
Croutonillion	\(0\)
Sam's Number	\(0\)
BIG FOOT	\(0\)
Little Bigeddon	\(0\)
Sasquatch	\(0\)
Utter Oblivion	\(0\)
Rayo's Number	\(1\)
Fish number 7	\(2\)