ペア数列システムの停止性証明に用いられた変換写像の全単射性

ペア数列システムの停止性^[1]にて定義された写像$\textrm{Trans}$が全単射であることを示す。

背景[]

ペア数列システムはp進大好きbot氏によってBuchholzの表記系へ対応させる写像$\textrm{Trans}$によって停止性が証明されている^[1]。しかし、これは基本列によって定められる大小関係が線形であることや、任意の行列未満の標準形である行列の順序形、つまり行列が実際に何に対応するかはわからない。しかし、基本列の順序数への像が基本列であることを示すことで全射性が得られると教わった^[2]:

別に挟まなくても、任意のn∈Nに対しTrans(M[n]) < Trans(M)であることさえ分かっていれば、任意のn∈Nに対しあるa∈N（nに依存して良い）が存在してTrans(M)[n] < Trans(M[n+a])となることをいうだけでOKです。

実際に使うのはこれが厳密に書かれている^[3]の命題11である。

幸いにも、基本列の関係の証明に見られるようにすでに必要なものは揃っている。脚注の一つに「当初の予定ではペア数列の解析、すなわちペア数列システムに伴う順序数表記系の限界を決定するつもりだったが」とあるように^[1]、この記事でしたような議論をする予定であったことが推測できる。新たに全単射であるような$\textrm{Trans2}$を定義しなければならないようなことにならず安心した。

表記[]

^[1]より次の記法を用いる。

$\mathbb{N}$ - 非負整数全体の集合
$\mathbb{N}_+$ - 正整数全体の集合
$\textrm{Lng}(a)$ - $a$の長さ
$a\oplus_Ab$ - 2つの配列の結合
$\bigoplus_Aa$ - 配列の成分の結合
$M_{i,j}$ - 2次元配列の要素
$T_{\textrm{PS}}$ - ペア数列全体の集合
$PT_{\textrm{PS}}$ - 単項なペア数列全体の集合
$MT_{\textrm{PS}}$ - 複項なペア数列全体の集合
$ST_{\textrm{PS}}$ - 広い意味で標準形なペア数列全体の集合
$S_kT_{\textrm{PS}}$ - 広い意味で標準形であり基本列を$k$回取ることで得られるペア数列全体の集合
$\textrm{Pred}(M)$ - ペア数列の前者
$P(M)\mid M\in T_{\textrm{PS}}$ - ペア数列の単項成分
$M[n]\mid M\in T_{\textrm{PS}}$ - ペア数列の基本列
$T_{\textrm{B}}$ - $D_\omega$を含まないBuchholozの表記系の部分集合
$PT_{\textrm{B}}$ - $D_\omega$を含まない単項なBuchholozの表記系全体の集合
$MT_{\textrm{B}}$ - $D_\omega$を含まない複項なBuchholozの表記系全体の集合
$OT_{\textrm{B}}$ - $D_\omega$を含まない順序数項であるBuchholozの表記系全体の集合
$\underline{(}$、$\underline{,}$、$\underline{)}$ - Buchholozの表記系の字母
$P(t)\mid t\in T_{\textrm{B}}$ - Buchholozの表記系の単項成分
$T_{\textrm{B}}$上の$+$、$\times$、$\textrm{dom}$、$[]$
$\Sigma_{\textrm{B}}$ - Buchholozの表記系の総和
$\Sigma$ - $D_\omega$を含まないBuchholozの表記系の字母
$\textrm{Trans}$

$T_{\textrm{B}}$上の$<$と$\leq$は区別のため$<_{\textrm{B}}$と$\leq_{\textrm{B}}$と書く。

^[4]及び^[5]も参照。

^[4]より次の記法を用いる。

$\psi_ua$
$D_ua$
$G_ua$
$o$

$OT_{\textrm{B}\omega}$を^[4]の(字母$D_\omega$を許容する)$OT$とする。

$CT_{\textrm{PS}}=\{M\mid M\in ST_{\textrm{PS}}\land M_0=(0,0)\}$とする。

$T_{\textrm{PS}}^2$上の関係$<_{\textrm{PS}}$を以下のように再帰的に定める。

任意の$M,N\in T_{\textrm{PS}}$に対して、$M<_{\textrm{PS}}N$は次のいずれかが成り立つことと同値である。
1. $M_{0,0}< N_{0,0}$である。
2. $M_{0,0}=N_{0,0}$かつ$M_{1,0}< N_{1,0}$である。
3. $M_{0,0}=N_{0,0}$かつ$M_{1,0}=N_{1,0}$かつ$(M_i)_{i=1}^{\textrm{Lng}(M)-1}<_{\textrm{PS}}(N_i)_{i=1}^{\textrm{Lng}(N)-1}$である。

任意の$M,N\in T_{\textrm{PS}}$に対して$M\leq_{\textrm{PS}}N$を$M=N\lor M<_{\textrm{PS}}N$の略記とする。

証明[]

系 (辞書式的順序が辞書式順序であること)
$<_{\textrm{lex}}$を数列に対する辞書式順序としたとき、任意の$M,N\in T_{\textrm{PS}}$に対して、$M<_{\textrm{PS}}N$は$\bigoplus_\mathbb{N}M<_{\textrm{lex}}\bigoplus_\mathbb{N}N$と同値である。

証明: $<_{\textrm{PS}}$の定義から即座に従う。□

系 (辞書式的順序の線形性)
$<_{\textrm{PS}}$は狭義全順序、$\leq_{\textrm{PS}}$は全順序である。

証明: 辞書式的順序が辞書式順序であることより即座に従う。□

命題 (基本列的順序が推移性)
$<_{\textrm{PS}[]}$及び$\leq_{\textrm{PS}[]}$は推移律を満たす。

証明: 任意の$M,N,O\in T_{\textrm{PS}}$を取り、$M\leq_{\textrm{PS}[]}N$かつ$N\leq_{\textrm{PS}[]}O$であるとする。; $\leq_{\textrm{PS}[]}$の定義より、ある$a,b\in\mathbb{N}_+^{<\omega}$が存在して$M=N[a_0]\cdots[a_{\textrm{Lng}(a)-1}]$かつ$N=O[b_0]\cdots[b_{\textrm{Lng}(b)-1}]$である。; 上より$M=O[b_0]\cdots[b_{\textrm{Lng}(b)-1}][a_0]\cdots[a_{\textrm{Lng}(a)-1}]$であるから$M\leq_{\textrm{PS}[]}O$である。; 従って$\leq_{\textrm{PS}[]}$は推移律を満たす。また$<_{\textrm{PS}[]}$の推移性も同様に導かれる。□

命題 (基本列の辞書式的縮小性)
任意の$M\in T_{\textrm{PS}}$と$n\in\mathbb{N}_+$に対して、$\textrm{Lng}(M)>1$ならば$M[n]<_{\textrm{PS}}M$である。

証明

$\textrm{operator}[]$の定義中の記号を$M$に対して定義する。

条件より$j_1>0$である。

$M[n]=\textrm{Pred}(M)$ならば明らかに$M[n]<_{\textrm{PS}}M$である。

よって$M_{j_1}\neq(0,0)$かつある非負整数$j_0$が存在して$(i_1,j_0)<^\textrm{Next}_M(i_1,j_1)$であるとする。

^[1]の$\textrm{Pred}$が$[1]$で表されることより$n=1$ならば$M[n]=\textrm{Pred}(M)$であり、$M[n]=\textrm{Pred}(M)$の場合は考えなくていいから$n>1$とする。

$$\begin{align}M[n]&=G\oplus_{\mathbb{N}^2}\left(\bigoplus_{\mathbb{N}^2}B\right)\\&=G\oplus_{\mathbb{N}^2}B_0\oplus_{\mathbb{N}^2}\left(\bigoplus_{\mathbb{N}^2}(B_i)_{i=1}^{n-1}\right)\\&=(M_j)_{j=0}^{j_0-1}\oplus_{\mathbb{N}^2}(M_j)_{j=j_0}^{j_1-1}\oplus_{\mathbb{N}^2}\left(\bigoplus_{\mathbb{N}^2}(B_i)_{i=1}^{n-1}\right)\\&=(M_j)_{j=0}^{j_1-1}\oplus_{\mathbb{N}^2}\left(\bigoplus_{\mathbb{N}^2}(B_i)_{i=1}^{n-1}\right)\end{align}$$である。

