亜原始数列とVeblen関数

亜原始数列の停止性を証明するための記事です。十分に見直していないので誤植や論理的誤りがいっぱいあるかもしれません。何か見つけたら教えて下さい。

背景

ユーザーブログ:Naruyoko/亜原始数列とペア数列システム（2022/05/18 17:01の版）に

亜原始数列とはYukito氏が考案した表記で、極限\((0,\omega)\)はヴェブレンの関数で\(\varphi(\omega,0)\)に対応すると信じられてきたが、その証明は2022/05/17現在存在しない。

および

過去にヴェブレンの関数への対応写像を公開したが、非常に乱雑かつ複雑であり、証明は難航していた。

と書かれているのを2022/05/18 21:00頃に読んだ。当時「亜原始数列から順序数への適切な対応はVeblen関数を用いて非常に簡潔に書ける」と思っていたので驚き、

亜原始数列の解析って未証明なんですね。難しいのかな。

とtweetし、直後に変換写像の定義を

例えば単純にoを加法的にしてaddive principalな亜原始数列xの根の右端の子cの成分をdとしてcより左側をyとしてcとその右側の数列全てからdを引いた数列をzとしてo(x)を o(y)==0?(φ_{d-1}(o(z)):o(y)のφ_{d-1}成分を1+o(z)上げたもの) とするだけじゃ駄目かな？

とtweetした。ただしここでは空列は扱わず\(o(0) = 0\)と定める流儀で、addiveはadditiveの誤植である。更に亜原始数列の停止性に関して

亜原始数列の[n]は右端の子が子を持つ限り伝播しVeblen関数も通常の基本列系に関してそのような伝播をするから右端の子が子を持たない場合に帰着され、この場合は[n]が全体のコピーをずらしただけなので、o側はφ_{d-1}内1引いてd=1の時はn倍、d>1の時は×2してからφ_{d-2}入れ子なので順序同型っぽい。

と証明の概要をtweetした。

tweet内では亜原始数列の用語（additive principalや根や[n]など）および「加法的」や「伝播」などの意味を説明していないが、亜原始数列とVeblen関数を熟知していればそれらが推測でき、証明の細部をどう記述するかが分かるだろうと期待し、結果的にほぼ停止性の証明として完結していると思い満足していた。

その後特に間違いが指摘されることもなかったのでNaruyokoさん本人に

Veblenとの変換写像が難しいと書いてありますが、僕のtweetのやつすごく短いんですけどこれ間違ってますかね？

とコメントで質問したところ

多分合っていると思います。実際、順序数そのものを扱うならばそんな感じでかなり楽にできると思います。前にVeblenと対応させてやっていたときは伴う順序数表記を使おうとして複雑化していた上、あまり理解せずに使っていたため方向性がわからなくなってしまい、今回停滞したところを一度リセットして、ついでに順序に同じ辞書式順序を使うペア数列への対応の大まかな機構があったためそちらに切り替えた感じです。

とコメントで返信をいただいた。

もしVeblen関数を用いた対応が正しいならば、Veblen関数とペア数列の対応の証明はさほど簡単でないと推測したため、ペア数列を用いて亜原始数列を解析しようとしているNaruyokoさんの手法は難航すると予想した。というわけで上記の証明の概要をきちんと数式で書き下すことを決意したのだが、普通に難航しなかったら内容を被せてしまい申し訳ない。

用語と記法

というわけで、元のtweetで省略した用語の説明から始める。そのために記法をいくつか導入する。

数列

\(\mathbb{N}^{< \omega}\)で自然数の有限列全体の集合を表す。

\((a,b) \in (\mathbb{N}^{< \omega})^2\)に対し\(a \frown b\)で\(a\)と\(b\)の結合を表す。

\((a,d) \in \mathbb{N}^{< \omega} \times \mathbb{N}\)に対し、\(\uparrow(a,d)\)を以下のように再帰的定める：

1. \(a = ()\)ならば、\(\uparrow(a,d) := ()\)である。
2. \(a = (s) \frown b\)を満たす\((s,b) \in \mathbb{N} \times \mathbb{N}^{< \omega}\)が存在するならば、\(\uparrow(a,d) := (s+d) \frown \uparrow(b,d)\)である。

要するに\(a\)の全成分を\(d\)増やして得られる数列である。

\(\mathbb{N}^{< \omega}\)の再帰的部分集合\(T_{<(0,\omega)}\)を \begin{eqnarray*} T_{<(0,\omega)} := \{()\} \cup \{(0) \frown a \mid a \in \mathbb{N}^{< \omega}\} \end{eqnarray*} と定める。

\(a \in T_{<(0,\omega)}\)がadditive principalであるとは、\(a = (0) \frown \uparrow(b,1)\)を満たす\(b \in \mathbb{N}^{< \omega}\)が存在するということである。

