ZFCのPTOの「証明論的類似」

この記事では\(\textrm{ZFC}\)集合論を用います。算術を含む帰納的公理系でも同様の議論が可能であることを注意しておきます。

それでは\(\textrm{ZFC}\)のPTOの「証明論的類似」を表す再帰的順序数表記を定義し、それに標準的な基本列を１つ定めます。

これでも大きい順序数を表現できていると思いますが、まだ満足していないです。今後も更新して、強めつつもサラダビリティを減らしていきます。

原文は英語の記事なため、少しずつ日本語に翻訳していきます。誰か解析して下さい。

Rough Sketch

I will define a map \(\textrm{RWO}\) sending an \((n,d) \in \mathbb{N} \times \mathbb{N}\) to (the Goedel number of) a formula \(\textrm{RWO}(n,d)\) in an internal set theory such that if there is a formula \(F\) satisfying the following two conditions with respect to the notion of the complexity of a formal proof defined later, then \(\textrm{RWO}(n,d)\) also satisfies them:

1. The statement that \(F\) is a definition of a recursive well-order on a recursive subset of \(\mathbb{N} \times \mathbb{N}\) admits a formal proof of complexity \(\leq d \).
2. For any \(m \in \mathbb{N}\) with \(m < n\), either one of the statement that the ordinal type of the well-order defined by \(F\) is smaller than that of \(\textrm{RWO}(m,d)\) and the statement that the ordinal type of the well-order defined by \(F\) is greater than that of \(\textrm{RWO}(m,d)\) admits a formal proof of complexity \(\leq d\).

Then \(\textrm{RWO}\) yields a recursive "整礎" strict partial order \(<_{\textrm{RWO}}\) on \(\mathbb{N} \times \mathbb{N}\), which admits a canonical system of fundamental sequences and a canonical subset of standard forms.

The "整礎" roughly means that there exists no infinite strictly decreasing sequence with respect to \(<_{\textrm{RWO}}\) starting from any pair \((n,d)\) of natural numbers presented by the repetition of successors eventually terminates. A reader might think that every natural number is presentable in that way, but it is not true. I will explain it later.

The second condition of \(\textrm{RWO}(n,d)\) is very important in this ordinal notation. Indeed, the construction would work even if I removed it, and the resulting ordinal notation would correspond to the PTO of \(\textrm{ZFC}\) by definition. Is it happy? No. The resulting order would become non-recursive, and hence I could not define computable large functions and computable large numbers. The second condition is given in a proof-theoretic way, and that is why I wrote that it corresponds to a "proof-theoretic analogue" of the PTO of \(\textrm{ZFC}\).

Preparation

For an \(n \in \mathbb{N}\), I denote by \(\textrm{Prj}_0(n) \in \mathbb{N}\) the greatest natural number with \(2^{\textrm{Prj}_0(n)} \mid n+1\), and by \(\textrm{Prj}_1(n) \in \mathbb{N}\) the natural number \(2^{-1}(2^{- \textrm{Prj}_0(n)}(n+1)-1)\). Then the pair function \begin{eqnarray*} \mathbb{N} & \to & \mathbb{N} \times \mathbb{N} \\ n & \mapsto & (\textrm{Prj}_0(n),\textrm{Prj}_1(n)) \end{eqnarray*} is a bijective map, whose inverse is the map \begin{eqnarray*} \mathbb{N} \times \mathbb{N} & \to & \mathbb{N} \\ (n_0,n_1) & \mapsto & 2^{n_0}(2n_1+1) - 1. \end{eqnarray*}

\(i \in \mathbb{N}\)に対し、\(\textrm{Prm}(i) \in \mathbb{N}\)で条件「任意の\(j \in \mathbb{N}\)に対し、\(j\)が\(i\)未満ならば\(\textrm{Prm}(j) < \textrm{Prm}(i)\)」を満たす最小の素数を表す。（これはいわゆる\(i+1\)番目の素数の原始再帰的定義である）

For a prime number \(p\), I denote by \(v_p \colon \mathbb{N} \setminus \{0\} \to \mathbb{N}\) the normalised additive \(p\)-adic valuation.

The map \begin{eqnarray*} \mathbb{N}^{\oplus \mathbb{N}} & \to & \mathbb{N} \setminus \{0\} \\ (e_i)_{i \in \mathbb{N}} & \mapsto & \prod_{i \in \mathbb{N}} \textrm{Prm}(i)^{e_i}. \end{eqnarray*} is a bijective map, whose inverse is the map \begin{eqnarray*} \mathbb{N} \setminus \{0\} & \to & \mathbb{N}^{\oplus \mathbb{N}} \\ n & \mapsto & (v_{\textrm{Prm}(i)}(n))_{i \in \mathbb{N}}, \end{eqnarray*} where \(\mathbb{N}^{\oplus \mathbb{N}}\) denotes \(\mathbb{N}^{\mathbb{N}} \cap \mathbb{Z}^{\oplus \mathbb{N}}\).

For an \(n \in \mathbb{N} \setminus \{0\}\), I denote by \(\textrm{Lng}(n) \in \mathbb{N}\) the smallest natural number with \(v_{\textrm{Prm}(j)}(n) = 0\) for any \(j \in \mathbb{N}\) with \(j < \textrm{Lng}(n)\).

Internal Formal Theory

For an \(i \in \mathbb{N}\), I put \begin{eqnarray*} x^L(i) := (0,i). \end{eqnarray*} Also, I put \begin{eqnarray*} \in^L & := & (1,0) \\ \to^L & := & (2,0) \\ \neg^L & := & (2,1) \\ \forall^L & := & (3,0). \end{eqnarray*} Then the set \(L := \{ x^L(i) \mid i \in \mathbb{N} \} \cup \{\in^L, \to^L, \neg^L, \forall^L \}\) forms a formal language of first order set theory such that \(x^L(i)\)'s are variable symbols, \(\in^L\) is a \(2\)-ary relation symbol, \(\to^L\) is the logical connective symbol for the implication, \(\neg^L\) is the logical connective symbol for the negation, and \(\forall^L\) is the symbol for the universal quantifier. I denote by \(A\) the \(\textrm{ZFC}\) axiom realised as a set of formulae in \(L\). I might use obvious syntax sugars in first order set theory, e.g. \(\wedge^L, \vee^L, \exists^L, \exists !^L, \notin^L, =^L, \neq^L, \subset^L, \cup^L, \times^L, (x,y)^L, \{x\}^L, \mathbb{N}^L, \omega^L, \ldots\).