よって$M[n]<_{\textrm{PS}}M$は$\bigoplus_{\mathbb{N}^2}(B_i)_{i=1}^{n-1}<_{\textrm{PS}}(M_{j_1})$と同値である。

$\left(\bigoplus_{\mathbb{N}^2}(B_i)_{i=1}^{n-1}\right)_0=(B_1)_0=(M_{0,j_0}+\delta_0,M_{1,j_0}+\delta_1)$である。

$i_1=0$とする。

$(M_{0,j_0}+\delta_0,M_{1,j_0}+\delta_1)=(M_{0,j_0},M_{1,j_0})$である。

$<^\textrm{Next}$の定義より、$M_{0,j_0}< M_{0,j_1}$である。

よって$\bigoplus_{\mathbb{N}^2}(B_i)_{i=1}^{n-1}<_{\textrm{PS}}(M_{j_1})$である。

$i_1=1$とする。

$(M_{0,j_0}+\delta_0,M_{1,j_0}+\delta_1)=(M_{0,j_1},M_{1,j_0})$である。

$<^\textrm{Next}$の定義より、$M_{1,j_0}< M_{1,j_1}$である。

よって$\bigoplus_{\mathbb{N}^2}(B_i)_{i=1}^{n-1}<_{\textrm{PS}}(M_{j_1})$である。

よっていずれの場合でも$\bigoplus_{\mathbb{N}^2}(B_i)_{i=1}^{n-1}<_{\textrm{PS}}(M_{j_1})$である。

従って$M[n]<_{\textrm{PS}}M$である。

よっていずれの場合でも$M[n]<_{\textrm{PS}}M$である。□

命題 (辞書式的順序が基本列的順序を含意すること)
任意の$M,N\in CT_{\textrm{PS}}$に対して、$M<_{\textrm{PS}[]}N$ならば$M<_{\textrm{PS}}N$である。

証明: $<_{\textrm{PS}[]}$の定義よりある$a\in\mathbb{N}_+^{<\omega}\setminus\{()\}$が存在して$M=N[a_0]\cdots[a_{\textrm{Lng}(a)-1}]$である。; $N=(0,0)$とすると、任意の$n\in\mathbb{N}_+$に対して$N[n]=N$であるから、$M=N$となり、これは条件と反するから$N\neq(0,0)$である。; 上より$\textrm{Lng}(N)>1$である。; 任意の非負整数$i<\textrm{Lng}(a)$に対して$Q_0=N$、$Q_{i+1}=Q_i[a_i]$とする。; よって基本列の辞書式的縮小性より$Q_1=N[a_0]<_{\textrm{PS}}N$である。; 任意の非負整数$1\leq i<\textrm{Lng}(a)$をとり、$Q_i<_{\textrm{PS}}N$と仮定すると、辞書式的順序の線形性及び基本列の辞書式的縮小性より$Q_{i+1}=Q_i[a_i]\leq_{\textrm{PS}}Q_i<_{\textrm{PS}}N$である。; 帰納法により任意の非負整数$1\leq i\leq\textrm{Lng}(a)$に対して$Q_i<_{\textrm{PS}}N$である。; よって$M=Q_{\textrm{Lng}(a)}<_{\textrm{PS}}N$である。□

命題 (基本列の切片の不変性)
任意の$M\in T_{\textrm{PS}}$と$j_0,j_1\in\mathbb{N}$と$m,n\in\mathbb{N}_+$に対して、$j_0\leq j_1$かつ$j_1<\textrm{Lng}(M[m])$かつ$j_1<\textrm{Lng}(M[n])$ならば$(M[m]_j)_{j=j_0}^{j_1}=(M[n]_j)_{j=j_0}^{j_1}$である。

証明

$\textrm{operator}[]$の定義中の記号を$M$に対して定義する。

$M[m]=M[n]$ならば明らかに$(M[m]_j)_{j=j_0}^{j_1}=(M[n]_j)_{j=j_0}^{j_1}$である。

よって$m\neq n$かつ$j_1>0$かつ$M_{j_1}\neq(0,0)$かつある非負整数$j_0$が存在して$(i_1,j_0)<^\textrm{Next}_M(i_1,j_1)$であるとする。

命題が$m$と$n$に対して対称であることから$m< n$である場合のみ考えればいい。

$$\begin{align}(M[n]_j)_{j=0}^{\textrm{Lng}(M[m])-1}&=(G\oplus_{\mathbb{N}^2}\left(\bigoplus_{\mathbb{N}^2}B\right))_{j=0}^{\textrm{Lng}(M[m])-1}\\&=(G\oplus_{\mathbb{N}^2}\left(\bigoplus_{\mathbb{N}^2}(B_k)_{k=0}^{m-1}\right)\oplus_{\mathbb{N}^2}\left(\bigoplus_{\mathbb{N}^2}(B_k)_{k=m}^{n-1}\right))_{j=0}^{\textrm{Lng}(M[m])-1}\\&=(M[m]\oplus_{\mathbb{N}^2}\left(\bigoplus_{\mathbb{N}^2}(B_k)_{k=m}^{n-1}\right))_{j=0}^{\textrm{Lng}(M[m])-1}\\&=M[m]\end{align}$$である。

$j_0\leq j_1<\textrm{Lng}(M[m])$であるから、上より$(M[n]_j)_{j=j_0}^{j_1}=(((M[n]_j)_{j=0}^{\textrm{Lng}(M[m])-1})_j)_{j=j_0}^{j_1}=(M[m]_j)_{j=j_0}^{j_1}$である。

よっていずれの場合でも$(M[m]_j)_{j=j_0}^{j_1}=(M[n]_j)_{j=j_0}^{j_1}$である。□

命題 (展開と$\textrm{Pred}$の関係)
任意の$M\in T_{\textrm{PS}}$と$n\in\mathbb{N}_+$に対し、$j_1=\textrm{Lng}(M)-1$と置くと、$\textrm{Lng}(M[n])\geq j_1$かつ$(M[n]_j)_{j=0}^{j_1-1}=\textrm{Pred}(M)$である。

証明

$\textrm{operator}[]$の定義中の記号を$M$に対して定義する。

$M[n]=M$または$M[n]=\textrm{Pred}(M)$ならば明らかに$\textrm{Lng}(M[n])\geq j_1$かつ$(M[n]_j)_{j=0}^{j_1-1}=\textrm{Pred}(M)$である。

よって$j_1>0$かつ$M_{j_1}\neq(0,0)$かつある非負整数$j_0$が存在して$(i_1,j_0)<^\textrm{Next}_M(i_1,j_1)$であるとする。

$$\begin{align}\textrm{Lng}(M[n])&=\textrm{Lng}(G\oplus_{\mathbb{N}^2}\left(\bigoplus_{\mathbb{N}^2}B\right))\\&=j_0+n(j_1-j_0)\\&\geq j_1\end{align}$$である。

^[1]の$\textrm{Pred}$が$[1]$で表されること及び基本列の切片の不変性より$(M[n]_j)_{j=0}^{j_1-1}=\textrm{Pred}(M)$である。

よっていずれの場合でも$\textrm{Lng}(M[n])\geq j_1$かつ$(M[n]_j)_{j=0}^{j_1-1}=\textrm{Pred}(M)$である。□

補題 (最左列の不変性)
任意の$M,N\in T_{\textrm{PS}}$に対して、$M\leq_{\textrm{PS}[]}N$ならば$M_0=N_0$である。

証明

$\leq_{\textrm{PS}[]}$の定義よりある$a\in\mathbb{N}_+^{<\omega}$が存在して$M=N[a_0]\cdots[a_{\textrm{Lng}(a)-1}]$である。