additive principalな数列が順序数のadditive principal性の自然な類似であることは後に定義する写像\(o_T\)の性質から分かる。additive principalな\(a \in T_{<(0,\omega)}\)全体の集合を\(PT_{<(0,\omega)}\)と置く。

各\(a \in T_{<(0,\omega)}\)に対し、 \begin{eqnarray*} \textrm{Node}(a) := \{i \in \mathbb{N} \mid 0 < i < \textrm{Lng}(a) \land a_0 < a_i \land \forall j \in \mathbb{N}, 0 < j < i \to a_j \geq a_i\} \end{eqnarray*} と定め、\(\textrm{Node}(a) \neq \emptyset\)である時はその最大値を\(\textrm{RightmostNode}(a)\)と置き、\(a_{\textrm{RightmostNode}(a)}\)を\(\delta(a)\)と置く。

命題（additive principalかつ\((0)\)でないならば\(\textrm{RightmostNode}\)が定まること）
\(a \neq (0)\)を満たす任意の\(a \in PT_{<(0,\omega)}\)に対し、\(1 \in \textrm{Node}(a)\)である。

証明

\(PT_{<(0,\omega)}\)の定義より\(\textrm{Lng}(a) > 0\)かつ\(a_0 = 0\)である。更に\(a \neq (0)\)より\(\textrm{Lng}(a) > 1\)となる。\(PT_{<(0,\omega)}\)の定義より\(a = (0) \frown \uparrow(b,1)\)を満たす\(b \in \mathbb{N}^{< \omega}\)が存在するが、\(\textrm{Lng}(a) > 1\)より\(\textrm{Lng}(b) > 0\)となる。従って\(a_0 = 0 < b_0+1 = a_1\)となり、\(1 \in \textrm{Node}(a)\)である。□

\(a \neq ()\)を満たす各\(a \in T_{<(0,\omega)}\)に対し、 \begin{eqnarray*} \textrm{UpRightmostNode}(a) := \{i \in \mathbb{N} \mid a_i < a_{\textrm{Lng}(a) - 1}\} \end{eqnarray*} と定め、\(\textrm{UpRightmostNode}(a) \neq \emptyset\)である時はその最大値を\(\textrm{TopRightmostNode}(a)\)と置き、\((a_i)_{i=0}^{\textrm{TopRightmostNode}(a)-1}\)を\(G(a)\)と置き、\((a_i)_{i = \textrm{TopRightmostNode}(a)}^{\textrm{Lng}(a) - 2}\)を\(B(a)\)と置き、\(\Delta(a) := a_{\textrm{Lng}(a)-1} - a_{\textrm{TopRightmostNode}(a)} - 1\)と置く。

命題（\(()\)でなくかつ右端が\(0\)でないならば\(\textrm{TopRightmostNode}\)が定まること）
\(a \neq ()\)かつ\(a_{\textrm{Lng}(a) - 1} \neq 0\)を満たす任意の\(a \in T_{<(0,\omega)}\)に対し、\(0 \in \textrm{UpRightmostNode}(a)\)である。

証明

\(T_{<(0,\omega)}\)の定義より\(a_0 = 0 < a_{\textrm{Lng}(a) - 1}\)であるので\(0 \in \textrm{UpRightmostNode}(a)\)である。□

亜原始数列

\(T := T_{<(0,\omega)} \cup \{(0,\omega)\}\)と置き、\(PT := PT_{<(0,\omega)} \cup \{(0,\omega)\}\)と置く。今回は使わないが途中に小ネタを挟む事情で\(T\)の辞書式順序を\(<_T\)と表す。

各\(a \in T\)に対し、\(a\)の長さを\(\textrm{Lng}(a) \in \mathbb{N}\)と表す。\(i < \textrm{Lng}(a)\)を満たす各\((a,i) \in T \times \mathbb{N}\)に対し、\(a\)の第\(1+i\)成分を\(a_i \in \mathbb{N} \cup \{\omega\}\)と表す。

計算可能写像 \begin{eqnarray*} []_T \colon T \times \mathbb{N} & \to & \mathbb{N} \\ (a,n) & \mapsto & a[n]_T \end{eqnarray*} を亜原始数列#計算規則に記載された亜原始数列から自然数を定める計算手順から自然に得られる展開規則として以下のように再帰的に定める：

1. \(a = ()\)ならば、\(a[n]_T := ()\)である。
2. \(a = (0,\omega)\)ならば、\(a[n]_T := (0,n)\)である。
3. \(a \notin \{(),(0,\omega)\}\)とする。
   1. \(a_{\textrm{Lng}(a)-1} = 0\)ならば、\(a[n]_T := (a_i)_{i=0}^{\textrm{Lng}(a)-2}\)である。
   2. \(a_{\textrm{Lng}(a)-1} \neq 0\)とする。
      1. \(n = 0\)ならば、\(a[n]_T := G(a)\)である。
      2. \(n \neq 0\)ならば、\(a[n]_T := a[n-1]_T \frown \uparrow(B(a), (n-1) \Delta(a))\)である。

