拡張ブーフホルツのψ関数に伴う順序数表記(あるいは拡張Buchholz OCFに伴う順序数表記)^[1]は p進大好きbot^[2] が2018年6月9日に公開した表記である。

拡張ブーフホルツのψ関数に伴う順序数表記は、拡張ブーフホルツのψ関数に付随する順序数表記である。この表記から自然な順序数への対応\(o\)で表せない最小の可算順序数は拡張ブーフホルツ順序数である。

定義[]

記法[]

\((\)と\()\)と \(\langle\)と \(\rangle\)とコンマのみからなる文字列の集合\(T\)と\(PT\)を以下のように再帰的に定める：

\(() \in T\)である。
いかなる\(X_1,X_2 \in T\)に対しても、\(\langle X_1, X_2 \rangle \in T\)かつ\(\langle X_1, X_2 \rangle \in PT\)である。
いかなる\(X_1, \ldots, X_m \in PT\) (\(2 \leq m < \infty\))に対しても、\((X_1, \ldots, X_m) \in T\)である。

後で\(T\)の上の再帰的強全順序と\(T\)の再帰的部分集合\(OT\)であって\((OT,<)\)が順序数表記になるもの、すなわち\(<\)の\(OT\)への制限が強整列順序になるものを定義する。\((OT,<)\)において、\(()\)は\(0\)の役割を持ち、\(\langle \ , \ \rangle\)は拡張Buchholz OCFの役割を持ち、\(( \ , \ldots, \ )\)は加法の役割を持つ。そのためカッコとコンマのみの表記が嫌いな人は\(()\)を\(0\)と置き換え、\(\langle X , Y \rangle\)を\(D_X Y\)なり\(\psi_X(Y)\)なりと置き換え、\((X_1, \ldots, X_m)\)を\(X_1 + \cdots + X_m\)と置き換えても良い。またカッコ以外が嫌いな人は\(\langle X , Y \rangle\)を\(\langle Y \rangle_X\)なり\((Y)_X\)なりと置き換え、\((X_1, \ldots, X_m)\)を\((X_1 \cdots X_m)\)なり\(X_1 \cdots X_m\)なりと置き換えても良い。

\(() \in T\)を\(\underline{0}\)と略記し、\(\langle \underline{0}, \underline{0} \rangle \in T\)を\(\underline{1}\)と略記し、\(1\)より大きい各\(n \in \mathbb{N}\)に対し\((\underbrace{\underline{1}, \ldots, \underline{1}}_{n}) \in T\)を\(\underline{n}\)と略記し、\(\langle \underline{0}, \underline{1} \rangle \in T\)を\(\underline{\omega}\)と略記する。

順序[]

\((X,Y) \in T^2\)に対し、\(2\)項関係\(X<Y\)を以下のように再帰的に定める：

もし\(X=\underline{0}\)ならば、\(X<Y\)は\(Y \neq \underline{0}\)と同値である。
ここで\(X = \langle X_1, X_2 \rangle \)を満たす\(X_1,X_2 \in T\)が存在するとする。
1. もし\(Y=\underline{0}\)ならば、\(X<Y\)は偽である。
2. ここで\(Y = \langle Y_1, Y_2 \rangle \)を満たす\(Y_1,Y_2 \in T\)が存在するとする。
  1. もし\(X_1=Y_1\)ならば、\(X<Y\)は\(X_2<Y_2\)と同値である。
  2. もし\(X_1 \neq Y_1\)ならば、\(X<Y\)は\(X_1<Y_1\)と同値である。