I note that I defined \(=^L\) as a syntax sugar in a standard way, and hence the axiom of extensionality is replaced by the axiom scheme of equality corresponding to the logical axioms on equality. This is just a choice of convention, and hence you can use the usual equality, which is not a syntax sugar, if you prefer it.

For an \(n \in \mathbb{N}\), I denote by \(\textrm{Fml}^L(n)\) the formula in \(L\) given in the following recursive way: \begin{eqnarray*} \textrm{Fml}^L(n) := \left\{ \begin{array}{ll} x^L(\textrm{Prj}_0(\frac{n}{2})) \in^L x^L(\textrm{Prj}_1(\frac{n}{2})) & (n \in 2 \mathbb{N}) \\ \textrm{Fml}^L(\textrm{Prj}_0(\frac{n-1}{4})) \to^L \textrm{Fml}^L(\textrm{Prj}_1(\frac{n-1}{4})) & (n \in 4 \mathbb{N} + 1) \\ \neg^L \textrm{Fml}^L(\frac{n-3}{8}) & (n \in 8 \mathbb{N} + 3) \\ \forall^L x^L(\textrm{Prj}_0(\frac{n-7}{8})), \textrm{Fml}^L(\textrm{Prj}_1(\frac{n-7}{8})) & (n \in 8 \mathbb{N} + 7) \end{array} \right. \end{eqnarray*}

\(n \in \mathbb{N}\)に対し、\(\textrm{Prf}^L(n) \in \mathbb{N}\)で以下を満たす正整数\(N\)のうち最小のものを表す：

1. 任意の\(m \in \mathbb{N}\)に対し、\(m\)が\(n\)未満ならば\(\textrm{Prf}^L(m)\)は\(N\)未満である。
2. 有限列\((\textrm{Fml}^L(v_{\textrm{Prm}(i)}(N)))_{i < \textrm{Lng}(N)}\)は\(A\)の下での形式証明である。

自然数dに対して、Aの下でのPの形式的証明が複雑性≦dであるとは、その証明が自然数n≦dを用いてPrf^L(n)として表されることである。定義から、Aの下での複雑性≦dの証明は有限個しか存在しない。 \(d \in \mathbb{N}\)に対し、\(A\)の下での形式証明\(P\)が複雑性\(d\)以下であるとは、ある\(n \in \mathbb{N}\)が存在して\(n \leq d\)かつ\(P = \textrm{Prf}^L(n)\)であるということである。定義から、\(A\)の下での形式証明であって複雑性\(d\)以下であるものは有限個しか存在しない。

Ordinal Notation

\(\textrm{RWO}^L\)で「\(x^L(0)\)は\(\mathbb{N}^L \times^L \mathbb{N}^L\)の再帰的部分集合上の再帰的整列順序である」という\(L\)の論理式を表す。

I define a recursive partial order \(<_{\textrm{RWO}}\) on \(\mathbb{N} \times \mathbb{N}\) and a recursive subset \(\mathbb{N} \times \mathbb{N}\) consisting of terms of "standard form" to which the restriction of \(<_{\textrm{RWO}}\) is "整礎性" in the sense in Rough Sketch.

Enumeration of Provably Recursive Well-Orders

\((n,d) \in \mathbb{N} \times \mathbb{N}\)に対し、\(\textrm{RWO}(n,d) \in \mathbb{N}\)を以下のように再帰的に定める：

1. \(d > 0\)かつ\(\textrm{RWO}(n,d-1) \neq 0\)である時、\(\textrm{RWO}(n,d) = \textrm{RWO}(n,d-1)\)である。
2. 1の条件を満たさない時、もし以下の２条件を満たす\(N \in \mathbb{N}\)が存在するならば、\(\textrm{RWO}(n,d)\)はその２条件を満たす最小の自然数である：
   1. 論理式\(\exists !^L x^L(0), (\textrm{Fml}^L(N) \wedge^L \textrm{RWO}^L)\)の形式証明であって複雑性\(d\)以下のものが存在する。
   2. 任意の\(m \in \mathbb{N}\)に対し、もし\(m\)が\(n\)未満でありかつ\(\textrm{RWO}(m,d) \neq 0\)であるならば、以下のいずれかが成り立つ:
      1. 「論理式\(\textrm{Fml}^L(\textrm{RWO}(m,d))\)で定義される整列順序集合から論理式\(\textrm{Fml}^L(N)\)で定義される整列順序集合へ順序を保つ単射な非全射が存在する」という論理式の形式証明であって複雑性\(d\)以下のものが存在する。
      2. 「論理式\(\textrm{Fml}^L(N)\)で定義される整列順序集合から論理式\(\textrm{Fml}^L(\textrm{RWO}(m,d))\)で定義される整列順序集合へ順序を保つ単射な非全射が存在する」という論理式の形式証明であって複雑性\(d\)以下のものが存在する。
3. 1の条件も2の条件もいずれも満たさない時、\(\textrm{RWO}(n,d) = 0\)である。

\(d \in \mathbb{N}\)に対し、\(N(d) \in \mathbb{N}\)で\(\textrm{RWO}(N(d),d) = 0\)を満たす最小の自然数を表す。形式証明であって複雑性が\(d\)以下であるものは高々有限個しか存在しないため\(\textrm{RWO}(n,d) = 0\)を満たす\(n \in \mathbb{N}\)が存在し、従ってそのような\(n\)の最小値\(N(d)\)も存在する。

Strict Partial Orders

First, I define a binary relation \(<_{\textrm{RWO},d}\) on \(\mathbb{N} \times \{d\}\) for each \(d \in \mathbb{N}\).

Let \(n_0, n_1 \in \mathbb{N}\). For an \(n \in \mathbb{N}\), I abbreviate to \(\Phi(n_0,n_1,d;n)\) the statement that \((\textrm{Fml}^L(v_{\textrm{Prm}(i)}(n)))_{i < \textrm{Lng}(n)}\) is a formal proof of the existence of an order-preserving injective non-surjective map from the well-ordered set defined by \(\textrm{Fml}^L(\textrm{RWO}(n_0,d))\) to the one defined by \(\textrm{Fml}^L(\textrm{RWO}(n_1,d))\).

The relation \((n_0,d) <_{\textrm{RWO}} (n_1,d)\) is true if the following hold:

1. If \(n_1 < N(d)\), then the following hold:
   1. \(n_0 < N(d)\).
   2. There is an \(n \in \mathbb{N}\) with \(n \leq d\) such that \(\Phi(n_0,n_1,d;n)\) holds and \(\neg \Phi(n_1,n_0,d;m)\) holds for any \(m \in \mathbb{N}\) with \(m < n\).
2. If \(n_1 \geq N(d_1)\), then \(n_0 < n_1\).

Then \(<_{\textrm{RWO},d}\) forms a recursive strict well-order of ordinal type \(\omega\) by the definition of the computable function \(\textrm{RWO}\). I note that the latter condition on \(n\) in 1.2 can be removed if you assume \(\textrm{Con}(\textrm{ZFC})\) on the base theory.

Next, I define a binary relation \(<_{\textrm{RWO}}\) on \(\mathbb{N} \times \mathbb{N}\).

The relation \((n_0,d_0) <_{\textrm{RWO}} (n_1,d_1)\) is true if either one of the following hold:

1. If \(d_0 < d_1\), then \(n_0 < N(d_0)\) and either one of the following hold:
   1. \(n_0 = n_1\).
   2. \((n_0,d_1) <_{\textrm{RWO},d_1} (n_1,d_1)\).
2. If \(d_0 = d_1\), then \((n_0,d_0) <_{\textrm{RWO},d_1} (n_1,d_1)\).
3. If \(d_0 > d_1\), then \(n_1 < N(d_1)\) and \((n_0,d_0) <_{\textrm{RWO},d_0} (n_1,d_0)\).

Then \(<_{\textrm{RWO}}\) forms a recursive strict partial order, whose restriction to \(\mathbb{N} \times \{d\}\) coincides with \(<_{\textrm{RWO},d}\) for any \(d \in \mathbb{N}\).

Only the transitivity of \(<_{\textrm{RWO}}\) looks non-trivial, because of the limits of the complexity of formal proofs. A reader can immediately prove it, after reading back the definition of \(\textrm{RWO}\) again.

Standard Form

An \((n,d) \in \mathbb{N} \times \mathbb{N}\) is said to be of standard form if \(d\) is the smallest natural number such that \(\textrm{RWO}(n,d) \neq 0\). Then the set of pairs \((n,d)\) of standard form forms a recursive subset of \(\mathbb{N} \times \mathbb{N}\), and the restriction of \(<_{\textrm{RWO}}\) to it is a strict total order, which is an "well-order" in a natural sense.

I denote by \(\textrm{Std}(n,d) \in \mathbb{N} \times \mathbb{N}\) the unique pair of standard form whose first entry is \(n\).

Fundamental Sequence

For an \((n,d) \in \mathbb{N} \times \mathbb{N}\), I define a map \begin{eqnarray*} \mathbb{N} & \to & \mathbb{N} \times \mathbb{N} \\ s & \mapsto & (n,d)[s] \end{eqnarray*} in the following way:

1. If \(n < N(d)\), then the following hold:
   1. If \((n,d+s)\) is minimal in \(\mathbb{N} \times \{d+s\}\) with respect to \(<_{\textrm{RWO},d+s}\), then \((n,d)[s] = (n,d+s)\).
   2. Otherwise, \((n,d)[s]\) is the unique element of \(\mathbb{N} \times \{d+s\}\) whose successor is \((n,d+s)\) with respect to \(<_{\textrm{RWO},d+s}\).
2. If \(n \geq N(d)\), then the following hold:
   1. If \(n = N(d)\), the the following hold:
      1. If \(n = 0\), then \((n,d)[s] = (n,d)\).
      2. Otherwise, then \((n,d)[s]\) is the greatest element of \(N(d) \times \{d\}\), whose successor is \((n,d)\), with respect to \(<_{\textrm{RWO},d}\).
   2. Otherwise, then \((n,d)[s] = (n-1,d)\).

I note that this system of fundamental sequences is defined to any \((n,d)\) which does not necessarily correspond to a limit ordinal, and hence is not a fundamental sequence in the usual sense. If \((n,d)\) corresponds to a limit ordinal, then the sequence of ordinals corresponding to \((n,d)[s]\) converges to the ordinal corresponding to \((n,d)\). Otherwise, the successor of the ordinal corresponding to \((n,d)[s]\) coincides with the ordinal corresponding to \((n,d)\) or \((n,d+s)\).

If \((n,d)\) is of standard form, then the alternative sequence \(\textrm{Std}((n,d)[s])\) works as a system of fundamental sequences restricted to the subset of pairs of standard form, because \(\textrm{Std}((n,d)[s])\) is a pair of standard form which shares the corresponding ordinal with \((n,d)[s]\).

"整礎性"

In this section, I need to refer to the meta theory of the base theory. As I defined \(L\) and \(A\) in the base theory, the base theory is defined in the meta theory by using a formal language \(L^{\textrm{M}}\) and \(\textrm{ZFC}\) axiom \(A^{\textrm{M}}\) realised as a set of formulae in \(L^{\textrm{M}}\).

Here the meta theory is an arithmetic or another formal theory containing arithmetic whose axiom contains \(\textrm{Con}(A^{\textrm{M}})\). I note that assuming \(\textrm{Con}(A^{\textrm{M}})\) in the meta theory does not mean assuming \(\textrm{Con}(A)\) in the base theory. Both of \(A\) and \(A^{\textrm{M}}\) are \(\textrm{ZFC}\) axiom, and hence \(\textrm{Con}(A)\) is independent of \(A^{\textrm{M}}\) by the incompleteness theorem.

Although I have no proof of the 整礎性 of \(<_{\textrm{RWO}}\) under \(A^{\textrm{M}}\), I verify the 整礎性 on any \(\omega\)-model of \(A^{\textrm{M}}\). This is what I called the "整礎性" in Rough Sketch.

Meta Natural Number

A meta natural number is a natural number in the meta theory. Through the von Neumann construction, a meta natural number corresponds to a formula in \(L^{\textrm{M}}\) defining a natural number in the base theory. Namely, the meta natural number \(0\) corresponds to the formula \(\forall x_1, x_1 \notin x_0\) defining \(\ulcorner 0 \urcorner := \emptyset\), and the meta natural number \(n+1\) corresponds to the formula defining \(\ulcorner n+1 \urcorner := \ulcorner n \urcorner \cup \{\ulcorner n \urcorner\}\). Therefore every meta natural number is regarded as a natural number in the base theory in a harmless way.

Similarly, for a natural number \(n\) in the base theory, I denote by \(n^L\) the term in \(L\) defined under \(A\) by the formula corresponding to \(n\) through the von Neumann construction. I will demonstrate the computation of the formulae defining \(0^L\) and \(1^L\) later.

Is every natural number in the base theory a meta natural number? It is impossible to express the question as a formula in the base theory or the meta theory, and hence none can assume that every natural number is a meta natural number. Moreover, even if a formula on a natural number \(n\) in the base theory is provable for any meta natural number, the formula quantified by \(\forall n\) is not necessarily provable. So the non-existence of an infinite strictly decreasing chain starting from any meta natural number does not imply the 整礎性.

Now let \(n\) and \(d\) be meta natural numbers. If \(n \geq N(d)\), then any strictly decreasing sequence with respect to \(<_{\textrm{RWO}}\) starting from \((n,d)\) eventually lies in the locus of pairs of meta natural numbers corresponding to well-ordered sets. Therefore it is reduced to the case \(n < N(d)\). Then the formal proof of the 整礎性 of the recursive relation defined by \(\textrm{Fml}^L(\textrm{RWO}(n,d))\) under \(A\) actually gives a formal proof of the 整礎性 of the recursive relation defined by the corresponding formula \(\textrm{Fml}^{L^{\textrm{M}}}(\textrm{RWO}(n,d))\) in the base theory under \(A^{\textrm{M}}\).

Please be careful that the map \((n,d) \mapsto \textrm{Fml}^{L^{\textrm{M}}}(\textrm{RWO}(n,d))\) is just a term in the meta theory sending a pair of meta natural numbers to a formula in \(L^{\textrm{M}}\), and hence is not realised as a map in the base theory.

Realisation in the Base Theory

For each \((n,d) \in \mathbb{N}\) in the base theory, I denote by \(R(n,d)\) the binary relation of a subset of \(\mathbb{N} \times \mathbb{N}\) defined as the graph consisting of all pairs \(((n_0,d_0),(n_1,d_1)) \in \mathbb{N} \times \mathbb{N}\) such that the formula \begin{eqnarray*} \textrm{Fml}^L(\textrm{RWO}(n,d)) \to^L ((n_0^L,d_0^L)^L,(n_1^L,d_1^L)^L)^L \in^L x^L(0) \end{eqnarray*} is provable under \(A\).

If \(n < N(d)\), then the formula \(\textrm{Con}(A)\) in the base theory implies that \(R(n,d)\) forms a (possibly non-recursive) total order, because the well-order defined by \(\textrm{Fml}^L(\textrm{RWO}(n,d))\) is recursive, i.e. admits a finite string describing the computation process in the internal formal theory determining whether \((n_0^L,d_0^L)^L\) is greater than \((n_1^L,d_1^L)^L\) or not. I note that \(\textrm{Con}(A)\) is independent of \(A\) as long as we assume \(\textrm{Con}(A^{\textrm{M}})\) in the meta theory, and hence then the base theory admits a model which does not satisfy the statement that \(R(n,d)\) is a total order.

By the definition, if \(n\) and \(d\) are meta natural numbers with \(n < N(d)\), then on any model of \(A^{\textrm{M}} + \textrm{Con}(A)\), e.g. any \(\omega\)-model of \(A^{\textrm{M}}\), \(R(n,d)\) coincides with the binary relation defined by \(\textrm{Fml}^{L^{\textrm{M}}}(\textrm{RWO}(n,d))\), which is a recursive well-order on a recursive subset of \(\mathbb{N} \times \mathbb{N}\). Therefore the map \((n,d) \mapsto R(n,d)\) gives an appropriate realisation of the meta theoretic correspondence \((n,d) \mapsto \textrm{Fml}^{L^{\textrm{M}}}(\textrm{RWO}(n,d))\).

I denote by \(\alpha(n,d)\) the ordinal type of \(R(n,d)\) if it is a well-order, and \(0\) otherwise. By the argument above, if \(n\) and \(d\) are meta natural numbers with \(n < N(d)\), then on any model of \(A^{\textrm{M}} + \textrm{Con}(A)\), \(\alpha(n,d)\) is the ordinal type of the well-order defined by \(\textrm{Fml}^{L^{\textrm{M}}}(\textrm{RWO}(n,d))\). In this case, for any pairs \((n_0,d_0)\) and \((n_1,d_1)\) of meta natural numbers with \(n_0 < N(d_0)\) and \(n_1 < N(d_1)\), the relation \((n_0,d_0) <_{\textrm{RWO}}\) is equivalent to \(\alpha(n_0,d_0) \in \alpha(n_1,d_1)\) because a formal proof in \(L\) consisting of meta natural numbers is derived from a formal proof in \(L^{\textrm{M}}\).

Proof of the "整礎性"

Let \((M,\epsilon)\) be an \(\omega\)-model of \(A^{\textrm{M}}\). Then for any \((n_i,d_i)^{(M,\epsilon)}_{i \ \epsilon \ \mathbb{N}^{(M,\epsilon)}} \ \epsilon \ \mathbb{N}^{(M,\epsilon)} \times^{(M,\epsilon)} \mathbb{N}^{(M,\epsilon)}\), there is an \(i \epsilon \mathbb{N}^{(M,\epsilon)}\) such that \((n_{i+1},d_{i+1})^{(M,\epsilon)} <_{\textrm{RWO}}^{(M,\epsilon)} (n_i,d_i)^{(M,\epsilon)}\) is false by the 整礎性 of \(\alpha(n_0,d_0)^{(M,\epsilon)}\). It implies the 整礎性 of \(<_{\textrm{RWO}}^{(M,\epsilon)}\). This completes the proof of the "整礎性".

As a consequence, the 整礎性 of \(<_{\textrm{RWO}}\) is unprovable in the base theory if we assume on the meta theory the existence of an \(\omega\)-model of \(A^{\textrm{M}}\). I note that this assumption is strictly stronger than the original assumption of the meta theory, i.e. the consistency of \(A^{\textrm{M}}\).

FGH

For an \((n,d) \in \mathbb{N} \times \mathbb{N}\), putting \begin{eqnarray*} B(d) := 2 \uparrow^4 10^{100}(d+1), \end{eqnarray*} I define a computable function \(f_{(n,d)}(s)\) in the following recursive way:

1. If \((n,B(d))[s] = (n,B(d)+s)\), then \(f_{(n,d)}(s) = s+1\).
2. Otherwise, \(f_{(n,d)}(s) = f_{(n,B(d))[s]}^s(s)\).

The domain of \(f_{(n,d)}\) is \(\mathbb{N}\) as long as \(n\) and \(d\) are meta natural numbers, because the fundamental sequence of a pair of meta natural numbers consists of pairs of meta natural numbers. Otherwise, the domain of \(f_{(n,d)}\) might be empty. At least, the correspondence \((n,d,s) \mapsto f_{(n,d)}(s)\) is a well-defined partial function on \(\mathbb{N} \times \mathbb{N} \times \mathbb{N}\).

I note that it will be clear why I defined \(B(d)\) in this way when I demonstrate the estimation of \(N(d)\) later.

Large Number

I denote by \(f\) the computable partial function in the base theory defined as \(f(n) := f_{(n,2 \uparrow^4 n)}(n)\). It is not provably total, because the termination of the recursion process is just true on \(\omega\)-models of \(A^{\textrm{M}}\).

At least, \(10^{100}\) is a meta natural number, and the computable function \(f_{(n,d)}(s)\) sends a triad \((n,d,s)\) of meta natural number to a triad of meta natural numbers. Therefore \(f^{10^{100}}(10^{100})\) is a well-defined computable large number in \(\textrm{ZFC}\) set theory, as long as I assume the existence of an \(\omega\)-model of \(A^{\textrm{M}}\) on the meta theory.

Indeed, for any fixed triad \((n,d,s)\) of meta natural numbers, the computation process of \(f_{(n,d)}(s)\) does not depend on a model, and hence the termination of the computation of \(f_{(n,d)}(s)\) on an \(\omega\)-model implies the provability of the termination of the computation of \(f_{(n,d)}(s)\). Since the proof depends on the choice of \((n,d,s)\), it does not imply the provability of its quantification by \(\forall n, \forall d, \forall s\).

I emphasise that this additional assumption of the existence of an \(\omega\)-model of \(A^{\textrm{M}}\) is just given on the meta theory, but not on the base theory. The base theory is still \(\textrm{ZFC}\) set theory. In the usual mathematics, we usually assume such variants of the consistency of the base theory on the meta theory in order to avoid non-sense arguments with contradiction.

Demonstrations

I try to compute or estimate several values of the functions introduced above. The inequalities between functions below mean the eventual domination.

Estimation of Prm(n)

By \(n! \leq n^n \leq 2^{2^n} \leq 2 \uparrow^2 n\), it is easy to see \(\textrm{Prm}(n) < 2 \uparrow^3 n \). As a consequence, I give an upperbound of the concatenation of arrays of natural numbers. The map \begin{eqnarray*} \mathbb{N} \times \mathbb{N} & \to & \mathbb{N} \\ (n,m) & \mapsto & n \prod_{i \in \mathbb{N}} \textrm{Prm}(i + \textrm{Lng}(n) + 1)^{v_{\textrm{Prm}(i)}(m)} \end{eqnarray*} realising the concatenation is bounded by \(n \times \textrm{Prm}(n+m)\), and hence by \(2 \uparrow^3 2 \uparrow^3 (n+m)\). Since \(2 \uparrow^3 x\) is a convex function, the concarnation of \((n_0,\ldots,n_k)\) is bounded by \begin{eqnarray*} \underbrace{2 \uparrow^3 \cdots 2 \uparrow^3}_{2k} \sum_{i = 0}^{k} n_i. \end{eqnarray*}

Computation of Fml(n)

To begin with, I compute standard notations and several syntax sugars. I abbreviate \(\max \{n,m\}+1\) to \([n,m]\). \begin{eqnarray*} & & \textrm{Fml}^L(n) \to^L \textrm{Fml}^L(m) \\ & = & \textrm{Fml}^L(4(2^n(2m+1)-1)+1)\\ & = & \textrm{Fml}^L(2^{n+2}(2m+1)-3)\\ & & \\ & & \neg^L \textrm{Fml}^L(n) \\ & = & \textrm{Fml}^L(8n+3) \\ & & \\ & & \forall^L x^L(n), \textrm{Fml}^L(m) \\ & = & \textrm{Fml}^L(8(2^n(2m+1)-1)+7) \\ & = & \textrm{Fml}^L(2^{n+3}(2m+1)-1) \\ & & \\ & & x^L(n) \in^L x^L(m) \\ & = & \textrm{Fml}^L(2(2^n(2m+1)-1)) \\ & = & \textrm{Fml}^L(2^{n+1}(2m+1)-2) \\ & & \\ & & \textrm{Fml}^L(n) \vee^L \textrm{Fml}^L(m) \\ & := & (\neg^L \textrm{Fml}^L(n)) \to^L \textrm{Fml}^L(m) \\ & = & \textrm{Fml}^L(8n+3) \to^L \textrm{Fml}^L(m) \\ & = & \textrm{Fml}^L(2^{(8n+3)+2}(2m+1)-3) \\ & = & \textrm{Fml}^L(2^{8n+5}(2m+1)-3) \\ & & \\ & & \textrm{Fml}^L(n) \wedge^L \textrm{Fml}^L(m) \\ & := & \neg^L((\neg^L \textrm{Fml}^L(n)) \vee^L (\neg^L \textrm{Fml}^L(m))) \\ & = & \neg^L(\textrm{Fml}^L(8n+3) \vee^L \textrm{Fml}^L(8m+3)) \\ & = & \neg^L(\textrm{Fml}^L(2^{8(8n+3)+5}(2(8m+3)+1)-3)) \\ & = & \neg^L(\textrm{Fml}^L(2^{64n+29}(16m+7)-3)) \\ & = & \textrm{Fml}^L(8(2^{64n+29}(16m+7)-3)+3) \\ & = & \textrm{Fml}^L(2^{64n+32}(16m+7)-21) \\ & & \\ & & \textrm{Fml}^L(n) \leftrightarrow^L \textrm{Fml}^L(m) \\ & := & (\textrm{Fml}^L(n) \to^L \textrm{Fml}^L(m)) \wedge^L (\textrm{Fml}^L(m) \to^L \textrm{Fml}^L(n)) \\ & = & \textrm{Fml}^L(2^{n+2}(2m+1)-3) \wedge^L \textrm{Fml}^L(2^{m+2}(2n+1)-3) \\ & = & \textrm{Fml}^L(2^{64(2^{n+2}(2m+1)-3) + 32}(16(2^{m+2}(2n+1)-3)+7)-21) \\ & = & \textrm{Fml}^L(2^{2^{n+8}(2m+1)-160}(2^{m+6}(2n+1)-41)-21) \\ & & \\ & & \exists^L x^L(n), \textrm{Fml}^L(m) \\ & := & \neg^L(\forall^L x^L(n), \neg^L \textrm{Fml}^L(m)) \\ & = & \neg^L(\forall^L x^L(n), \textrm{Fml}^L(8m+3)) \\ & = & \neg^L(\textrm{Fml}^L(2^{n+3}(2(8m+3)+1)-1)) \\ & = & \neg^L(\textrm{Fml}^L(2^{n+3}(16m+7)-1)) \\ & = & \textrm{Fml}^L(8(2^{n+3}(16m+7)-1)+3) \\ & = & \textrm{Fml}^L(2^{n+6}(16m+7)-5) \\ & & \\ & & x^L(n) \notin^L x^L(m) \\ & := & \neg^L(x^L(n) \in^L x^L(m)) \\ & = & \neg^L \textrm{Fml}^L(2^{n+1}(2m+1)-2) \\ & = & \textrm{Fml}^L(8(2^{n+1}(2m+1)-2)+3) \\ & = & \textrm{Fml}^L(2^{n+4}(2m+1)-13) \\ & & \\ & & x^L(n) =^L x^L(m) \\ & := & \forall^L x^L([n,m]), (x^L([n,m]) \in^L x^L(n) \leftrightarrow^L x^L([n,m]) \in^L x^L(m)) \\ & = & \forall^L x^L([n,m]), (\textrm{Fml}^L(2^{[n,m]+1}(2n+1)-2) \leftrightarrow^L \textrm{Fml}^L(2^{[n,m]+1}(2m+1)-2)) \\ & = & \forall^L x^L([n,m]), (\textrm{Fml}^L(2^{[n,m]+1}(2n+1)-2) \leftrightarrow^L \textrm{Fml}^L(2^{[n,m]+1}(2m+1)-2)) \\ & = & \forall^L x^L([n,m]), \textrm{Fml}^L(2^{2^{(2^{[n,m]+1}(2n+1)-2)+8}(2(2^{[n,m]+1}(2m+1)-2)+1)-160}(2^{(2^{[n,m]+1}(2m+1)-2)+6}(2(2^{[n,m]+1}(2n+1)-2)+1)-41)-21) \\ & = & \forall^L x^L([n,m]), \textrm{Fml}^L(2^{2^{2^{[n,m]+1}(2n+1)+6}(2^{[n,m]+2}(2m+1)-3)-160}(2^{2^{[n,m]+1}(2m+1)+4}(2^{[n,m]+2}(2n+1)-3)-41)-21) \\ & = & \textrm{Fml}^L(2^{([n,m])+3}(2(2^{2^{2^{[n,m]+1}(2n+1)+6}(2^{[n,m]+2}(2m+1)-3)-160}(2^{2^{[n,m]+1}(2m+1)+4}(2^{[n,m]+2}(2n+1)-3)-41)-21)+1)-1) \\ & = & \textrm{Fml}^L(2^{[n,m]+3}(2^{2^{2^{[n,m]+1}(2n+1)+6}(2^{[n,m]+2}(2m+1)-3)-159}(2^{2^{[n,m]+1}(2m+1)+4}(2^{[n,m]+2}(2n+1)-3)-41)-41)-1) \\ & & \\ & & x^L(n) \neq^L x^L(m) \\ & := & \neg^L(x^L(n) =^L x^L(m)) \\ & = & \neg^L \textrm{Fml}^L(2^{[n,m]+3}(2^{2^{2^{[n,m]+1}(2n+1)+6}(2^{[n,m]+2}(2m+1)-3)-159}(2^{2^{[n,m]+1}(2m+1)+4}(2^{[n,m]+2}(2n+1)-3)-41)-41)-1) \\ & = & \textrm{Fml}^L(8(2^{[n,m]+3}(2^{2^{2^{[n,m]+1}(2n+1)+6}(2^{[n,m]+2}(2m+1)-3)-159}(2^{2^{[n,m]+1}(2m+1)+4}(2^{[n,m]+2}(2n+1)-3)-41)-41)-1)+3) \\ & = & \textrm{Fml}^L(2^{[n,m]+3}(2^{2^{2^{[n,m]+1}(2n+1)+6}(2^{[n,m]+2}(2m+1)-3)-156}(2^{2^{[n,m]+1}(2m+1)+4}(2^{[n,m]+2}(2n+1)-3)-41)-41)+2) \\ \end{eqnarray*} As a consequence, all the entries of \(\textrm{Fml}\) above other than \(\neg^L \textrm{Fml}^L(n)\) are presented as \(\textrm{Fml}(N)\) for some \(N \in \mathbb{N}\) with \(N < 2 \uparrow^2 10(n+m+1)\). It might be better to explain how \(\exists !^L \) works, but I avoid it. If I did it, then I should explain the very tiresome (but quite elementary) syntax-theoretic definition of the substitution \(\textrm{Fml}^L(n)[x^L(m)/x^L(k)]\). If a reader wants to know it, it is much better to study formal logic with standard textbooks than reading this blog post.

Now I compute explicit formulae. The formula \(\forall^L x^L(1), x^L(1) \notin^L x^L(0)\) in \(L\) defines the empty set \(0^L\). The corresponding Goedel number is computed in the following way: \begin{eqnarray*} & & \forall^L x^L(1), x^L(1) \notin^L x^L(0) \\ & = & \forall^L x^L(1), \textrm{Fml}^L(2^{1+4}(2 \cdot 0 + 1)-13) \\ & = & \forall^L x^L(1), \textrm{Fml}^L(19) \\ & = & \textrm{Fml}^L(2^{1+3}(2 \cdot 19 + 1)-1) \\ & = & \textrm{Fml}^L(623) \end{eqnarray*} Also, the Goedel number of the existence of \(0^L\) is computed in the following way: \begin{eqnarray*} & & \exists^L x^L(0), \forall^L x^L(1), x^L(1) \notin^L x^L(0) \\ & = & \exists^L x^L(0), \textrm{Fml}^L(623) \\ & = & \textrm{Fml}^L(2^{0+6}(16 \cdot 623 + 7)-5) \\ & = & \textrm{Fml}^L(638395) \end{eqnarray*} The formula \(\forall^L x^L(1), (x^L(1) \in^L x^L(0) \leftrightarrow^L \forall^L x^L(2), x^L(2) \notin^L x^L(1))\) in \(L\) defines the next easiest example \(1^L\). The corresponding Goedel number is computed in the following way: \begin{eqnarray*} & & \forall^L x^L(1), (x^L(1) \in^L x^L(0) \leftrightarrow^L \forall^L x^L(2), x^L(2) \notin^L x^L(1)) \\ & = & \forall^L x^L(1), (\textrm{Fml}^L(2^1(2 \cdot 0 + 1) - 1) \leftrightarrow^L \forall^L x^L(2), \textrm{Fml}^L(2^{2+4}(2 \cdot 1 + 1)-13)) \\ & = & \forall^L x^L(1), (\textrm{Fml}^L(1) \leftrightarrow^L \forall^L x^L(2), \textrm{Fml}^L(179)) \\ & = & \forall^L x^L(1), (\textrm{Fml}^L(1) \leftrightarrow^L \textrm{Fml}^L(2^{2+3}(2 \cdot 179 + 1)-1)) \\ & = & \forall^L x^L(1), (\textrm{Fml}^L(1) \leftrightarrow^L \textrm{Fml}^L(11487)) \\ & = & \forall^L x^L(1), \textrm{Fml}^L(2^{2^{1+8}(2 \cdot 11487 + 1)-160}(2^{11487+6}(2 \cdot 1 + 1)-41)-21) \\ & = & \forall^L x^L(1), \textrm{Fml}^L(2^{2^9 \cdot 22975 - 160}(2^{11493} \cdot 3 - 41) - 21) \\ & = & \textrm{Fml}^L(2^{1+3}(2(2^{2^9 \cdot 22975 - 160}(2^{11493} \cdot 3 - 41) - 21)+1)-1) \\ & = & \textrm{Fml}^L(2^{11763025}(2^{11493} \cdot 3 - 41) - 657) \end{eqnarray*} Also, the Goedel number of the existence of \(1^L\) is computed in the following way: \begin{eqnarray*} & & \exists^L x^L(0), (\forall^L x^L(1), (x^L(1) \in^L x^L(0) \leftrightarrow^L \forall^L x^L(2), x^L(2) \notin^L x^L(1))) \\ & = & \exists^L x^L(0), \textrm{Fml}^L(2^{11763025}(2^{11493} \cdot 3 - 41) - 657) \\ & = & \textrm{Fml}^L(2^{0+6}(16 \cdot (2^{11763025}(2^{11493} \cdot 3 - 41) - 657) + 7)-5) \\ & = & \textrm{Fml}^L(2^{11763035}(2^{11493} \cdot 3 - 41) - 672325) \end{eqnarray*}

Estimation of Prf(n)

A formal proof of sufficiently small complexity is of length \(1\). Therefore the value of \(\textrm{Prf}(n)\) for sufficiently small \(n\) is presented as \(2^m\) for an \(m \in \mathbb{N}\) with \(\textrm{Fml}^L(m) \in A\). For example, the existence of \(0^L\), which is computed as \(\textrm{Fml}^L(638395)\) above, is a formal proof of length \(1\) and complexity \(\leq 2^{638395}\). It implies \(\textrm{Prf}(0) \leq 2^{638395}\).

I guess that \(2^{638395}\) is the smallest among the Goedel numbers of formal proofs, because all axioms other than the existence of \(0^L\) heavily contain the syntax sugars, which make their Goedel numbers very large compared to \(10^6\). Therefore \(\textrm{Prf}(0)\) perhaps coincides with \(2^{638395}\).

I give an upperbound of \(\textrm{Prf}(n)\). For any \(m \in \mathbb{N}\), \(\textrm{Fml}^L(m) \vee^L \textrm{Fml}^L(638395)\) admits the formal proof \((\textrm{Fml}^L(638395),\textrm{Fml}^L(m) \vee^L \textrm{Fml}^L(638395))\). Its Goedel number is computed in the following way: \begin{eqnarray*} & & (\textrm{Fml}^L(638395),\textrm{Fml}^L(m) \vee^L \textrm{Fml}^L(638395)) \\ & = & (\textrm{Fml}^L(638395),\textrm{Fml}^L(2^{8m+5}(2 \cdot 638395 + 1)-3)) \\ & = & (\textrm{Fml}^L(638395),\textrm{Fml}^L(2^{8m+5} \cdot 1276791 - 3)) \\ & = & (\textrm{Fml}^L(v_{\textrm{Prm}(i)}(2^{638395} \cdot 3^{2^{8m+5} \cdot 1276791 - 3})))_{i < 2} \end{eqnarray*} It implies \(\textrm{Prf}(n) \leq 2^{638395} \cdot 3^{2^{8n+5} \cdot 1276791 - 3} < 2 \uparrow^2 10(n+1)\).

Estimation of RWO(n,d)

By the definition, there is no formal proof of complexity \(\leq 0\). It implies that \(\textrm{RWO}(n,0)\) is the constant function \(0\). I need to give an example of \(d\) for which \(\textrm{RWO}(n,d)\) is not the constant function \(0\).

Now the existence of \(0^L\), which is \(\textrm{Fml}^L(638395)\), is an axiom. The uniqueness of \(0^L\) is a theorem, which admits a proof under the deduction theorem of length \(\leq 30\), and hence admits a formal proof of length \(\leq 300\). Therefore the unique existence of \(0^L\) admits a formal proof of length \(302\). Each entry of the formal proof would have the Goedel number smaller than \(2 \uparrow^2 10^{100}\). Therefore the Goedel number of the proof of the unique existence of \(0^L\) is bounded by \(2 \uparrow^4 400\) by the estimation of the concatenation above. It implies \(0 < \textrm{RWO}(0,2 \uparrow^4 2) \leq 623\).

I guess that \((623,2 \uparrow^4 2)\) is the smallest element of \(\mathbb{N} \times \{2 \uparrow^4 2\}\) with respect to \(<_{\textrm{RWO},2 \uparrow^4 2}\), as I guesses \(\textrm{Prf}(0) = 2^{638395}\). It would be incorrect if there were a "shorter" formula in \(L\) which defines a recursive well-order on a recursive subset of \(\mathbb{N}^L \times^L \mathbb{N}^L\) whose ordinal such that the statement that its ordinal type is \(0^L\) is independent of \(A\). Although I do not check all possible formulae, the non-existence of such a formula is not so doubtful. If it is correct, then I obtain the following: \begin{eqnarray*} \textrm{RWO}(n,d) & = & 0 \ (d \ll 2 \uparrow^4 2) \\ \textrm{RWO}(0,2 \uparrow^4 2) & = & 623 \end{eqnarray*}

Let \(N \in \mathbb{N}\) be a natural number such that \(\textrm{Fml}^L(N)\) defines \(\mathbb{N}^L\) without occurrence of \(x^L(i)\) for any \(i \in 5\) and with free variable \(x^L(5)\). Then the formula \begin{eqnarray*} \forall^L x^L(1), \forall^L x^L(2), \left( \begin{array}{l} (x^L(1),x^L(2))^L \in^L x^L(0) \\ \leftrightarrow^L \exists^L x^L(3), \exists^L x^L(4), \left( \begin{array}{cl} & x^L(1) =^L (x^L(3),x^L(3))^L \\ \wedge^L & x^L(2) =^L (x^L(4),x^L(4))^L \\ \wedge^L & \forall^L x^L(5), \textrm{Fml}^L(N) \to^L x^L(4) \in^L x^L(5) \\ \wedge^L & x^L(3) \subset^L x^L(4) \end{array} \right) \end{array} \right)\end{eqnarray*} defines a recursive limit well-order on the diagonal subset of \(\mathbb{N}^L \times^L \mathbb{N}^L\), whose ordinal type is \(\omega^L\). Its Goedel number, which is clearly smaller than \(2 \uparrow^3 1000\), is a candidate of the value of \(\textrm{RWO}(n,d)\) for a \(d \in \mathbb{N}\) with \(d \gg 2 \uparrow^4 1000\).

I give an upperbound of \(\textrm{RWO}(n,d)\). If \(n \geq N(d)\), then \(\textrm{RWO}(n,d) = 0\) is bounded by \(1\). Suppose \(n < N(d)\). Then there is a formal proof \(\textrm{Prf}(N)\) of complexity \(\leq d \) of the 整礎性 of \(\textrm{RWO}(n,d)\), i.e. \(\exists !^L x^L(0), (\textrm{Fml}^L(N) \wedge^L \textrm{RWO}^L)\). It implies \(\textrm{RWO}(n,d) \leq \textrm{Prf}(N) < 2 \uparrow^2 10(d+1)\). Therefore \(2 \uparrow^2 10(d+1)\) is an upperbound of \(\textrm{RWO}(n,d)\).

It is not easy to determine whether the Goedel number of a given definition of a well-order corresponding to a recursive ordinal number well-known here, e.g. \(\varepsilon_0\), \(\textrm{LVO}\), \(\psi_0(\psi_I(0))\), \(\psi_0(\varepsilon_{K + 1})\) and so on, lies in the image of \(\textrm{RWO}\). However, \(\textrm{RWO}\) partially diagonalises the proof theoretic strengthen of the \(\textrm{ZFC}\) axiom. Therefore I expect that the limit of this ordinal notation is greater actually than that of another ordinal notation which is provably 整礎 under \(\textrm{ZFC}\) axiom.

Estimation of N(d)

Since \(2 \uparrow^2 10(d+1)\) is an upperbound of \(\textrm{RWO}(n,d)\), it is also an upperbound of \(N(d)\) by the strict monotonousness of \(\textrm{RWO}(n,d)\) on \(n\) with \(n < N(d)\). I give a lower bound of \(N(d)\).

By \(0 < \textrm{RWO}(0,2 \uparrow^4 2) \leq 623\), the inequality \(N(d) > 0\) holds for any \(d \in \mathbb{N}\) with \(d \geq 2 \uparrow^4 2\). Let \((n,d) \in \mathbb{N} \times \mathbb{N}\) with \(n < N(d)\) denote the element such that the ordinal type of the recursive well-order \(\leq_S\) defined by \(\textrm{RWO}(n,d)\) is the greatest among those of the recursive well-orders defined by \(\textrm{RWO}(m,d)\) with \(m < N(d)\).

I denote by \(S \subset^L \mathbb{N}^L \times^L \mathbb{N}^L\) the underlying set of \(\leq_S\). It is easy (and also tiresome) to define its successor by replacing \(S\) and \(\leq_S\) by \begin{eqnarray*} S' := \{(0^L,0^L)^L\}^L \cup^L \{(x \cup^L \{x\}^L, y \cup^L \{y\}^L)^L \mid (x,y)^L \in^L S\}^L \subset^L \mathbb{N}^L \times^L \mathbb{N}^L \end{eqnarray*} and \begin{eqnarray*} \leq_{S'} & := & \{(0^L,0^L)^L\}^L \cup^L \{(0,y \cup^L \{y\}^L)^L \mid (y,y)^L \in^L S \}^L \\ & & \cup^L \{(x \cup^L \{x\}^L, y \cup^L \{y\}^L)^L \mid (x,y)^L \in^L S \wedge^L x \leq_S y \}^L. \end{eqnarray*} I denote by \(\textrm{Suc}(n) \in \mathbb{N}\) the Goedel number of a fixed definition of the successor. Then the inequality \begin{eqnarray*} \textrm{Suc}(n) < \underbrace{2 \uparrow^2 \cdots 2 \uparrow^2}_{10^{100}} \textrm{RWO}(n,d) < 2 \uparrow^3 (10(d+1) + 10^{100}) \end{eqnarray*} holds by the construction of \(\textrm{Suc}(n)\).