この定義は2022/05/28時点のユーザーブログ:Naruyoko/亜原始数列とペア数列システム#亜原始数列における写像\(\textrm{ExpandS}\)とは一致することが想定されていると推測している。

亜原始数列の計算を行う関数に名前をつけたほうが停止性を厳密に議論できるため、それを元の亜原始数列の記法に合わせて\(S\)と名付ける。つまり計算可能部分写像 \begin{eqnarray*} S \colon T \times \mathbb{N} & \to & \mathbb{N} \\ (a,n) & \mapsto & Sa[n] \end{eqnarray*} を以下のように再帰的に定める：

1. \(a = ()\)ならば、\(Sa[n] := n\)である。
2. \(a = (0,\omega)\)ならば、\(Sa[n] := S a[n]_T [n]\)である。
3. \(a \notin \{(),(0,\omega)\}\)ならば、\(Sa[n] := S a[n+1]_T [n+1]\)である。

今回は亜原始数列の停止性を証明する目的であるので標準形を導入する必要はないが、ところどころ標準形に関する豆知識を挿入したいので標準形を導入する。

各\(i \in \mathbb{N}\)に対し再帰的枚挙可能部分集合\(OT_i \subset T\)を以下のように再帰的に定める：

1. \(i = 0\)ならば、\(OT_i := \{(0,\omega)\}\)である。
2. \(i \neq 0\)ならば、\(OT_i := \{a[n]_T \mid (a,n) \in OT_{i-1} \times \mathbb{N}\}\)である。

更に \begin{eqnarray*} OT := \bigcup_{i \in \mathbb{N}} OT_i \end{eqnarray*} と置く。定義から\(OT\)もまた\(T\)の再帰的枚挙可能部分集合である。\(OT\)が\(T\)の再帰的部分集合であるか否かは自明でないのでその辺も扱うと楽しそうだが、今回は\(OT\)の性質ではなく亜原始数列の停止性を扱うのでその辺には触れないことにする。\(<_{OT}\)で\(<_T\)の\(OT\)への制限を表す。

変換写像

変換写像を定義する前に、変換写像の加法性という概念を紹介する。そのために数列をadditive principalな数列に分解する方法を導入する。

命題（additive principalへの分解）
\(a \neq ()\)を満たす任意の\(a \in T\)に対し、\(a = b \frown c\)を満たす一意な\((b,c) \in T \times PT\)が存在する。

証明

\(a \neq ()\)より\(T\)の定義から、\(\textrm{Lng}(a) > 0\)かつ\(a_0 = 0\)である。従って

\begin{eqnarray*} \{i \in \mathbb{N} \mid i < \textrm{Lng}(a) \land a_i = 0\} \end{eqnarray*}

は空でない有限集合であり、最大元\(I\)を持つ。

\(a = b \frown c\)を満たす\((b,c) \in T \times PT\)が存在することは、

\begin{eqnarray*} B & := & (a_i)_{i = 0}^{I - 1} \\ C & := & (a_i)_{i = I}^{\textrm{Lng}(a) - 1} \\ \end{eqnarray*}

と定めると\((b,c) = (B,C)\)が例となることから従う。

\(a = b \frown c\)を満たす\((b,c) \in T \times PT\)が一意であることは、\(PT\)の定義から\(\textrm{Lng}(c) > 0\)かつ\(c_0 = 0\)かつ\(0 < i < \textrm{Lng}(c)\)を満たす任意の\(i \in \mathbb{N}\)に対し\(c_i > 0\)となるために\(\textrm{Lng}(b) + 1 = I\)となり\((b,c) = (B,C)\)となることから従う。□

命題（additive principalへの分解）により一意な存在が保証される\(b\)と\(c\)をそれぞれ\(L(a)\)と\(R(a)\)と置く。

順序数\(\alpha\)と写像 \begin{eqnarray*} o \colon T & \to & \alpha \\ a & \mapsto & o(a) \end{eqnarray*} が加法的であるとは、以下を全て満たすということである：

1. \(o(()) = 0\)である。
2. \(a \neq ()\)を満たす任意の\(a \in T\)に対し\(o(a) = o(L(a)) + o(R(a))\)である。

要するに加法を加法に適切に移すということである。

\(\varphi\)でVeblen関数を表し、\(\Lambda := \varphi_{\omega}(0)+1\)と置く。

\(a \neq (0)\)を満たす各\(a \in PT_{<(0,\omega)}\)に対し、\(\mathcal{L}(a) := (a_i)_{i=0}^{\textrm{RightmostNode}(a)-1}\)と置くと\(\textrm{RightmostNode}(a)\)の定義より\(a = \mathcal{L}(a) \frown \uparrow(b,\delta(a))\)を満たす\(b \in PT_{<(0,\omega)}\)が一意に存在するのでそれを\(\mathcal{R}(a)\)と置く。

