This is a summary of my Japanese blog post, in which I created a computable large function \(\textrm{LIM}(n)\). **It must be the fastest well-defined computable function which you have ever seen.**

If you are working in \(\textrm{ZFC}\) set theory, my system yields a computable large function corresponding to \(\textrm{PTO}(\textrm{ZFC})\) through FGH. If you are working in a stronger set theory, my system yields a computable large function corresponding to the PTO of that theory.

I note that my original blog post is much longer than this blog post, because...

- I wrote the full definition in terms of explicit expansion rules of nested arrays without using complicated mathematical stuffs.
- I wrote the full proof of the well-definedness of the resulting large number.

I only explain the essence of the construction in terms of usual mathematics without overlapping the proof.

## Preparation

I fixed explicit Goedel numberings of Turing machines and nested arrays. To be more precise, I introduced a Turing complete computation model called **code array** using arrays of \(3 \times 2\) matrices with coefficients in \(\mathbb{N}\), and hence enumerating nested arrays automatically yields Goedel numbering of code arrays. I interpreted many notions in proof theory (e.g. axioms, formal proofs, termination, etc.) into specific properties of nested arrays.

## Notation System

I call a triad of a code array, a natural number, and a code array a **decreasing sequence array**. I call an array of decreasing sequence array an **ordinal array**. I fix an explicit sequence \(a_{\omega}^{0}, a_{\omega}^{1}, a_{\omega}^{2}, \ldots\) of decreasing sequence, and dealt with the ordinal array \((a_{\omega}^{k})\) as a counterpart of each natural number \(k\). The concrete expression of the sequence itself does not matter heavily here. I only use the property that the second entr of \(a_{\omega}^{k}\) is \(k\) for any natural number \(k\).

Let \(T\) denote the set theory in which we are working in. For almost all googologists, \(T\) would be \(\textrm{ZFC}\) set theory.

For an ordinal array \(A\) and a natural number \(n\), I define a new ordinal array \(A[n]\) in the following recursive way:

- Denote by \(L\) the length of \(A\).
- If \(L = 0\), then \(A[n] := A\).
- Suppose \(L > 0\).
- Put \(A = (A_0,\ldots,A_{L-1})\) and \(A_{L-1} = (\Theta,k,\Phi)\).
- For each natural number \(i\) smaller than or equal to \(n\), define a natural number \(b_i\) in the following recursive way:
- Suppose \(i = 0\).
- If \(A_{L-1} \neq a_{\omega}^{k}\), then \(b_i := 0\)
- If \(A_{L-1} = a_{\omega}^{k}\), then \(b_i := 1\)

- Suppose \(i > 0\).
- If \(b_{i-1} > 0\), then \(b_i := b_{i-1}\).
- Suppose \(b_{i-1} = 0\).
- If \(i\) is the Goedel number of a formal proof in \(T\) of the statement "The domains of \(\Theta\) and \(\Phi\) contain \(\mathbb{N}^2\), the restriction of \(\Theta\) to \(\mathbb{N}^2\) defines a well-order \(R\) on \(\mathbb{N}\), and the restriction of \(\Phi\) to \(\mathbb{N}^2\) satisfies the following properties", then \(b_i = i\):
- For any \((a,n) \in \mathbb{N}^2\), the relation \(\Phi(a,n) R a\) holds.
- For any \((a,n) \in \mathbb{N}^2\), if \(\Phi(a,n) = a\), then for any \(b \in \mathbb{N}\), the relation \(a R b\) holds.

- Otherwise, \(b_i = 0\).

- If \(i\) is the Goedel number of a formal proof in \(T\) of the statement "The domains of \(\Theta\) and \(\Phi\) contain \(\mathbb{N}^2\), the restriction of \(\Theta\) to \(\mathbb{N}^2\) defines a well-order \(R\) on \(\mathbb{N}\), and the restriction of \(\Phi\) to \(\mathbb{N}^2\) satisfies the following properties", then \(b_i = i\):

- Suppose \(i = 0\).
- If \(b_n = 0\), then \(A[n] := (A_0,\ldots,A_{L-2},a_{\omega}^{n})\).
- Suppose \(b_n > 0\).
- Put \(k' := \Phi(k,n)\).
- Suppose \(k' = k\).
- If \(A_{L-1} = a_{\omega}^{k}\), then \(A[n] := (A_0,\ldots,A_{L-2})\).
- If \(A_{L-1} \neq a_{\omega}^{k}\), then \(A[n] := (A_0,\ldots,A_{L-2},a_{\omega}^{n})\).

- If \(k' \neq k\), then \(A[n] := (A_0,\ldots,A_{L-2},(\Theta,k',\Phi))\).