任意の非負整数$i<\textrm{Lng}(a)$に対して$Q_0=N$、$Q_{i+1}=Q_i[a_i]$とする。

$(Q_0)_0=N_0$である。

任意の非負整数$k<\textrm{Lng}(a)$を取り、$(Q_k)_0=N_0$であると仮定する。

$\textrm{Lng}(Q_k)=1$ならば$(Q_{k+1})_0=(Q_k)_0=N_0$である。

$\textrm{Lng}(Q_k)>1$ならば展開と$\textrm{Pred}$の関係より$(Q_{k+1})_0=\textrm{Pred}(Q_k)_0=N_0$である。

よっていずれの場合でも$(Q_{k+1})_0=N_0$である。

帰納法により任意の非負整数$k\leq\textrm{Lng}(a)$に対して、$(Q_k)_0=N_0$である。

よって$M_0=(Q_{\textrm{Lng}(a)})_0=N_0$である。

補題 (標準形と基本列的順序の関係)
任意の$M\in T_{\textrm{PS}}$に対して、$M\in ST_{\textrm{PS}}$はある$u,v\in\mathbb{N}$が存在して$u\leq v$かつ$M\leq_{\textrm{PS}[]}((j,j))_{j=u}^v$であることと同値である。

証明: (⇒) 任意の$u,v\in\mathbb{N}$に対し、$u\leq v$ならば$((j,j))_{j=u}^v\leq_{\textrm{PS}[]}((j,j))_{j=u}^v$であるから、任意の$M\in S_0T_{\textrm{PS}}$に対して、ある$u,v\in\mathbb{N}$が存在して$u\leq v$かつ$M\leq_{\textrm{PS}[]}((j,j))_{j=u}^v$である。; 任意の$k\in\mathbb{N}$をとり、任意の$M\in S_kT_{\textrm{PS}}$に対して、ある$u,v\in\mathbb{N}$が存在して$u\leq v$かつ$M\leq_{\textrm{PS}[]}((j,j))_{j=u}^v$であると仮定すると、任意の$M\in S_{k+1}T_{\textrm{PS}}$に対して、ある$N\in S_kT_{\textrm{PS}}$が存在して$M\leq_{\textrm{PS}[]}N$であるから、基本列的順序が推移性よりある$u,v\in\mathbb{N}$が存在して$u\leq v$かつ$M\leq_{\textrm{PS}[]}((j,j))_{j=u}^v$である。; 帰納法により任意の$k\in\mathbb{N}$に対して、任意の$M\in S_kT_{\textrm{PS}}$に対して、ある$u,v\in\mathbb{N}$が存在して$u\leq v$かつ$M\leq_{\textrm{PS}[]}((j,j))_{j=u}^v$である。; $ST_{\textrm{PS}}=\bigcup_{k\in\mathbb{N}}S_kT_{\textrm{PS}}$であるから、任意の$M\in ST_{\textrm{PS}}$に対して、ある$u,v\in\mathbb{N}$が存在して$u\leq v$かつ$M\leq_{\textrm{PS}[]}((j,j))_{j=u}^v$である。; (⇐) $\leq_{\textrm{PS}[]}$の定義よりある$a\in\mathbb{N}_+^{<\omega}$が存在して$M=((j,j))_{j=u}^v[a_0]\cdots[a_{\textrm{Lng}(a)-1}]$である。; 任意の非負整数$i<\textrm{Lng}(a)$に対して$Q_0=((j,j))_{j=u}^v$、$Q_{i+1}=Q_i[a_i]$とする。; $Q_0=((j,j))_{j=u}^v\in ST_{\textrm{PS}}$である。; 任意の非負整数$k<\textrm{Lng}(a)$を取り、$Q_k\in ST_{\textrm{PS}}$であると仮定すると、$Q_{k+1}=Q_k[a_{k+1}]\in ST_{\textrm{PS}}$である。; 帰納法により任意の非負整数$k\leq\textrm{Lng}(a)$に対して、$Q_k\in ST_{\textrm{PS}}$である。; よって$M=Q_{\textrm{Lng}(a)}\in ST_{\textrm{PS}}$である。□

命題 (可算な標準形の起源)
任意の$M\in T_{\textrm{PS}}$に対して、$M\in CT_{\textrm{PS}}$はある$v\in\mathbb{N}$が存在して$M\leq_{\textrm{PS}[]}((j,j))_{j=0}^v$であることと同値である。

証明: (⇒) $ST_{\textrm{PS}}\subset CT_{\textrm{PS}}$であるから、標準形と基本列的順序の関係より、ある$u,v\in\mathbb{N}$が存在して$u\leq v$かつ$M\leq_{\textrm{PS}[]}((j,j))_{j=u}^v$である。; 最左列の不変性より$M_0=(u,u)$である。; $CT_{\textrm{PS}}$の定義より$M_0=(0,0)$である。; 従って$u=0$である。; よってある$v\in\mathbb{N}$が存在して$M\leq_{\textrm{PS}[]}((j,j))_{j=0}^v$である。; (⇐) 最左列の不変性より$M_0=(0,0)$である。; $M\in ST_{\textrm{PS}}$である。; よって$M\in CT_{\textrm{PS}}$である。□

補題 (標準形の始切片への経路)
任意の$M\in ST_{\textrm{PS}}$と$j_1'\in\mathbb{N}$に対し、$j_1=\textrm{Lng}(M)-1$と置くと、$j_1'\leq j_1$ならば$(M_j)_{j=0}^{j_1'}<_{\textrm{PS}[]}M$である。

証明: ^[1]の$\textrm{Pred}$が$[1]$で表されることより、帰納法により$(M_j)_{j=0}^{j_1'}=\textrm{Pred}^{j_1-j_1'}(M)=M[1]^{j_1-j_1'}<_{\textrm{PS}[]}M$であるから、$(M_j)_{j=0}^{j_1'}<_{\textrm{PS}[]}M$である。□

命題 (基本列的順序が辞書式的順序を含意すること)
任意の$M,N\in CT_{\textrm{PS}}$に対して、$M<_{\textrm{PS}}N$ならば$M<_{\textrm{PS}[]}N$である。

証明

$\textrm{operator}[]$の定義中の記号を$M$と$N$に対して定義し、それぞれ右肩に$M$と$N$を乗せて表記する。

$j_1^M=0$とする。

$CT_{\textrm{PS}}$の定義より$M=((0,0))=(N_j)_{j=0}^0$である。

標準形の始切片への経路より$M<_{\textrm{PS}[]}N$である。

$j_1^M>0$ならば、任意の$M',N'\in CT_{\textrm{PS}}$に対して、$\textrm{Lng}(M')<\textrm{Lng}(M)$かつ$M'<_{\textrm{PS}}N'$ならば$M'<_{\textrm{PS}[]}N'$であると仮定する。

$f=\min\{\min(j_1^M,j_1^N)+1\}\cup\{j\mid j\in\mathbb{N}\land j\leq\min(j_1^M,j_1^N)\land M_j\neq N_j\}$とする。

$f=j_1^M+1$ならば、$M=(N_j)_{j=0}^{j_1^M}$であるから標準形の始切片への経路より$M<_{\textrm{PS}[]}N$である。

$f\leq j_1^M$とする。

$M<_{\textrm{PS}}N$であるから$f\leq j_1^N$である。

$f=j_1^N$とする。

仮定より$j_1^N\leq j_1^M$である。

^[1]の簡約性と係数の関係、条件(A)と(B)と係数の基本性質(1)及び(2)、標準形の簡約性及び$CT_{\textrm{PS}}$の定義より任意の$M'\in CT_{\textrm{PS}}$に対して、$\textrm{Lng}(M')=\textrm{Lng}(N)$ならば$M'_{1,j_1^N}\leq M'_{0,j_1^N}\leq j_1^N$である。

任意の$M'\in CT_{\textrm{PS}}$に対して、$\textrm{Lng}(M')=\textrm{Lng}(N)$ならば$M'=(M'_j)_{j=0}^{j_1^N-1}\oplus((M'_{0,j_1^N},M'_{1,j_1^N}))$である。