写像 \begin{eqnarray*} o_T \colon T & \to & \Lambda \\ a & \mapsto & o_T(a) \end{eqnarray*} を以下のように再帰的に定める：

1. \(a = ()\)ならば、\(o_T(a) := 0\)である。
2. \(a = (0)\)ならば、\(o_T(a) := \varphi_0(0)\)である。
3. \(a = (0,\omega)\)ならば、\(o_T(a) := \varphi_{\omega}(0)\)である。
4. \(a \in PT_{< (0,\omega)}\)かつ\(a \neq (0)\)とする。
   1. \(o_T(\mathcal{L}(a)) = \varphi_{\delta(a)-1}(\alpha)\)を満たす\(\alpha \in \Lambda\)が存在するならば、\(o_T(a) := \varphi_{\delta(a)-1}(\alpha + o_T(\mathcal{R}(a)))\)である。
   2. そうでないならば、\(1 + \alpha = o_T(\mathcal{R}(a))\)を満たす一意な\(\alpha\)を用いて\(o_T(a) := \varphi_{\delta(a)-1}(\alpha)\)である。
5. 上記のいずれの場合でもないならば、\(o_T(a) := o_T(L(a)) + o_T(R(a))\)である。

定義の分岐5から即座に従うように、\(o_T\)は加法的である。

停止性

\((a,n) \in T \times \mathbb{N}^{< \omega}\)に対し、\(\textrm{Expand}(a,n)\)を以下のように再帰的に定める：

1. \(n = ()\)ならば、\(\textrm{Expand}(a,n) := a\)である。
2. \(n \neq ()\)ならば、\(\textrm{Expand}(a,n) := \textrm{Expand}(a[n_0]_{\Lambda},(n_i)_{i=1}^{\textrm{Lng}(n)-1})\)である。

要するに基本列を反復する写像である。

\((a,b) \in T^2\)に関する関係\(a <_{T,[]_T} b\)を以下のように再帰的に定める：

1. \(b = 0\)ならば、\(a <_{T,[]_T} b\)は偽である。
2. \(b \neq 0\)ならば、\(a <_{T,[]_T} b\)が真であることと\(\textrm{Expand}(b,n) = a\)かつ\(n \neq ()\)を満たす\(n \in \mathbb{N}^{< \omega}\)が存在するということは同値である。

要するに\(a \neq b\)でありかつ\(b\)に基本列を施していって\(a\)に変形可能であるということである。

各\(a \in T\)に対し、 \begin{eqnarray*} T_a := \{b \in T \mid b <_{T,[]_T} a\} \end{eqnarray*} と定め、\(<_{T,[]_T}\)の\(T_a\)への制限を\(<_{a,[]_T}\)と置く。

定理（\(OT\)が\(\Lambda\)に対応すること）
(1) 任意の\(a \in T\)に対し、\((o_T(t[n]_T))_{n \in \textrm{cof}(o_T(t))}\)は\(o_T(a)\)の基本列である。
(2) 任意の\(a \in T\)に対し、\(o_T\)の\(T_a\)への制限は全射順序保存写像\((T_a,<_{a,[]_T}) \to (o_T(a),\in)\)を定める。

ちなみに追加で\(o_T\)の\(OT\)への制限\(o_{OT}\)が順序同型\((OT,<_{OT}) \to (\Lambda,\in)\)を与えることを示すには\(o_{OT}\)の単射性を示す必要があり、それは\(o_{OT}\)の定義と同様に定義される文字列への写像がVeblen関数に付随する順序数表記への写像を定めることを示すことに帰着され、それは\(<_T\)に付随する全順序\(\leq_T\)に関して\(o_T\)が順序保存写像\((T,\leq_T) \to (\Lambda,\subset)\)となることを示すことと標準形のノードたちが\(\leq_T\)に関して降順に並ぶことなどに帰着され、そこそこ議論は面倒である。しかし停止性を示したいだけならばそんなことを示す必要はないのでこことでは扱わない。

定理（\(OT\)が\(\Lambda\)に対応すること）の証明

(1) \(a\)の長さに関する数学的帰納法で示す。

\(\textrm{Lng}(a) = 0\)ならば

\begin{eqnarray*} o_T(a) = o_T(()) = 0 \end{eqnarray*}

であるので確かに\((o_T(a[n]_T))_{n \in \textrm{cof}(o_T(a))}\)は空列\((o_T(a[n]_T))_{n \in 0}\)に他ならず\(o_T(a) = 0\)の基本列である。

\(a = (0)\)ならば

\begin{eqnarray*} o_T(a) = o_T((0)) = \varphi_0(0) = 1 \end{eqnarray*}

かつ任意の\(n \in \textrm{cof}(o_T(a)) = \textrm{cof}(1) = 1\)に対し

\begin{eqnarray*} o_T(a[n]_T) = o_T(()) = 0 \end{eqnarray*}