Although I only dealt with the case where \(T\) is \(\textrm{ZFC}\) set theory in my original blog post, you can consider the case where \(T\) is any effectively axiomisable set theory which you are working in.

For each natural number \(n\), I define an ordinal array \(A_{\textrm{Lim}}^{n}\) in the following recursive way:

- If \(n = 0\), then \(A_{\textrm{Lim}}^{n} := ()\).
- Suppose \(n > 0\).
- Denote by \(L\) the length of \(A\).
- Put \(A_{\textrm{Lim}}^{n-1} = (A_0,\ldots,A_{L-1})\).
- If \(n\) is not the Goedel number of a decreasing array, then \(A_{\textrm{Lim}}^{n} := (A_0,\ldots,A_{L-1},a_{\omega}^{n})\).
- If \(n\) is the Goedel number of a decreasing array \(a\), then \(A_{\textrm{Lim}}^{n} := (A_0,\ldots,A_{L-1},a)\).

An ordinal array \(A\) is said to be **standard** if there is a finite array \((n_0,n_1,\ldots,n_L)\) of natural numbers of length \(> 0\) satisfying \(A = A_{\textrm{Lim}}^{n_0}[n_1]\cdots[n_L]\). Then the set \(\mathcal{A}\) of standard ordinal arrays forms a notation system equipped with a natural bijective map \(O\) to \(\textrm{PTO}(T)\). Since I used \(O\) only in proofs, I omit its definition.

I emphasise that this is not an ordinal notation system in the usual sense. Well, I need to clarify that this "usual" means "usual in mathematics" but not "usual in this wiki". In mathematics, an ordinal notation system means a recursive set equipped with a primitive recursive well-ordering. Since I have not constructed a primitive recursive interpretation of \(O\), \(\mathcal{A}\) does not form an ordinal notation system at all. The reason why I needed to clarify the meaning is because many googologists here use the wrong terminology of "ordinal notation". They often refer to their original expression of ordinals (without primitive recursive interpretation of the corresponding well-ordering) by calling them "new ordinal notations".

## FGH

For an ordinal array \(A\), I define a computable function \(f_A(n)\) in the following recursive way:

- If \(A = ()\), then \(f_A(n) := n+1\).
- If \(A \neq ()\), then \(f_A(n) := f_{A[n]}^{n}(n)\).

It is a pointwise well-defined computable function, but is not necessarily provably total. I define the limit functions \(\textrm{Lim}(n)\) and \(\textrm{LIM}(n)\) in the following way:

- \(\textrm{Lim}(n) := f_{A_{\textrm{Lim}}^{n}}(n)\).
- \(\textrm{LIM}(n) := \textrm{Lim}^{n}(n)\).

Then they are also pointwise well-defined computable functions, and **\(\textrm{LIM}(n)\) must be the greatest among all well-defined large functions in \(T\) which you have ever seen.** Actually, \(\textrm{LIM}\) can be regarded as \(f_{\textrm{PTO}(T)+1}(n)\) with respect to a certain system of fundamental sequences on \(\mathcal{A}\) under a specific soundness of \(T\).

If I want to make \(T\) clearer, I denote \(\textrm{LIM}\) by \(\textrm{LIM}_T\). For example, the function \(\textrm{LIM}\) in the original description is \(\textrm{LIM}_{\textrm{ZFC}}\). I expect that \(\textrm{LIM}_{\textrm{ZFC}}(n)\) goes beyond the transcendental integer system \(\textrm{TR}(\textrm{ZFC},n)\), and \(\textrm{LIM}_{\textrm{ZFC}+\textrm{I}0}\) goes beyond \(\textrm{I}0\) function.

## Large Number

In particular, \(\textrm{LIM}(100 \uparrow^{100} 100)\) is a well-defined large number because \(100 \uparrow^{100} 100\) is a standard natural number, which must be the greatest among all well-defined large numbers in \(T\) which you have ever seen.

For example, I coined \(\textrm{LIM}_{\textrm{ZFC}}(100 \uparrow^{100} 100)\) in the original definition. A shorthand of the name of the number is **Large Number Residence Number**. As the name shows, it is a cousin of my uncomputable large number Large Number Garden Number. It is a well-defined large number in \(\textrm{ZFC}\), and its variant \(\textrm{LIM}_{\textrm{ZFC}+\textrm{I}0}(100 \uparrow^{100} 100)\) is a well-defined larger number in \(\textrm{ZFC}+\textrm{I}0\).

## External Links

- pdf-version of the original source translated by koteitan
- Code Array Simulator in jdoodle by 巨大数大好きbot
- 巨大数屋敷の大きさが知りたい by 高梨明日香 (A spreadsheet for syntax analysis of arrays in this notation)