従って$\textrm{Lng}(M')=\textrm{Lng}(N)$かつ$(M'_j)_{j=0}^{j_1^N-1}=(N_j)_{j=0}^{j_1^N-1}$である$M'\in CT_{\textrm{PS}}$は高々$(j_1^N)^2$個である。

任意の$M',N'\in CT_{\textrm{PS}}$に対して、$\textrm{Lng}(M')=\textrm{Lng}(N)$かつ$N\leq_{\textrm{PS}}M'<_{\textrm{PS}}N'$ならば$M'<_{\textrm{PS}[]}N'$であると仮定する。

可算な標準形の起源よりある$v^M,v^N\in\mathbb{N}$が存在して$M\leq_{\textrm{PS}[]}((j,j))_{j=0}^{v^M}$かつ$N\leq_{\textrm{PS}[]}((j,j))_{j=0}^{v^N}$である。

$v=\max(v^M,v^N)$とする。

標準形の始切片への経路より$((j,j))_{j=0}^{v^M}\leq_{\textrm{PS}[]}((j,j))_{j=0}^v$かつ$((j,j))_{j=0}^{v^N}\leq_{\textrm{PS}[]}((j,j))_{j=0}^v$である。

基本列的順序が推移性より$M\leq_{\textrm{PS}[]}((j,j))_{j=0}^v$かつ$N\leq_{\textrm{PS}[]}((j,j))_{j=0}^v$である。

$\leq_{\textrm{PS}[]}$の定義よりある$a\in\mathbb{N}_+^{<\omega}$が存在して$M=((j,j))_{j=0}^v[a_0]\cdots[a_{\textrm{Lng}(a)-1}]$である。

辞書式的順序が基本列的順序を含意することより$N\leq_{\textrm{PS}}((j,j))_{j=0}^v$である。

$M=((j,j))_{j=0}^v[a_0]\cdots[a_{\textrm{Lng}(a)-1}]\leq_{\textrm{PS}}N\leq_{\textrm{PS}}((j,j))_{j=0}^v$よりある$g\in\mathbb{N}$が存在して$g\leq\textrm{Lng}(a)$かつ$((j,j))_{j=0}^v[a_0]\cdots[a_g]<_{\textrm{PS}}N$であり、そのような$g$で最小のものを$g_0$とする。

$N'=((j,j))_{j=0}^v[a_0]\cdots[a_{g_0-1}]$とする。

辞書式的順序の線形性及び$g_0$の定義より$N\leq_{\textrm{PS}}N'$である。

$N<_{\textrm{PS}}N'$とする。

辞書式的順序が基本列的順序を含意することより$M<_{\textrm{PS}}N'[a_{g_0}]<_{\textrm{PS}}N$である。

$f$の定義及び仮定より$(M_j)_{j=0}^{j_1^N-1}=(N_j)_{j=0}^{j_1^N-1}$であるから、上より$\textrm{Lng}(N'[a_{g_0}])>j_1^N$かつ$(M_j)_{j=0}^{j_1^N-1}=(N'[a_{g_0}]_j)_{j=0}^{j_1^N-1}$である。

上より$(N'[a_{g_0}]_j)_{j=j_1^N}^{\textrm{Lng}(N'[a_{g_0}])-1}<_{\textrm{PS}}(N_j)_{j=j_1^N}^{j_1^N}=(N_{j_1^N})$であり、よって$(N'[a_{g_0}]_{j_1^N})<_{\textrm{PS}}(N_{j_1^N})$であるから、$(N'[a_{g_0}]_j)_{j=0}^{j_1^N}<_{\textrm{PS}}N$である。

任意の$n\in\mathbb{N}_+$を取る。