であるので確かに\((o_T(a[n]_T))_{n \in \textrm{cof}(o_T(a))}\)は長さ\(1\)の列\((0)_{n \in 1}\)に他ならず\(o_T(a) = 1\)の基本列である。

\(a = (0,\omega)\)ならば

\begin{eqnarray*} o_T(a) = o_T((0,\omega)) = \varphi_{\omega}(0) \end{eqnarray*}

かつ任意の\(n \in \textrm{cof}(o_T(a)) = \textrm{cof}(\varphi_{\omega}(0)) = \omega\)に対し

\begin{eqnarray*} o_T(a[n]_T) = o_T((0,n)) = \varphi_n(0) \end{eqnarray*}

であるので確かに\((o_T(a[n]_T))_{n \in \textrm{cof}(o_T(a))}\)は無限列\((\varphi_n(0))_{n \in \omega}\)に他ならず\(o_T(a) = \varphi_{\omega}(0)\)の基本列である。

\(\textrm{Lng}(a) > 0\)かつ\(a \notin \{(0),(0,\omega)\}\)とする。

\(\textrm{Lng}(L(a)) = 0 \)とする。

\(a = R(a) \in PT\)であり、\(\textrm{RightmostNode}\)の定義から\(\delta(a) \neq 0\)であり、\(a[n]_T\)の計算は分岐4を通る。

\(\textrm{RightmostNode}(a) = \textrm{Lng}(a) - 1\)とする。

\(\textrm{TopRightmostNode}(a) = 0\)かつ\(G(a) = ()\)かつ\(B(a) = \mathcal{L}(a) = (a_i)_{i=0}^{\textrm{Lng}(a)-2}\)かつ\(\mathcal{R}(a) = (0)\)である。\(o_T\)の定義（分岐1）より

\begin{eqnarray*} o_T(a[0]_T) = o_T(G(a)) = o_T(()) = 0 \end{eqnarray*}

であり、\([]_T\)の定義より任意の\(m \in \mathbb{N}\)に対し

\begin{eqnarray*} a[m+1]_T & = & a[m]_T \frown \uparrow(B(a), m \Delta(a)) = a[m]_T \frown \uparrow(B(a), m(\delta(a) - 0 - 1)) \\ & = & a[m]_T \frown \uparrow(B(a),m(\delta(a) - 1)) = B(a) \frown \uparrow(a[m]_T,\delta(a) - 1) \end{eqnarray*}

である。特に\(\delta(a) > 1\)ならば、\(\textrm{RightmostNode}(a) = \textrm{Lng}(a) - 1\)かつ

\begin{eqnarray*} (a[m+1]_T)_{\textrm{Lng}(a)-1} = (a[m]_T)_0 + (\delta(a) - 1) = \delta(a) - 1 < \delta(a) = a_{\textrm{RightmostNode}(a)} = a_{\textrm{Lng}(a)-1} \end{eqnarray*}

より\(\textrm{RightmostNode}(a[m+1]_T) = \textrm{Lng}(a) - 1\)となる。

\(o_T(\mathcal{L}(a)) = \varphi_{\delta(a)-1}(\alpha)\)を満たす\(\alpha \in \varphi_{\omega}(0)\)が存在するとする。

\(o_T(B(a)) = o_T(\mathcal{L}(a)) = \varphi_{\delta(a)-1}(\alpha)\)であり、また\(o_T\)の定義（分岐41）より

\begin{eqnarray*} o_T(a) = \varphi_{\delta(a)-1}(\alpha + o_T((0))) = \varphi_{\delta(a)-1}(\alpha + 1) \end{eqnarray*}

である。特に\(\textrm{cof}(o_T(a)) = \omega\)である。

\(\delta(a) = 1\)とする。

任意の\(n \in \mathbb{N}\)に対し

\begin{eqnarray*} o_T(a[n]_T) = \varphi_0(\alpha) \times n \end{eqnarray*}

が成り立つことを\(n\)に関する数学的帰納法で示す。

\(n = 0\)ならば、既に確認したように

\begin{eqnarray*} o_T(a[n]_T) = o_T(a[0]_T) \textcolor{red}{=} 0 = \varphi_0(\alpha) \times n \end{eqnarray*}

である。

\(n > 0\)ならば、\(o_T\)が加法的であることと\(n\)に関する数学的帰納法の仮定から

\begin{eqnarray*} o_T(a[n]_T) & = & o_T(a[n-1]_T \frown \uparrow(B(a),m(\delta(a) - 1))) = o_T(a[n-1]_T \frown B(a)) \textcolor{red}{=} o_T(a[n-1]_T) + o_T(B(a)) \\ & \textcolor{blue}{=} & \varphi_0(\alpha) \times (n-1) + \varphi_0(\alpha) = \varphi_0(\alpha) \times n \end{eqnarray*}

である。