Let \(M_1 = \textrm{Prf}(m_1)\) be a formal proof of complexity \(\leq d\) that \(\leq_S\) is a recursive well-order, and \(M_2 = \textrm{Prf}(m_2)\) a formal proof of the statement that if \(x^L(0)\) is a recursive well-order, then its successor is a recursive successor whose ordinal type is greater than that of \(x^L(0)\). Then \(M_2\) can be obviously chosen as to be bounded by \(2 \uparrow^4 10^{100}\) by the estimation of the Goedel numbers of the concatenation and the syntax sugars.

Applying \(\forall^L\)-elimination to the consequence of \(\textrm{Prf}(m_1)\), I obtain a formal proof of the statement that the ordinal type of \(\textrm{Suc}(n)\) is greater than that of \(\textrm{RWO}(n,d)\) with respect to \(<_{\textrm{RWO}}\) of complexity \begin{eqnarray*} & \leq & \underbrace{2 \uparrow^3 \cdots 2 \uparrow^3}_{10^{100}} (\textrm{Suc}(n) + M_1 + M_2 + 1) \\ & \leq & \underbrace{2 \uparrow^3 \cdots 2 \uparrow^3}_{10^{100}} ((2 \uparrow^3 (10(d+1) + 10^{100})) + (\uparrow^2 10(d+1)) + (2 \uparrow^4 10^{100})) \\ & \leq & 2 \uparrow^4 10^{100}(d+1) = B(d). \end{eqnarray*} It implies \(N(d) + 1 \leq N(B(d))\) for any \(d \in \mathbb{N}\) with \(d \geq 2 \uparrow^4 2\), and hence \(\lim_{d \to \infty} N(d) = \infty\). Therefore \(B(d)\) roughly tells us an upperbound of "when the greatest recursive well-order is updated".

Similarly, it is not so difficult to estimate an upperbound of "when the greatest recursive well-order below a given recursive limit well-order is updated". Maybe it is also bounded by \(B(d)\), because the estimation above is not so tight. That is why I defined \(B(d)\) in this way when I introduced the system of functions \(f_{(n,d)}\).