3. もし\(Y=(Y_1, \ldots, Y_{m'})\)を満たす\(Y_1,\ldots,Y_{m'} \in PT\) (\(2 \leq m' < \infty\))が存在するならば、\(X<Y\)は\(X=Y_1\)または\(X<Y_1\)と同値である。
ここで\(X=(X_1, \ldots, X_m)\)を満たす\(X_1,\ldots,X_m \in PT\) (\(2 \leq m < \infty\))が存在するとする。
1. もし\(Y=\underline{0}\)ならば、\(X<Y\)は偽である。
2. もし\(Y = \langle Y_1, Y_2 \rangle \)を満たす\(Y_1,Y_2 \in T\)が存在するならば、\(X<Y\)は\(X_1<Y\)と同値である。
3. ここで\(Y=(Y_1, \ldots, Y_{m'})\)を満たす\(Y_1,\ldots,Y_{m'} \in PT\) (\(2 \leq m' < \infty\))が存在するとする。
  1. ここで\(X_1=Y_1\)とする。
    1. もし\(m = 2\)かつ\(m' = 2\)ならば、\(X<Y\)は\(X_2<Y_2\)と同値である。
    2. もし\(m = 2\)かつ\(m' > 2\)ならば、\(X<Y\)は\(X_2<(Y_2,\ldots,Y_{m'})\)と同値である。
    3. もし\(m > 2\)かつ\(m' = 2\)ならば、\(X<Y\)は\((X_2,\ldots,X_m)<Y_2\)と同値である。
    4. もし\(m > 2\)かつ\(m' > 2\)ならば、\(X<Y\)は\((X_2, \ldots, X_m)<(Y_2, \ldots, Y_{m'})\)と同値である。
  2. もし\(X_1 \neq Y_1\)ならば、\(X<Y\)は\(X_1<Y_1\)と同値である。

ただし\(<\)自身は強整列順序でなく、単なる強全順序である。「\(X<Y\)または\(X=Y\)」を「\(X \leq Y\)」と略記する。

基本列[]

全域再帰的写像 \begin{eqnarray*} \textrm{dom} \colon T & \to & T \\ X & \mapsto & \textrm{dom}(X) \\ & & \\ [ \ ] \colon T \times T & \to & T \\ (X,Y) & \mapsto & X[Y] \end{eqnarray*} を以下のように再帰的に定める：

もし\(X = \underline{0}\)ならば、\(\textrm{dom}(X) = \underline{0}\)かつ\(X[Y] = \underline{0}\)である。
ここで\(X = \langle X_1, X_2 \rangle \)を満たす\(X_1,X_2 \in T\)が存在するとする。
1. ここで\(\textrm{dom}(X_2) = \underline{0}\)とする。
  1. もし\(\textrm{dom}(X_1) = \underline{0}\)ならば、\(\textrm{dom}(X) = X\)かつ\(X[Y] = \underline{0}\)である。
  2. もし\(\textrm{dom}(X_1) = \underline{1}\)ならば、\(\textrm{dom}(X) = X\)かつ\(X[Y]=Y\)である。
  3. もし\(\textrm{dom}(X_1) \notin \{\underline{0},\underline{1}\}\)ならば、\(\textrm{dom}(X) = \textrm{dom}(X_1)\)かつ\(X[Y] = \langle X_1[Y] , \underline{0} \rangle\)である。
2. もし\(\textrm{dom}(X_2) = \underline{1}\)ならば、\(\textrm{dom}(X) = \underline{\omega}\)である。
  1. もし\(Y = \underline{1}\)ならば、\(X[Y] = \langle X_1, X_2[\underline{0}] \rangle\)である。
  2. もし\(Y = \underline{k}\) (\(2 \leq k < \infty\))ならば、\(X[Y]=(\underbrace{\langle X_1, X_2[\underline{0}] \rangle, \ldots, \langle X_1, X_2[\underline{0}] \rangle}_{k})\)である。
  3. そうでないならば、\(X[Y] = \underline{0}\)である。
3. もし\(\textrm{dom}(X_2) = \underline{\omega}\)ならば、\(\textrm{dom}(X) = \underline{\omega}\)かつ\(X[Y] = \langle X_1 , X_2[Y] \rangle \)である。
4. ここで\(\textrm{dom}(X_2) \notin \{\underline{0},\underline{1},\underline{\omega}\}\)とする。
  1. もし\(\textrm{dom}(X_2) < X\)ならば、\(\textrm{dom}(X) = \textrm{dom}(X_2) \)かつ\(X[Y] = \langle X_1 , X_2[Y] \rangle \)である。
  2. そうでないならば、\(\textrm{dom}(X) = \underline{\omega}\)である。
    1. \(\textrm{dom}(X_2) = \langle Z, \underline{0} \rangle\)と置く。
    2. もし\(Y = \underline{h}\) (\(1 \leq h < \infty\))かつ\(X[Y[\underline{0}]] = \langle X_1, \Gamma \rangle\)を満たす\(\Gamma \in T\)が存在するならば、\(X[Y]= \langle X_1, X_2[\langle Z[\underline{0}], \Gamma \rangle] \rangle\)である。
    3. そうでないならば、\(X[Y] = \langle X_1, X_2[\langle Z[\underline{0}], \underline{0} \rangle] \rangle\)である。
もし\(X = (X_1, \ldots,X_m)\)を満たす\(X_1,\ldots,X_m \in PT\) (\(2 \leq m < \infty\))が存在するならば、\(\textrm{dom}(X)=\textrm{dom}(X_m)\)である。
1. もし\(X_m[Y] = \underline{0}\)かつ\(m = 2\)ならば、\(X[Y]=X_1\)である。
2. もし\(X_m[Y] = \underline{0}\)かつ\(m > 2\)ならば、\(X[Y]=(X_1, \ldots, X_{m-1})\)である。
3. もし\(X_m[Y] \in PT\)ならば、\(X[Y]=(X_1, \ldots, X_{m-1},X_m[Y])\)である。
4. \(X_m[Y] = (Z_1, \ldots, Z_{m'})\)を満たす\(Z_1, \ldots, Z_{m'} \in PT\) (\(2 \leq m' < \infty\))が存在するならば、\(X[Y]=(X_1, \ldots, X_{m-1}, Z_1, \ldots, Z_{m'})\)である。

次の章で再帰的部分集合\(OT \subset T\)を\(\{[\underline{n}] \mid n \in \mathbb{N}\}\)で閉じかつ\([ \ ]\)の\(\{X \in OT \mid X < \langle \underline{1}, \underline{0} \rangle\} \times \{\underline{n} \mid n \in \mathbb{N}\}\)への制限が\(<\)の制限に関する基本列系をなすように定義する。

標準形[]

\((X,Y,Z) \in T^3\)に対し、再帰的\(3\)項関係\(G(X,Y) \triangleleft Z\)を以下のように再帰的に定める：

もし\(Y = \underline{0}\)ならば、\(G(X,Y) \triangleleft Z\)は真である。
ここで\(Y = \langle W_1, W_2 \rangle\)を満たす\(W_1,W_2 \in T\)が存在するとする。
1. もし\(X \leq W_1\)ならば、\(G(X,Y) \triangleleft Z\)は\(W_2 < Z\)かつ\(G(X,W_1) \triangleleft Z\)かつ\(G(X,W_2) \triangleleft Z\)と同値である。
2. もし\(W_1 < X\)ならば、\(G(X,Y) \triangleleft Z\)は真である。
もし\(Y = (W_1,\ldots,W_{m'})\)を満たす\(W_1,\ldots,W_{m'} \in PT\) (\(2 \leq m' < \infty\))が存在するならば、\(G(X,Y) \triangleleft Z\)は\(m'\)未満のいかなる\(i \in \mathbb{N}\)に対しても\(G(X,W_{i+1}) \triangleleft Z\)となることと同値である。

部分集合\(OT \subset T\)を以下のように再帰的に定める：

\(\underline{0} \in OT\)である。
いかなる\(X_1,X_2 \in T\), \(\langle X_1, X_2 \rangle \in OT\)は\(X_1 \in OT\)かつ\(X_2 \in OT\)かつ\(G(X_1,X_2) \triangleleft X_2\)と同値である。
いかなる\(X_1, \ldots, X_m \in PT\) (\(2 \leq m < \infty\))に対しても、\((X_1, \ldots, X_m) \in OT\)は\(m\)未満のいかなる\(i \in \mathbb{N}\)に対しても\(X_{i+1} \in OT\)となりかつ\(m-1\)未満のいかなる\(i \in \mathbb{N}\)に対しても\(X_{i+2} \leq X_{i+1}\)となることと同値である。

最小の\(\Omega\)不動点を\(\Omega_{\Omega_{\cdot_{\cdot_{\cdot}}}}\)と置く。写像 \begin{eqnarray*} o \colon T & \to & \Omega_{\Omega_{\cdot_{\cdot_{\cdot}}}} \\ X & \mapsto & o(X) \end{eqnarray*} を以下のように帰納的に定める：

もし\(X = \underline{0}\)ならば、\(o(X) = 0\)である。
もし\(X = \langle Y_1, Y_2 \rangle\)を満たす\(Y_1,Y_2 \in T\)が存在するならば、\(o(X) = \psi_{o(Y_1)}(o(Y_2))\)である。ただし\(\psi\)は拡張Buchholz OCFである。
もし\(X = (Y_1,\ldots,Y_m)\)を満たす\(Y_1,\ldots,Y_m \in PT\) (\(2 \leq m < \infty\))が存在するならば、\(o(X) = o(Y_1) + \cdots + o(Y_m)\)である。

構成から、\((OT,<)\)は順序数表記をなし、\(o\)の制限は順序集合の同型 \begin{eqnarray*} (OT,<) & \to & (C_0(\Omega_{\Omega_{\cdot_{\cdot_{\cdot}}}}),\in) \\ (\{X \in OT \mid X < \langle \underline{1}, \underline{0} \rangle\},<) & \to & (C_0(\Omega_{\Omega_{\cdot_{\cdot_{\cdot}}}}) \cap \Omega,\in) \end{eqnarray*} を与える。

FGH[]

全域再帰的写像 \begin{eqnarray*} f \colon OT \times \mathbb{N} & \to & \mathbb{N} \\ (X,n) & \mapsto & f_X(n) \end{eqnarray*} を以下のように再帰的に定める：

もし\(\textrm{dom}(X) = \underline{0}\)ならば、\(f_X(n) = n+1\)である。
もし\(\textrm{dom}(X) = \underline{1}\)ならば、\(f_X(n) = f_{X[\underline{0}]}^n(n)\)である。
そのいずれでもないならば、\(f_X(n) = f_{X[\underline{n}]}(n)\)である。

\(n \in \mathbb{N}\)に対し、\(X_n \in OT\)を以下のように再帰的に定める：

もし\(n = 0\)ならば、\(X_n = \underline{0}\)である。
もし\(n > 0\)ならば、\(X_n = \langle X_{n-1} , \underline{0} \rangle\)である。

\(f\)の全域性は\((OT,<)\)の整礎性と\([ \ ]\)の\(OT \times \{\underline{n} \mid n \in \mathbb{N}\}\)への制限が基本列系をなすことからただちに従う。構成から、全域計算可能関数 \begin{eqnarray*} F \colon \mathbb{N} & \to & \mathbb{N} \\ n & \mapsto & f_{\langle \underline{0}, X_n \rangle}(n) \end{eqnarray*} は拡張Buchholz OCFの標準的な基本列系に関する\(f_{\psi_0(\Omega_{\Omega_{\cdot_{\cdot_{\cdot}}}})}(n)\)と厳密に一致する。

計算例[]

以下\(f_X\)を\(X\)と略記する。\(F(0),F(1),F(2),\ldots,F(10^{100})\)までを順に計算してみる。

\begin{eqnarray*} F(0) & = & \langle \underline{0}, X_0 \rangle(0) \\ & = & \langle \underline{0}, \underline{0} \rangle(0) \\ & = & \underline{1}(0) \\ & = & \underline{0}^0(0) \\ & = & 0 \\ & & \\ F(1) & = & \langle \underline{0}, X_1 \rangle(1) \\ & = & \langle \underline{0}, \langle X_0 , \underline{0} \rangle \rangle(1) \\ & = & \langle \underline{0}, \langle \underline{0} , \underline{0} \rangle \rangle(1) \\ & = & \langle \underline{0}, \underline{1} \rangle(1) \\ & = & [\langle \underline{0}, \underline{1} \rangle|\underline{1}](1) \\ & = & (\langle \underline{0}, \underline{0} \rangle)(1) \\ & = & (\underline{1})(1) \\ & = & \underline{0}^1(1) \\ & = & 1+1 \\ & = & 2 \\ & & \\ F(2) & = & \langle \underline{0}, X_2 \rangle(2) \\ & = & \langle \underline{0}, \langle X_1, \underline{0} \rangle \rangle(2) \\ & = & \langle \underline{0}, \langle \underline{1}, \underline{0} \rangle \rangle(2) \\ & = & [\langle \underline{0}, \langle \underline{1}, \underline{0} \rangle \rangle|\underline{2}](2) \\ & = & \langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, \langle \underline{0}, \underline{0} \rangle \rangle] \rangle] \rangle(2) \\ & = & \langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, \underline{0} \rangle] \rangle] \rangle] \rangle(2) \\ & = & \langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\underline{1}] \rangle] \rangle] \rangle(2) \\ & = & \langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, \underline{1} \rangle] \rangle] \rangle(2) \\ & = & \langle \underline{0}, [\langle \underline{1}, \underline{0} \rangle|\langle \underline{0}, \langle \underline{0}, \underline{1} \rangle \rangle] \rangle(2) \\ & = & \langle \underline{0}, \langle \underline{0}, \langle \underline{0}, \underline{1} \rangle \rangle \rangle(2) \\ & = & [\langle \underline{0}, \langle \underline{0}, \langle \underline{0}, \underline{1} \rangle \rangle \rangle|\underline{2}](2) \\ & = & \langle \underline{0}, [\langle \underline{0}, \langle \underline{0}, \underline{1} \rangle \rangle|\underline{2}] \rangle(2) \\ & = & \langle \underline{0}, \langle \underline{0}, [\langle \underline{0}, \underline{1} \rangle|\underline{2}] \rangle \rangle(2) \\ & = & \langle \underline{0}, \langle \underline{0}, (\langle \underline{0}, \underline{0} \rangle, \langle \underline{0}, \underline{0} \rangle) \rangle \rangle(2) \\ & = & \langle \underline{0}, \langle \underline{0}, (\underline{1},\underline{1}) \rangle \rangle(2) \\ & = & \langle \underline{0}, \langle \underline{0}, \underline{2} \rangle \rangle(2) \\ & = & [\langle \underline{0}, \langle \underline{0}, \underline{2} \rangle \rangle|\underline{2}](2) \\ & = & \langle \underline{0}, [\langle \underline{0}, \underline{2} \rangle|\underline{2}] \rangle(2) \\ & = & \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \langle \underline{0}, \underline{1} \rangle) \rangle(2) \\ & = & [\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \langle \underline{0}, \underline{1} \rangle) \rangle|\underline{2}](2) \\ & = & \langle \underline{0}, [(\langle \underline{0}, \underline{1} \rangle, \langle \underline{0}, \underline{1} \rangle)|\underline{2}] \rangle(2) \\ & = & \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \langle \underline{0}, \underline{0} \rangle, \langle \underline{0}, \underline{0} \rangle) \rangle(2) \\ & = & \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}, \underline{1}) \rangle(2) \\ & = & [\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}, \underline{1}) \rangle|\underline{2}](2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle)(2) \\ & = & [(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle)|\underline{2}](2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle)(2) \\ & = & [(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle)|\underline{2}](2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, [\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle|\underline{2}])(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, [(\langle \underline{0}, \underline{1} \rangle)|\underline{2}] \rangle)(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{0} \rangle, \langle \underline{0}, \underline{0} \rangle) \rangle)(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1},\underline{1}) \rangle)(2) \\ & = & [(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1},\underline{1}) \rangle)|\underline{2}](2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, [\langle \underline{0}, (\underline{1},\underline{1}) \rangle|\underline{2}])(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \langle \underline{0}, (\underline{1}) \rangle)(2) \\ & = & [(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \langle \underline{0}, (\underline{1}) \rangle)|\underline{2}](2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, [\langle \underline{0}, (\underline{1}) \rangle|\underline{2}])(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \langle \underline{0}, \underline{0} \rangle, \langle \underline{0}, \underline{0} \rangle)(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1}, \underline{1})(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1})^2(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1})(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle)^2(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1})(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle)[(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle)|\underline{2}](2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1})(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle)(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, [\langle \underline{0}, (\underline{1}) \rangle|\underline{2}])(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1})(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle)(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, \underline{0} \rangle, \langle \underline{0}, \underline{0} \rangle)(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1})(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle)(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \underline{1}, \underline{1})(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1})(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle)(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \underline{1})^2(2) \\ & = & (\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle, \underline{1})(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \langle \underline{0}, (\underline{1}) \rangle)(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle, \underline{1})(\langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle, \underline{1}) \rangle, \langle \underline{0}, (\langle \underline{0}, \underline{1} \rangle) \rangle)^2(2) \\ & = & \cdots \end{eqnarray*}

拡張ブーフホルツのψ関数に伴う順序数表記

目次