以上より確かに\((o_T(a[n]_T))_{n \in \textrm{cof}(o_T(a))}\)は無限列\((\varphi_0(\alpha) \times n)_{n \in \omega}\)に他ならず\(o_T(a) = \varphi_0(\alpha+1)\)の基本列である。

\(\delta(a) > 1\)とする。

写像

\begin{eqnarray*} \Lambda & \to & \Lambda \\ \xi & \mapsto & \varphi_{\delta(a)-1}(\alpha + \xi) \end{eqnarray*}

を\(f\)と置く。任意の\(n \in \mathbb{N}\)に対し

\begin{eqnarray*} o_T(a[n]_T) = f^n(0) \end{eqnarray*}

が成り立つことを\(n\)に関する数学的帰納法で示す。

\(n = 0\)ならば、既に確認したように

\begin{eqnarray*} o_T(a[n]_T) = o_T(a[0]_T) \textcolor{red}{=} 0 = f^0(0) \end{eqnarray*}

である。

\(n > 0\)ならば、\(\textrm{RightmostNode}(a[n]_T) = \textrm{Lng}(a) - 1\)かつ\(\textrm{Lng}(B(a)) = \textrm{Lng}(a) - 2\)と\(n\)に関する数学的帰納法の仮定より

\begin{eqnarray*} o_T(a[n]_T) & = & o_T(B(a) \frown \uparrow(a[n-1]_T,\delta(a) - 1)) \textcolor{red}{=} \varphi_{\delta(a)-1}(\alpha + o_T(a[n-1]_T)) = \varphi_{\delta(a)-1}(o_T(a[n-1]_T)) \\ & = & f(o_T(a[n-1]_T)) \textcolor{blue}{=} f(f^{n-1}(0)) = f^n(0) \end{eqnarray*}

である。

以上より確かに\((o_T(a[n]_T))_{n \in \textrm{cof}(o_T(a))}\)は無限列\((f^n(0))_{n \in \omega}\)に他ならず\(o_T(a) = \varphi_{\delta(a)-1}(\alpha + 1)\)の基本列である。

\(o_T(\mathcal{L}(a)) = \varphi_{\delta(a)-1}(\alpha)\)を満たす\(\alpha \in \varphi_{\omega}(0)\)が存在しないとする。

\(o_T\)の定義（分岐42）より\(B(a) = \mathcal{L}(a) = (0)\)かつ\(\delta(a) > 1\)であり、\(a = (0,\delta(a))\)かつ\(o_T(a) = \varphi_{\delta(a)-1}(0)\)である。任意の\(n \in \mathbb{N}\)に対し