$\textrm{Lng}(N'[n])\leq j_1^N$ならば、基本列の切片の不変性より$N'[n]=(N'[a_{g_0}]_j)_{j=0}^{\textrm{Lng}(N'[n])-1}<_{\textrm{PS}}(N'[a_{g_0}]_j)_{j=0}^{j_1^N}<_{\textrm{PS}}N$である。

$\textrm{Lng}(N'[n])>j_1^N$ならば、基本列の切片の不変性より$(N'[n]_j)_{j=0}^{j_1^N}=(N'[a_{g_0}]_j)_{j=0}^{j_1^N}$であり、$(N'[a_{g_0}]_j)_{j=0}^{j_1^N}<_{\textrm{PS}}N$であるから、$<_{\textrm{PS}}$の定義より$N'[n]<_{\textrm{PS}}N$である。

従って任意の$n\in\mathbb{N}_+$に対して$N'[n]<_{\textrm{PS}}N$である。

辞書式的順序が基本列的順序を含意することより任意の$n\in\mathbb{N}_+$に対して$N<_{\textrm{PS}[]}N'[n]$ではない。

従って$N<_{\textrm{PS}[]}N'$ではない。

仮定より$N<_{\textrm{PS}[]}N'$であるが、これは上と矛盾する。

従って$N=N'$である。

よって$N[a_{g_0}]\cdots[a_{\textrm{Lng}(a)-1}]=M$であるから、$M<_{\textrm{PS}[]}N$である。

仮定より任意の$N'\in CT_{\textrm{PS}}$に対して、$N<_{\textrm{PS}}N'$ならば$N<_{\textrm{PS}[]}N'$である。

基本列的順序が推移性より、任意の$N'\in CT_{\textrm{PS}}$に対して、$N\leq_{\textrm{PS}}N'$ならば$M<_{\textrm{PS}[]}N'$である。

ある$M'\in CT_{\textrm{PS}}$が存在して、$\textrm{Lng}(M')=\textrm{Lng}(N)$かつ$(M'_j)_{j=0}^{j_1^N-1}=(N_j)_{j=0}^{j_1^N-1}$かつ$M'<_{\textrm{PS}}N$であるならば、そのようなもののうち$<_{\textrm{PS}}$に対する最大元をとる。

$M=M'$とした場合により、任意の$N'\in CT_{\textrm{PS}}$に対して、$N\leq_{\textrm{PS}}N'$ならば$M'<_{\textrm{PS}[]}N'$である。

任意の$O\in CT_{\textrm{PS}}$をとり、$M'<_{\textrm{PS}}O<_{\textrm{PS}}N$とする。

$<_{\textrm{PS}}$の定義より$M'\leq_{\textrm{PS}}(O_j)_{j=0}^{\min(\textrm{Lng}(O)-1,j_1^N)}<_{\textrm{PS}}N$である。

$(M'_j)_{j=0}^{j_1^N-1}=(N_j)_{j=0}^{j_1^N-1}$であるから、$\textrm{Lng}(O)\geq\textrm{Lng}(M')$かつ$(O_j)_{j=0}^{j_1^N-1}=(N_j)_{j=0}^{j_1^N-1}$である。

^[1]の標準形の始切片への遺伝性及び$CT_{\textrm{PS}}$の定義より$(O_j)_{j=0}^{j_1^N}\in CT_{\textrm{PS}}$である。

$M'$の最大性より、$(O_j)_{j=0}^{j_1^N}=M'$である。

標準形の始切片への経路より$M'=(O_j)_{j=0}^{j_1^N}\leq_{\textrm{PS}[]}O$である。

よって任意の$N'\in CT_{\textrm{PS}}$に対して、$M'<_{\textrm{PS}}N'$ならば$M'<_{\textrm{PS}[]}N'$である。

$\textrm{Lng}(N)$及び$(N_j)_{j=0}^{j_1^N-1}$を固定したときの帰納法により、任意の$N'\in CT_{\textrm{PS}}$に対して、$N\leq_{\textrm{PS}}N'$ならば$M<_{\textrm{PS}[]}N'$である。

よって$f=j_1^N$ならば、任意の$N'\in CT_{\textrm{PS}}$に対して、$N\leq_{\textrm{PS}}N'$ならば$M<_{\textrm{PS}[]}N'$である。

$f\leq j_1^N$であり、$f$の定義より$N$を$(N_j)_{j=0}^f$に置き換えても$f$が不変であり、$(N_j)_{j=0}^f\leq_{\textrm{PS}}N$であるから上より$M<_{\textrm{PS}[]}N$である。

よっていずれの場合でも$M<_{\textrm{PS}[]}N$である。

帰納法により任意の$M,N\in CT_{\textrm{PS}}$に対して、$M<_{\textrm{PS}}N$ならば$M<_{\textrm{PS}[]}N$である。□

系 (順序の等価性)
任意の$M,N\in CT_{\textrm{PS}}$に対して、$M\leq_{\textrm{PS}}N$は$M\leq_{\textrm{PS}[]}N$と同値である。

証明: 基本列的順序が辞書式的順序を含意すること及び辞書式的順序が基本列的順序を含意することより即座に従う。□

系 (順序の線形性)
$\leq_{\textrm{PS}}$及び$\leq_{\textrm{PS}[]}$は$CT_{\textrm{PS}}$上で全順序である。

証明: 辞書式的順序の線形性及び順序の等価性より即座に従う。□

命題 (後続な項の基本列)
任意の$M\in RT_{\textrm{PS}}$と$n\in\mathbb{N}_+$に対して、$\textrm{dom}(\textrm{Trans}(M))=1$ならば$(\textrm{Trans}(M),\textrm{Trans}(M[n]))=(D_00,0)$または$\textrm{Trans}(M[n])+D_00=\textrm{Trans}(M)$である。

証明

$T_{\textrm{B}}$上の$\textrm{dom}$の定義より、$\textrm{dom}(\textrm{Trans}(M))=1$ならば$\textrm{Trans}(M)=D_00$またはある$s\in\Sigma^{<\omega}$が存在して$\underline{(}s\underline{,}D_00\underline{)}$である。

$\textrm{Trans}(M)=D_00$とする。

^[1]の$\textrm{Trans}$と非可算基数の関係より$M=((0,0),(0,0))$である。

$(\textrm{Trans}(M),\textrm{Trans}(M[n]))=(D_00,\textrm{Trans}(((0,0))))=(D_00,0)$である。

ある$s\in\Sigma^{<\omega}$が存在して$\underline{(}s\underline{,}D_00\underline{)}$であるとする。

$\textrm{Trans}(M)=\underline{(}s\underline{,}D_00\underline{)}$は複項である。

$P(M)_0$が零項でありかつ$\textrm{Lng}(P(M))=2$であるとすると、^[1]の$\textrm{Trans}$が零項性を保つことより$\textrm{Trans}(M)=\textrm{Trans}(P(M)_0)+\textrm{Trans}(P(M)_1)=0+\textrm{Trans}(P(M)_1)=\textrm{Trans}(P(M)_1)$であり、^[1]の$P$の各成分の非複項性、$\textrm{Trans}$が零項性を保つこと及び$\textrm{Trans}$が単項性を保つことより$\textrm{Trans}(M)=0$または$\textrm{Trans}(M)$は単項であるが、これは上と矛盾するから$P(M)_0$が零項でないか$\textrm{Lng}(P(M))\neq2$である。

$\textrm{Trans}(M)=\underline{(}s\underline{,}D_00\underline{)}$は複項であり、かつ$P(M)_0$が零項でないか$\textrm{Lng}(P(M))\neq2$であるから、^[1]の$\textrm{Trans}$が単項性を保つことより$M$は複項である。

$\textrm{Trans}$の定義中の記号を$M$に対して定義する。

^[1]の$P$の各成分の非複項性、$\textrm{Trans}$が零項性を保つこと、$\textrm{Trans}$が単項性を保つこと、$\textrm{Trans}$の定義及び仮定より$P(M)_{J_1}$は単項であり、かつ$P(M)_{J_1}=((0,0))$または$\textrm{Trans}(P(M)_{J_1})=D_00$である。

$\textrm{Trans}(P(M)_{J_1})=D_00$とすると、^[1]の$\textrm{Trans}$と非可算基数の関係より$P(M)_{J_1}=((0,0),(0,0))$であり、よって$P(M)_{J_1}$は複項であるが、これは上と矛盾するため$P(M)_{J_1}=((0,0))$である。

^[1]の$P$の加法性より$P(M)=P(\textrm{Pred}(M))\oplus_{T_{\textrm{PS}}}(((0,0)))$である。

$P$の定義より$M=\textrm{Pred}(M)\oplus_{\mathbb{N}^2}((0,0))$である。

上より$\textrm{Trans}(M)=\textrm{Trans}((M_j)_{j_0}^{j_0-1})+D_00=\textrm{Trans}((M_j)_{j_0}^{j_1-1})+D_00=\textrm{Trans}(\textrm{Pred}(M))+D_00=\textrm{Trans}(M[n])+D_00$である。

よって$(\textrm{Trans}(M),\textrm{Trans}(M[n]))=(D_00,0)$または$\textrm{Trans}(M[n])+D_00=\textrm{Trans}(M)$である。□

補題 (基本列の関係)
任意の$M\in ST_{\textrm{PS}}$と$m\in\mathbb{N}$に対して、$\textrm{dom}(\textrm{Trans}(M))=\omega$ならばある$n\in\mathbb{N}_+$が存在して$\textrm{Trans}(M)[m]\leq_{\textrm{B}}\textrm{Trans}(M[n])$である。

証明

$\textrm{Trans}$の定義中の記号を$M$に対して定義する。

^[1]の標準形の簡約性より$M$は簡約である。

$\textrm{dom}(0)=0\neq\omega$かつ任意の$u\in\mathbb{N}$に対して$\textrm{dom}(D_u0)=\Omega_u\neq\omega$であるから$j_1>0$である。

$M$が単項であるとする。

$t_1=0$とする。

$M=((0,0),(1,0))$または$M=((0,0),(1,1))$である。^[1]の基本列の降下性の証明を参照。

$M=((0,0),(1,0))$とする。

$\textrm{Trans}(M)=D_0D_00$かつ任意の$n\in\mathbb{N}$に対して$\textrm{Trans}(M[n])=(D_00)\times(n-1)$である。^[1]の基本列の降下性の証明を参照。

$\textrm{dom}(D_00)=1$であるから$[]$の定義より任意の$n\in\mathbb{N}$に対して$(D_0D_00)[n]=(D_0(D_00[0]))\times(n+1)=(D_00)\times(n+1)$である。

よって$\textrm{Trans}(M)[m]\leq_{\textrm{B}}\textrm{Trans}(M[m+2])$である。

$M=((0,0),(1,1))$とする。

$\textrm{Trans}(M)=D_0D_10$かつ任意の$n\in\mathbb{N}$に対して$\textrm{Trans}(M[n])=D_0^n0$である。^[1]の基本列の降下性の証明を参照。

$\textrm{dom}(D_10)=\Omega_1$であるから$[]$の定義より任意の$n\in\mathbb{N}$に対して$(D_0D_10)[n]=D_0D_0^nD_0D_00=D_0^{n+3}0$である。

よって$\textrm{Trans}(M)[m]\leq_{\textrm{B}}\textrm{Trans}(M[m+3])$である。

$t_1\neq0$とする。

$M$が条件(I)-(VI)を満たすとき、それぞれ^[1]の条件(I)の下でのTransと基本列の交換関係(1)、条件(II)の下でのTransと基本列の交換関係(2)、条件(III)か(IV)の下でのTransと基本列の交換関係(3)、条件(V)の下でのTransと基本列の交換関係(3)及び条件(VI)の下でのTransと基本列の交換関係(2)よりある$n\in\mathbb{N}_+$が存在して$\textrm{Trans}(M)[m]\leq_{\textrm{B}}\textrm{Trans}(M[n])$である。

よって任意の$M\in PT_{\textrm{PS}}\cap ST_{\textrm{PS}}$と$m\in\mathbb{N}$に対して、$\textrm{dom}(\textrm{Trans}(M))=\omega$ならばある$n\in\mathbb{N}_+$が存在して$\textrm{Trans}(M)[m]\leq_{\textrm{B}}\textrm{Trans}(M[n])$である。

$M$が複項であるとする。

任意の$t_0,t_1\in T_{\textrm{B}}$と$m\in\textrm{dom}(t_1)$に対して$\textrm{dom}(t_0+t_1)=\textrm{dom}(t_1)$かつ$(t_0+t_1)[m]=t_0+(t_1[m])$である。

上より任意の$t\in T_{\textrm{B}}$に対して$\textrm{dom}(t+D_00)=\textrm{dom}(D_00)=1$であるから$P(M)_{J_1}\neq((0,0))$である。

仮定より$\textrm{dom}(\textrm{Trans}(P(M)_{J_1}))=\omega$である。

^[1]の$P$の各成分の非複項性及び標準形の単項成分が標準形であることより$P(M)_{J_1}\in PT_{\textrm{PS}}\cup ST_{\textrm{PS}}$である。

上より任意の$m\in\mathbb{N}$に対しある$n\in\mathbb{N}_+$が存在して$\textrm{Trans}(P(M)_{J_1})[m]\leq_{\textrm{B}}\textrm{Trans}(P(M)_{J_1}[n])$である。

$\textrm{dom}(0)=0\neq\omega$かつ任意の$u\in\mathbb{N}$に対して$\textrm{dom}(D_u0)=\Omega_u\neq\omega$であるから$\textrm{Lng}(P(M)_{J_1})>1$である。

^[1]の$P$と基本列の関係(2)より任意の$n\in\mathbb{N}_+$に対して$P(M[n])=(P(M)_J)_{J=0}^{J_1-1}\oplus_{T_{\textrm{PS}}}P(P(M)_{J_1}[n])$である。

^[1]の$P$の各成分の非複項性(2)より任意の$n\in\mathbb{N}_+$に対して$M[n]$は複項である。

任意の$M\in T_{\textrm{PS}}$に対して、$M$が零項ならば$M^+=D_00$、$M$が零項でないならば$M^+=\textrm{Trans}(M)$とする。

^[1]の$\textrm{Trans}$の$(\textrm{IncrFirst},\textrm{Red})$不変$P$同変性(2)、また任意の$t_0,t_1\in T_{\textrm{B}}^{<\omega}$に対して明らかに$\Sigma_{\textrm{B}}(t_0+t_1)=\Sigma_{\textrm{B}}t_0+\Sigma_{\textrm{B}}t_1$であり、任意の$n\in\mathbb{N}_+$に対して$P(M)_{J_1}$及び$P(M)_{J_1}[n]$は零項ではないから、$P(M)_{J_1}^+=\textrm{Trans}(P(M)_{J_1})$かつ$\textrm{Trans}(M)=\Sigma_{\textrm{B}}(P(M)_J^+)_{J=0}^{J_1}$かつ任意の$n\in\mathbb{N}_+$に対して$$\begin{array}{l}\textrm{Trans}(M[n])\\=\Sigma_{\textrm{B}}(P(M[n])_J^+)_{J=0}^{\textrm{Lng}(P(M[n]))-1}\\=\Sigma_{\textrm{B}}(P(M)_J^+)_{J=0}^{J_1-1}+\Sigma_{\textrm{B}}(P(P(M)_{J_1}[n])_J^+)_{J=0}^{\textrm{Lng}(P(P(M)_{J_1}[n]))-1}\\=\Sigma_{\textrm{B}}(P(M)_J^+)_{J=0}^{J_1-1}+\textrm{Trans}(P(M)_{J_1}[n])\end{array}$$である。

よって$$\begin{array}{l}\textrm{Trans}(M)[m]\\=\Sigma_{\textrm{B}}(P(M)_J^+)_{J=0}^{J_1}[m]\\=\Sigma_{\textrm{B}}(P(M)_J^+)_{J=0}^{J_1-1}+(P(M)_{J_1}^+[m])\\=\Sigma_{\textrm{B}}(P(M)_J^+)_{J=0}^{J_1-1}+(\textrm{Trans}(P(M)_{J_1})[m])\\=\Sigma_{\textrm{B}}(P(M)_J^+)_{J=0}^{J_1-1}+\textrm{Trans}(P(M)_{J_1}[m])\\=\textrm{Trans}(M[m])\\\leq_{\textrm{B}}\textrm{Trans}(M[m])\end{array}$$である。

よっていずれの場合でもある$n\in\mathbb{N}_+$が存在して$\textrm{Trans}(M)[m]\leq_{\textrm{B}}\textrm{Trans}(M[n])$である。□

命題 (基本列の収束性)
任意の$M\in ST_{\textrm{PS}}$に対して、$\textrm{dom}(\textrm{Trans}(M))=\omega$ならば$\sup_{n\in\mathbb{N}_+}o(\textrm{Trans}(M[n]))=o(\textrm{Trans}(M))$である。

証明: 基本列の関係、^[1]の基本列の降下性、^[5]のTheorem 1.4(a)及びLemma 1.6より$\{o(\textrm{Trans}(M[n]))\mid n\in\mathbb{N}_+\}$は$o(\textrm{Trans}(M))$の非有界な部分集合であることから即座に従う。□

命題 ($\textrm{Trans}$が順序を保つこと)
任意の$M,N\in CT_{\textrm{PS}}$に対して、$M<_{\textrm{PS}}N$ならば$\textrm{Trans}(M)<_{\textrm{B}}\textrm{Trans}(N)$である。

証明: 基本列的順序が辞書式的順序を含意することより$M<_{\textrm{PS}[]}N$である。; $<_{\textrm{PS}[]}$の定義よりある$a\in\mathbb{N}_+^{<\omega}\setminus\{()\}$が存在して$M=N[a_0]\cdots[a_{\textrm{Lng}(a)-1}]$である。; 任意の$((0,0))$は$<_{\textrm{PS}}$に対して$T_{\textrm{PS}}$の最小の要素であるから、$N\neq(0,0)$である。; 上より$\textrm{Lng}(N)>1$である。; 任意の非負整数$i<\textrm{Lng}(a)$に対して$Q_0=N$、$Q_{i+1}=Q_i[a_i]$とする。; ^[1]の基本列の降下性より$\textrm{Trans}(Q_1)=\textrm{Trans}(N[a_0])<_{\textrm{B}}\textrm{Trans}(N)$である。; 任意の非負整数$1\leq i<\textrm{Lng}(a)$をとり、$\textrm{Trans}(Q_i)<_{\textrm{B}}\textrm{Trans}(N)$とすると、^[1]の基本列の降下性及び^[4]のLemma 2.1より$\textrm{Trans}(Q_{i+1})\leq_{\textrm{B}}\textrm{Trans}(Q_i)<_{\textrm{B}}\textrm{Trans}(N)$である。; 帰納法により任意の非負整数$1\leq i<\textrm{Lng}(a)$に対して$\textrm{Trans}(Q_i)<_{\textrm{B}}\textrm{Trans}(N)$である。; よって$\textrm{Trans}(M)=\textrm{Trans}(Q_{\textrm{Lng}(a)})<_{\textrm{B}}\textrm{Trans}(N)$である。□

補題 (対応する項の上界未満の字母)
任意の$t\in T_{\textrm{B}\omega}$に対して、$t<_{\textrm{B}}D_0D_\omega0$ならば$t\in OT_{\textrm{B}\omega}$は$t\in OT_{\textrm{B}}$と同値である。

証明

(⇒) 任意の$t'\in OT_{\textrm{B}\omega}$をとり、$t'<_{\textrm{B}}D_\omega0$かつ$D_0t'\in OT_{\textrm{B}\omega}$とする。

仮定及び$OT_{\textrm{B}\omega}$の定義より任意の$x\in G_0t'$に対して$x<_{\textrm{B}}D_\omega0$である。

$t'$が字母$D_\omega$を含むとする。

ある$u\in\mathbb{N}\cup\{\omega\}$と$a\in OT_{\textrm{B}\omega}$が存在して$t'=D_ua$とすると、仮定より$u=\omega$またはある$b\in OT_{\textrm{B}\omega}$が存在して$D_\omega b\in G_ua\subset G_0t'$であるが、いずれも矛盾する。

ある$u\in(\mathbb{N}\cup\{\omega\})^{<\omega}$と$a\in OT_{\textrm{B}\omega}^{<\omega}$が存在して$\textrm{Lng}(a)=\textrm{Lng}(u)\geq2$かつ$t'=\underline{(}D_{u_0}a_0\underline{,}\cdots\underline{,}D_{\textrm{Lng}(a)-1}a_{\textrm{Lng}(a)-1}\underline{)}$とする。

仮定よりある非負整数$0\leq i<\textrm{Lng}(a)$が存在して$u_i=\omega$またはある$b\in OT_{\textrm{B}\omega}$が存在して$D_\omega b\in G_{u_i}a_i\subset G_0t'$である。

$OT_{\textrm{B}\omega}$の定義より任意の非負整数$0\leq i<\textrm{Lng}(a)$に対して$D_{u_i}a_i\leq_{\textrm{B}}D_{u_0}a_0<_{\textrm{B}}t'$である。

ある非負整数$0\leq i<\textrm{Lng}(a)$が存在して$u_i=\omega$とすると、上が$t'<_{\textrm{B}}D_\omega0$と矛盾する。

ある非負整数$0\leq i<\textrm{Lng}(a)$と$b\in OT_{\textrm{B}\omega}$が存在して$D_\omega b\in G_{u_i}a_i\subset G_0t'$であるとすると、任意の$x\in G_0t'$に対して$x<_{\textrm{B}}D_\omega0$であることと矛盾する。

いずれの場合も矛盾するため$t'$は字母$D_\omega$を含まない。

$t=0$ならば$t\in T_{\textrm{PS}}$である。

$t$が単項であるとする。

$OT_{\textrm{B}\omega}$の定義及び条件よりある$a\in OT_{\textrm{B}\omega}$が存在して$t<_{\textrm{B}}D_\omega0$かつ$t=D_0a$である。

上より$a$は字母$D_\omega$を含まないから$t\in T_{\textrm{PS}}$である。

$t$が複項であるとする。

$OT_{\textrm{B}}$の定義よりある$a\in OT_{\textrm{B}\omega}^{<\omega}\setminus\{()\}$が存在して$D_0a_0<_{\textrm{B}}t$かつ$t=\underline{(}D_0a_0\underline{,}\cdots\underline{,}D_0a_{\textrm{Lng}(a)-1}\underline{)}$である。

上より任意の非負整数$0\leq i<\textrm{Lng}(a)$に対して$a_i\leq_{\textrm{B}}a_0<_{\textrm{B}}D_\omega0$である。

上より任意の非負整数$0\leq i<\textrm{Lng}(a)$に対して$a_i$は字母$D_\omega$を含まないから$t\in T_{\textrm{PS}}$である。

よっていずれの場合でも$t\in T_{\textrm{PS}}$である。

よって$t\in OT_{\textrm{B}}=OT_{\textrm{B}\omega}\cap T_{\textrm{PS}}$である。

(⇐) $OT_{\textrm{B}}\subset OT_{\textrm{B}\omega}$より即座に従う。□

命題 (対応する項の上界)
(1) 任意の$M\in CT_{\textrm{PS}}$に対して$\textrm{Trans}(M)<_{\textrm{B}}D_0D_\omega0$である。
(2) 任意の$t\in T_{\textrm{B}}$に対して、$t<_{\textrm{B}}D_0D_\omega0$ならばある$M\in CT_{\textrm{PS}}$が存在して$t<_{\textrm{B}}\textrm{Trans}(M)$である。

証明

(1) 可算な標準形の起源より任意の$M\in CT_{\textrm{PS}}$に対してある$v\in\mathbb{N}$が存在して$M\leq_{\textrm{PS}[]}((j,j))_{j=0}^v$である。

辞書式的順序が基本列的順序を含意することより$M\leq_{\textrm{PS}}((j,j))_{j=0}^v$である。

^[1]の公差$(1,1)$のペア数列の$\textrm{Trans}$の基本性質より$\textrm{Trans}(((j,j))_{j=0}^v)=D_0D_v0<_{\textrm{B}}D_0D_\omega0$である。

$\textrm{Trans}$が順序を保つことより$\textrm{Trans}(M)<_{\textrm{B}}\textrm{Trans}(((j,j))_{j=0}^v)<_{\textrm{B}}D_0D_\omega0$である。□

(2) 任意の$t'\in T_{\textrm{B}}$をとる。

$t'=0$ならば$t'<_{\textrm{B}}D_00$である。

$t'\in PT_{\textrm{B}}$とする。

ある$u\in\mathbb{N}$と$a\in OT_{\textrm{B}}$が存在して$t'=D_ua$である。

$t'<_{\textrm{B}}D_{u+1}0$である。

$t'\in MT_{\textrm{B}}$とする。

ある$u\in\mathbb{N}$と$a\in OT_{\textrm{B}}$と$s\in\Sigma^{<\omega}$が存在して$t'=\underline{(}D_ua\underline{,}s\underline{)}$である。

$t'<_{\textrm{B}}D_{u+1}0$である。

よっていずれの場合でもある$u\in\mathbb{N}$が存在して$t'<_{\textrm{B}}D_u0$である。

$t=0$ならば$t<_{\textrm{B}}D_00$である。

$t\in PT_{\textrm{B}}$とする。

ある$a\in T_{\textrm{B}}$が存在して$t=D_0a$である。

上よりある$u\in\mathbb{N}$が存在して$a<_{\textrm{B}}D_u0$である。

よってある$u\in\mathbb{N}$が存在して$t<_{\textrm{B}}D_0D_u0$である。

$t\in MT_{\textrm{B}}$とする。

ある$a\in T_{\textrm{B}}$と$s\in\Sigma^{<\omega}$が存在して$t=\underline{(}D_0a\underline{,}s\underline{)}$である。

上よりある$u\in\mathbb{N}$が存在して$a<_{\textrm{B}}D_u0$である。

よってある$u\in\mathbb{N}$が存在して$D_0a<_{\textrm{B}}D_0D_u0$である。

よってある$u\in\mathbb{N}$が存在して$t<_{\textrm{B}}D_0D_u0$である。

よっていずれの場合でもある$u\in\mathbb{N}$が存在して$t<_{\textrm{B}}D_0D_u0$である。

^[1]の公差$(1,1)$のペア数列の$\textrm{Trans}$の基本性質より$t<_{\textrm{B}}D_0D_u=0\textrm{Trans}(((j,j))_{j=0}^u)=D_0D_u0$である。□

命題 (変換写像の順序数への全単射性)
$o\circ\textrm{Trans}$は$CT_{\textrm{PS}}\to\psi_0\psi_\omega0$上で全域かつ全単射である。

証明: 対応する項の上界未満の字母、対応する項の上界(1)と(2)及び^[1]の$\textrm{Trans}$が標準形を保つことより$\{\textrm{Trans}(M)\mid M\in CT_{\textrm{PS}}\}$は$\{t\mid t\in OT_{\textrm{B}\omega}\land t<_{\textrm{B}}D_0D_\omega0\}$の$<_{\textrm{B}}$に対して非有界な部分集合である。; ^[4]のLemma 2.2(c)より$\{o(\textrm{Trans}(M))\mid M\in CT_{\textrm{PS}}\}$は$o(D_0D_\omega0)=\psi_0\psi_\omega0$の非有界な部分集合である。; ^[4]のLemma 2.3(b)及び^[5]のLemma 1.6より任意の$t\in\{t\mid t\in OT_{\textrm{B}\omega}\land t<_{\textrm{B}}D_10\}$に対して$\textrm{dom}(t)=\textrm{cof}(o(t))$である。; 後続な項の基本列及び^[1]の標準形の簡約性より任意の$M\in CT_{\textrm{PS}}$に対して、$\textrm{cof}(o(\textrm{Trans}(M)))=1$ならば$o(\textrm{Trans}(M))=o(\textrm{Trans}(M[1])+D_00)=o(\textrm{Trans}(M[1]))+o(D_00)=o(\textrm{Trans}(M[1]))+1$である。; 基本列の収束性より任意の$M\in CT_{\textrm{PS}}$に対して、$\textrm{cof}(o(\textrm{Trans}(M)))=\omega$ならば$o(\textrm{Trans}(M))=\sup_{n\in\mathbb{N}_+}o(\textrm{Trans}(M[n]))$である。; ^[3]の命題11より$o\circ\textrm{Trans}$は$CT_{\textrm{PS}}\to\psi_0\psi_\omega0$上で全射である。; $\textrm{Trans}$が順序を保つこと、^[4]のLemma 2.1及びLemma 2.2(c)より$o\circ\textrm{Trans}$は$CT_{\textrm{PS}}\to\psi_0\psi_\omega0$上で単射である。; よって$o\circ\textrm{Trans}$は$CT_{\textrm{PS}}\to\psi_0\psi_\omega0$上で全域かつ全単射である。□

系 (ペア数列の解析)
(1) 任意の$M\in CT_{\textrm{PS}}$に対して、$o\circ\textrm{Trans}$は同型写像$(\{N\mid N\in CT_{\textrm{PS}}\land N<_{\textrm{PS}}M\},<_{\textrm{PS}})\to(\{\alpha\mid\alpha\in o(\textrm{Trans}(M))\},\in)$である。
(2) 任意の$M\in CT_{\textrm{PS}}$に対して、$\textrm{Trans}$は同型写像$(\{N\mid N\in CT_{\textrm{PS}}\land N<_{\textrm{PS}}M\},<_{\textrm{PS}})\to(\{t\mid t\in OT_{\textrm{B}\omega}\land t<_{\textrm{B}}\textrm{Trans}(M)\},<_{\textrm{B}})$である。

証明: (1) $\textrm{Trans}$が順序を保つこと及び変換写像の順序数への全単射性より即座に従う。; (2) 対応する項の上界(1)と(2)、対応する項の上界未満の字母、^[4]のLemma 2.2(c)及びLemma 2.3(b)より$o$は同型写像$(\{t\mid t\in OT_{\textrm{B}\omega}\land t<_{\textrm{B}}D_0D_\omega0\},<_{\textrm{B}})\to(o(D_0D_\omega0)=\psi_0\psi_\omega0,\in)$である。; $\textrm{Trans}=o^{-1}\circ o\circ\textrm{Trans}$であるから(1)より従う。□

定理 (変換写像の全単射性)
$\textrm{Trans}$は$CT_{\textrm{PS}}\to\{t\mid t\in OT_{\textrm{B}\omega}\land t<_{\textrm{B}}D_0D_\omega0\}$上で全域かつ全単射であり、特に同型写像である。

証明: 可算な標準形の起源及び辞書式的順序が基本列的順序を含意することより任意の$M\in CT_{\textrm{PS}}$に対してある$v\in\mathbb{N}$が存在して$M\leq_{\textrm{PS}}((j,j))_{j=0}^v<_{\textrm{PS}}((j,j))_{j=0}^{v+1}\in CT_{\textrm{PS}}$であるから、$CT_{\textrm{PS}}=\bigcup_{M\in CT_{\textrm{PS}}}\{N\mid N\in CT_{\textrm{PS}}\land N<_{\textrm{PS}}M\}$である。; ^[4]のLemma 2.1より$\{t\mid t\in OT_{\textrm{B}\omega}\land t<_{\textrm{B}}D_0D_\omega0\}=\bigcup_{t_0\in\{t\mid t\in OT_{\textrm{B}\omega}\land t<_{\textrm{B}}D_0D_\omega0\}}\{t\mid t\in OT_{\textrm{B}\omega}\land t<_{\textrm{B}}t_0\}$である。; 対応する項の上界(2)より$\{t\mid t\in OT_{\textrm{B}\omega}\land t<_{\textrm{B}}D_0D_\omega0\}=\bigcup_{M\in CT_{\textrm{PS}}}\{t\mid t\in OT_{\textrm{B}\omega}\land t<_{\textrm{B}}\textrm{Trans}(M)\}$である。; ペア数列の解析(2)より従う。□

文献・脚注[]

↑ ^1.00 ^1.01 ^1.02 ^1.03 ^1.04 ^1.05 ^1.06 ^1.07 ^1.08 ^1.09 ^1.10 ^1.11 ^1.12 ^1.13 ^1.14 ^1.15 ^1.16 ^1.17 ^1.18 ^1.19 ^1.20 ^1.21 ^1.22 ^1.23 ^1.24 ^1.25 ^1.26 ^1.27 ^1.28 ^1.29 ^1.30 ^1.31 p進大好きbot, ペア数列の停止性, ユーザーブログ, Retrieved 2022/07/26
↑ p進大好きbot, [1], ユーザーブログへのコメント, Retrieved 2022/07/24
↑ ^3.0 ^3.1 ^3.2 p進大好きbot, 変換写像による解析, ユーザーブログ, Retrieved 2022/07/17
↑ ^4.0 ^4.1 ^4.2 ^4.3 ^4.4 ^4.5 ^4.6 ^4.7 ^4.8 W. Buchholz, A new system of proof-theoretic ordinal functions, Annals of Pure and Applied Logic, Volume 32, 1986, pp. 195--207.
↑ ^5.0 ^5.1 ^5.2 W. Buchholz, Relating ordinals to proofs in a prespicious way, unpublished article.

[ja-gwikiblog.psstermination-1] 1.00 ^1.01 ^1.02 ^1.03 ^1.04 ^1.05 ^1.06 ^1.07 ^1.08 ^1.09 ^1.10 ^1.11 ^1.12 ^1.13 ^1.14 ^1.15 ^1.16 ^1.17 ^1.18 ^1.19 ^1.20 ^1.21 ^1.22 ^1.23 ^1.24 ^1.25 ^1.26 ^1.27 ^1.28 ^1.29 ^1.30 ^1.31 p進大好きbot, ペア数列の停止性, ユーザーブログ, Retrieved 2022/07/26

[2] 進大好きbot, [1], ユーザーブログへのコメント, Retrieved 2022/07/24

[ja-gwikiblog.translationmap-3] 3.0 ^3.1 ^3.2 p進大好きbot, 変換写像による解析, ユーザーブログ, Retrieved 2022/07/17

[buchholz1-4] 4.0 ^4.1 ^4.2 ^4.3 ^4.4 ^4.5 ^4.6 ^4.7 ^4.8 W. Buchholz, A new system of proof-theoretic ordinal functions, Annals of Pure and Applied Logic, Volume 32, 1986, pp. 195--207.

[buchholz2-5] 5.0 ^5.1 ^5.2 W. Buchholz, Relating ordinals to proofs in a prespicious way, unpublished article.

[1]

[2]

[3]

[4]

[5]

ペア数列システムの停止性証明に用いられた変換写像の全単射性

目次

背景[]

表記[]

証明[]

関連して[]

文献・脚注[]

命題 (対応する項の上界)
(1) 任意の\(M\in CT_{\textrm{PS}}\)に対して\(\textrm{Trans}(M)<_{\textrm{B}}D_0D_\omega0\)である。
(2) 任意の\(t\in T_{\textrm{B}}\)に対して、\(t<_{\textrm{B}}D_0D_\omega0\)ならばある\(M\in CT_{\textrm{PS}}\)が存在して\(t<_{\textrm{B}}\textrm{Trans}(M)\)である。