\begin{eqnarray*} o_T(a[n]_T) = \left\{ \begin{array}{ll} 0 & (n=0) \\ 1 & (n=1) \\ \varphi_{\delta(a)-1}^{n-1}(0) & (n>1) \end{array} \right. \end{eqnarray*}

が成り立つことを\(n\)に関する数学的帰納法で示す。

\(n = 0\)ならば、既に確認したように

\begin{eqnarray*} o_T(a[n]_T) = o_T(a[0]_T) = 0 = \varphi_{\delta(a)-1}^n(0) \end{eqnarray*}

であるのでよい。

\(n = 1\)ならば、

\begin{eqnarray*} o_T(a[n]_T) = o_T((0,\delta(a))[1]_T) = o_T((0)) = \varphi_0(0) = 1 \end{eqnarray*}

であるのでよい。

\(n = 2\)ならば、

\begin{eqnarray*} o_T(a[n]_T) = o_T((0,\delta(a))[2]_T) = o_T((0,\delta(a)-1)) = \varphi_{\delta(a)-1}(0) = \varphi_{\delta(a)-1}^{n-1}(0) \end{eqnarray*}

であるのでよい。

\(n > 2\)ならば、\(\varphi_{\delta(a)-1}^{n-2}(0) = 1 + \varphi_{\delta(a)-1}^{n-2}(0)\)かつ\(\textrm{RightmostNode}(a[n]_T) = \textrm{Lng}(a) - 1\)かつ\(\textrm{Lng}(B(a)) = \textrm{Lng}(a) - 2\)と\(n\)に関する数学的帰納法の仮定より

\begin{eqnarray*} o_T(a[n]_T) & = & o_T(B(a) \frown \uparrow(a[n-1]_T,\delta(a) - 1)) \textcolor{red}{=} \varphi_{\delta(a)-1}(0 + o_T(a[n-1]_T)) = \varphi_{\delta(a)-1}(o_T(a[n-1]_T)) \\ & \textcolor{blue}{=} & \varphi_{\delta(a)-1}(\varphi_{\delta(a)-1}^{n-2}(0)) = \varphi_{\delta(a)-1}^{n-1}(0) \end{eqnarray*}

である。

以上より確かに\((o_T(a[n]_T))_{n \in \textrm{cof}(o_T(a))}\)は\(o_T(a) = \varphi_{\delta(a)}(0)\)の基本列である。

\(\textrm{RightmostNode}(a) < \textrm{Lng}(a) - 1\)とする。

\(\textrm{RightmostNode}(a) < \textrm{Lng}(a) - 1\)より\(\textrm{Lng}(\mathcal{R}(a) > 1\)であるので\(o_T(\mathcal{R}(a)) \notin \{0,1\}\)である。\(\mathcal{R}(a) \in PT_{<(0,\omega)}\)であることと\(o_T\)の定義（分岐4）から\(o_T(\mathcal{R}(a)\)はadditive principalな順序数となり、\(o_T(\mathcal{R}(a)) \notin \{0,1\}\)であることから\(o_T(\mathcal{R}(a)) = 1 + o_T(\mathcal{R}(a))\)かつ\(\textrm{cof}(o_T(\mathcal{R}(a))) = \omega\)である。

また\(\textrm{Lng}(\mathcal{R}(a)) < \textrm{Lng}(a)\)より帰納法の仮定から\((o_T(\mathcal{R}(a)[n]_T))_{n \in \textrm{cof}(o_T(\mathcal{R}(a)))} = (o_T(\mathcal{R}(a)[n]_T))_{n \in \omega}\)は\(o_T(\mathcal{R}(a))\)の基本列をなす。

\(\textrm{RightmostNode}(a) < \textrm{Lng}(a) - 1\)より\(\mathcal{R}(a) \neq (0)\)であるので\(B(a) = \uparrow(B(\mathcal{R}(a)),\delta(a))\)であり、従って\([]_T\)の定義より

\begin{eqnarray*} a[n]_T = (\mathcal{L}(a) \frown \uparrow(\mathcal{R}(a),\delta(a)))[n]_T \textcolor{red}{=} \mathcal{L}(a) \frown \uparrow(\mathcal{R}(a)[n]_T,\delta(a)) \end{eqnarray*}

となり、更に

\begin{eqnarray*} (\mathcal{L}(a) \frown \uparrow(\mathcal{R}(a)[n]_T,\delta(a)))_{\textrm{RightmostNode}(a)} = (\mathcal{R}(a)[n]_T)_0 + \delta(a) = \delta(a) = a{\textrm{RightmostNode}(a)} \end{eqnarray*}

であるので

\begin{eqnarray*} \textrm{RightmostNode}(a[n]_T) = \textrm{RightmostNode}(a) \end{eqnarray*}

となる。

\(o_T(\mathcal{L}(a)) = \varphi_{\delta(a)-1}(\alpha)\)を満たす\(\alpha \in \varphi_{\omega}(0)\)が存在するとする。

\(o_T\)の定義（分岐41）より

\begin{eqnarray*} o_T(a) = \varphi_{\delta(a)-1}(\alpha + o_T(\mathcal{R}(a))) \end{eqnarray*}

である。従って\(\textrm{cof}(o_T(\mathcal{R}(a))) = \omega\)より

\begin{eqnarray*} \textrm{cof}(o_T(a)) = \textrm{cof}(\varphi_{\delta(a)-1}(\alpha + o_T(\mathcal{R}(a)))) = \omega \end{eqnarray*}

である。既に示したように

\begin{eqnarray*} a[n]_T & = & \mathcal{L}(a) \frown \uparrow(\mathcal{R}(a)[n]_T,\delta(a)) \\ \textrm{RightmostNode}(a[n]_T) & = & \textrm{RightmostNode}(a) \end{eqnarray*}

であるので、\(o_T\)の定義（分岐41）より

\begin{eqnarray*} o_T(a[n]_T) = o_T(\mathcal{L}(a) \frown \uparrow(\mathcal{R}(a)[n]_T,\delta(a))) \textcolor{red}{=} \varphi_{\delta(a)-1}(\alpha + o_T(\mathcal{R}(a)[n]_T)) \end{eqnarray*}

である。以上より\((o_T(a[n]_T))_{n \in \textrm{cof}(o_T(a))}\)は無限列\((\varphi_{\delta(a)-1}(\alpha + o_T(\mathcal{R}(a)[n]_T)))_{n \in \omega}\)に他ならず、\((o_T(\mathcal{R}(a)[n]_T))_{n \in \omega}\)が\(o_T(\mathcal{R}(a))\)の基本列をなすことと\(\varphi_{\delta(a)-1}\)の連続性から、これは確かに\(o_T(a) = \varphi_{\delta(a)-1}(\alpha + o_T(\mathcal{R}(a)))\)の基本列である。

\(o_T(\mathcal{L}(a)) = \varphi_{\delta(a)-1}(\alpha)\)を満たす\(\alpha \in \varphi_{\omega}(0)\)が存在しないとする。

\(o_T(\mathcal{R}(a)) = 1 + o_T(\mathcal{R}(a))\)であることと\(o_T\)の定義（分岐41）より

\begin{eqnarray*} o_T(a) = \varphi_{\delta(a)-1}(o_T(\mathcal{R}(a))) \end{eqnarray*}

である。既に示したように

\begin{eqnarray*} a[n]_T & = & \mathcal{L}(a) \frown \uparrow(\mathcal{R}(a)[n]_T,\delta(a)) \\ \textrm{RightmostNode}(a[n]_T) & = & \textrm{RightmostNode}(a) \end{eqnarray*}

であるので、\(o_T\)の定義（分岐42）より

\begin{eqnarray*} o_T(a[n]_T) = o_T(\mathcal{L}(a) \frown \uparrow(\mathcal{R}(a)[n]_T,\delta(a))) \textcolor{red}{=} \varphi_{\delta(a)-1}(o_T(\mathcal{R}(a)[n]_T)) \end{eqnarray*}

である。以上より\((o_T(a[n]_T))_{n \in \textrm{cof}(o_T(a))}\)は無限列\((\varphi_{\delta(a)-1}(o_T(\mathcal{R}(a)[n]_T)))_{n \in \omega}\)に他ならず、\((o_T(\mathcal{R}(a)[n]_T))_{n \in \omega}\)が\(o_T(\mathcal{R}(a))\)の基本列をなすことと\(\varphi_{\delta(a)-1}\)の連続性から、これは確かに\(o_T(a) = \varphi_{\delta(a)-1}(o_T(\mathcal{R}(a)))\)の基本列である。

\(\textrm{Lng}(L(a)) \neq 0\)とする。

\(o_T\)の加法性より

\begin{eqnarray*} o_T(a) = o_T(L(a) \frown R(a)) = o_T(L(a)) + o_T(R(a)) \end{eqnarray*}

であり、\(R(a) \in PT_{<(0,\omega)}\)より\(R(a) \neq ()\)であるので\(o_T\)の定義から\(o_T(R(a)) \neq 0\)である。従って

\begin{eqnarray*} \textrm{cof}(o_T(a)) = \textrm{cof}(o_T(R(a))) \end{eqnarray*}

である。また\(B(a)\)の定義より

\begin{eqnarray*} a[n]_T = L(a) \frown R(a)[n]_T \end{eqnarray*}

であり、\(o_T\)が加法的であることから

\begin{eqnarray*} o_T(a[n]_T) = o_T(L(a) \frown R(a)[n]_T) \textcolor{red}{=} o_T(L(a)) + o_T(R(a)[n]_T) \end{eqnarray*}

となる。\(\textrm{Lng}(R(a)) = \textrm{Lng}(a) - \textrm{Lng}(L(a)) < \textrm{Lng}(a)\)より数学的帰納法の仮定から\((o_T(R(a)[n]_T))_{n \in \textrm{cof}(o_T(R(a)))}\)は\(o_T(R(a))\)の基本列となるので、\(o_T(R(a)) \neq 0\)かつ\(\textrm{cof}(o_T(a)) = \textrm{cof}(o_T(R(a)))\)であることから\((o_T(a[n]_T))_{n \in \textrm{cof}(o_T(a))}\)は確かに\(o_T(a)\)の基本列である。

(2) (1)より\(o_T\)は順序保存写像\((T,<_{T,[]_T}) \to (\Lambda,\in)\)を定める。従って\(o_T\)の\(T_a\)への制限の像を\(X\)と置くと\(X \subset o_T(a)\)であり、かつ\(o_T\)の制限が全射順序保存写像\((T_a,<_{a,[]_T}) \to (X,\in)\)を定める。\(X \neq o_T(a)\)と仮定して矛盾を導く。

仮定より\(o_T(a) \setminus X\)は空でないので、\(o_T(a)\)の整礎性から\(o_T(a) \setminus X\)の最小元\(\alpha\)が存在する。自然数列\((n_i)_{i \in \mathbb{N}}\)を以下のように再帰的に定める：

• 任意の\(i \in \mathbb{N}\)に対し、(1)と\(\alpha \notin X\)より\(\{m \in \mathbb{N} \mid \alpha \in o_T(\textrm{Expand}(a,(n_j)_{j=0}^{i-1} \frown (m)))\)が空でないので\(n_i\)をその最小値と定める。

すると\(o_T\)が順序保存写像\((T,<_{T,[]_T}) \to (\Lambda,\in)\)であることから\((o_T(\textrm{Expand}(a,(n_j)_{j=0}^{i})))_{i \in \mathbb{N}}\)が\(\Lambda\)の無限降下列となり、\(\Lambda\)の整礎性に反し矛盾する。以上より\(X = o_T(a)\)である。□

というわけで本題の亜原始数列の停止性を示す準備が整った。

系（亜原始数列の停止性）
\(S\)は全域である。

証明

定理（\(OT\)が\(\Lambda\)に対応すること）(1)と\((\Lambda,\in)\)の整礎性より即座に従う。□