Dmytro氏のA Step towards Second Order Arithmeticで表される順序数の収束列と、収束列を求めるために必要な性質をまとめます。
ただし、記述の大部分は私の推測に過ぎない上にほとんど検証をしていないので、正しさは保証できません。
standard representationの定義は少し変えてあります。
詳細を知りたい人は、Dmytro氏のページを参照してください。
http://web.mit.edu/dmytro/www/other/OrdinalNotation.htm

1. standard representationへの書き換え

0, Ω_n (n≧2)は、standard representationである。
Ω_1のstandard representationは、C(Ω_2,0)である。

C(a,b)がstandard representationであるのは、
・a,bがstandard representationである
・bが最小である
・aが最大である
・C(a,b)=C(Ω_n,0) (n≧3)でない
の全てを満たすときである。

C(a,b)をstandard representationに書き換える手順は、以下の通りである。

a,bをstandard representationに書き換える。

b=0のとき、bは最小である。
b=C(c,d)のとき、
　a≦cならば、bは最小である。
　a＞cならば、C(a,b)をC(a,d)に書き換えてdの最小化をする。

Ω_n≦b＜Ω_{n+1}を満たすnを、cor(b)と表す。ただし、Ω_0=0とする。

bより大きいcorrectnessがnの最小の順序数を表すnextcor(b,n)を、以下のように定義する。
n＞cor(b)のとき、
　nextcor(b,n)=Ω_n
1≦n≦cor(b)のとき、
　nextcor(b,n)=C(nextcor(b,n+1),b)
nextcor(b,n)がstandard representationでないときは、standard representationに書き換える。

nextcor(b,n)≦a＜nextcor(b,n+1)を満たすn≧2が存在するとき、Ω=nextcor(b,n), Ω'=nextcor(b,n+1)とする。
a＜nextcor(b,2)のとき、Ω=nextcor(b,2)とする。

aが最大であるか判定するのに用いる関数stdcheck1(c,a,Ω,Ω')を、以下のように定義する。
stdcheck1(0,a,Ω,Ω')=1
stdcheck1(Ω_n,a,Ω,Ω')=1
C(c,d)＜Ωのとき、
　stdcheck1(C(c,d),a,Ω,Ω')=1
Ω≦C(c,d)≦aまたはC(c,d)＞Ω'のとき、
　stdcheck1(C(c,d),a,Ω,Ω')=stdcheck1(c,a,Ω,Ω')*stdcheck1(d,a,Ω,Ω')
a＜C(c,d)＜Ω'のとき、
　stdcheck1(C(c,d),a,Ω,Ω')=0

aが最大であるか判定するのに用いる関数stdcheck2(c,a,b,Ω)を、以下のように定義する。
stdcheck2(0,a,b,Ω)=1
stdcheck2(Ω_n,a,b,Ω)=1
C(c,d)＜Ωのとき、
　stdcheck2(C(c,d),a,b,Ω)=stdcheck3(C(c,d),a,b,C(c,d),Ω)
C(c,d)≧Ωのとき、
　stdcheck2(C(c,d),a,b,Ω)=stdcheck2(c,a,b,Ω)*stdcheck2(d,a,b,Ω)

aが最大であるか判定するのに用いる関数stdcheck3(d,a,b,c,Ω)を、以下のように定義する。
stdcheck3(0,a,b,c,Ω)=1
stdcheck3(Ω_n,a,b,c,Ω)=1
C(d,e)＜C(a,b)のとき、
　stdcheck3(C(d,e),a,b,c,Ω)=1
「C(d,e)≧C(a,b)かつC(d,e)≦c」またはC(d,e)＞Ωのとき、
　stdcheck3(C(d,e),a,b,c,Ω)=stdcheck3(d,a,b,c,Ω)*stdcheck3(e,a,b,c,Ω)
C(d,e)≧C(a,b)かつC(d,e)＞cかつC(d,e)＜Ωのとき、
　stdcheck3(C(d,e),a,b,c,Ω)=0

Ω'が定義されているとき、
　stdcheck1(a,a,Ω,Ω')=stdcheck2(a,a,b,Ω)=1ならばaは最大であり、
　stdcheck1(a,a,Ω,Ω')*stdcheck2(a,a,b,Ω)=0ならばaは最大でない。
Ω'が定義されていないとき、
　stdcheck3(a,a,b,a,Ω)=1ならばaは最大であり、
　stdcheck3(a,a,b,a,Ω)=0ならばaは最大でない。

aが最大になるように書き換えるのに用いる関数std1(c,a,Ω,Ω')を、以下のように定義する。
std1(0,a,Ω,Ω')=0
std1(Ω_n,a,Ω,Ω')=Ω_n
C(c,d)＜Ωのとき、
　std1(C(c,d),a,Ω,Ω')=C(c,d)
Ω≦C(c,d)≦aまたはC(c,d)＞Ω'かつ、
　stdcheck1(d,a,Ω,Ω')=0のとき、
　　std1(C(c,d),a,Ω,Ω')=std1(d,a,Ω,Ω')
　stdcheck1(d,a,Ω,Ω')=1かつstdcheck1(c,a,Ω,Ω')=0のとき、
　　std1(C(c,d),a,Ω,Ω')=C(std1(c,a,Ω,Ω'),d)
　stdcheck1(d,a,Ω,Ω')=stdcheck1(c,a,Ω,Ω')=1のとき、
　　std1(C(c,d),a,Ω,Ω')=C(c,d)
a＜C(c,d)＜Ω'のとき、
　std1(C(c,d),a,Ω,Ω')=Ω'

aが最大になるように書き換えるのに用いる関数std2(c,a,b,Ω)を、以下のように定義する。
std2(0,a,b,Ω)=0
std2(Ω_n,a,b,Ω)=Ω_n
C(c,d)＜Ωのとき、
　std2(C(c,d),a,b,Ω)=std3(C(c,d),a,b,C(c,d),Ω)
C(c,d)≧Ωかつ、
　stdcheck2(d,a,b,Ω)=0のとき、
　　std2(C(c,d),a,b,Ω)=std2(d,a,b,Ω)
　stdcheck2(d,a,b,Ω)=1かつstdcheck2(c,a,b,Ω)=0のとき、
　　std2(C(c,d),a,b,Ω)=C(std2(c,a,b,Ω),d)
　stdcheck2(d,a,b,Ω)=stdcheck2(c,a,b,Ω)=1のとき、
　　std2(C(c,d),a,b,Ω)=C(c,d)

aが最大になるように書き換えるのに用いる関数std3(d,a,b,c,Ω)を、以下のように定義する。
std3(0,a,b,c,Ω)=0
std3(Ω_n,a,b,c,Ω)=Ω_n
C(d,e)＜C(a,b)のとき、
　std3(C(d,e),a,b,c,Ω)=C(d,e)
「C(d,e)≧C(a,b)かつC(d,e)≦c」またはC(d,e)＞Ωかつ、
　stdcheck3(e,a,b,c,Ω)=0のとき、
　　std3(C(d,e),a,b,c,Ω)=std3(e,a,b,c,Ω)
　stdcheck3(e,a,b,c,Ω)=1かつstdcheck3(d,a,b,c,Ω)=0のとき、
　　std3(C(d,e),a,b,c,Ω)=C(std3(d,a,b,c,Ω),e)
　stdcheck3(e,a,b,c,Ω)=stdcheck3(d,a,b,c,Ω)=1のとき、
　　std3(C(d,e),a,b,c,Ω)=C(d,e)
C(d,e)≧C(a,b)かつC(d,e)＞cかつC(d,e)＜Ωのとき、
　std3(C(d,e),a,b,c,Ω)=Ω

Ω'が定義されているとき、
　stdcheck1(a,a,Ω,Ω')=0ならばaをstd1(a,a,Ω,Ω')に書き換える。
　stdcheck2(a,a,b,Ω)=0ならばaをstd2(a,a,b,Ω)に書き換える。
Ω'が定義されていないとき、
　stdcheck3(a,a,b,a,Ω)=0ならばaをstd3(a,a,b,a,Ω)に書き換える。
これを、aが最大になるまで繰り返す。

C(a,b)=C(Ω_n,0) (n≧3)のとき、C(a,b)をΩ_{n-1}に書き換える。

2. 大小比較

0＜Ω_n
m＜nのとき、Ω_m＜Ω_n

C(a,b)がstandard representationかどうかにかかわらず、
0＜C(a,b)
b＜Ω_nかつa＜Ω_{n+1}のとき、C(a,b)＜Ω_n
b＜Ω_nかつa=Ω_{n+1}のとき、C(a,b)=Ω_n
b≧Ω_nまたはa＞Ω_{n+1}のとき、C(a,b)＞Ω_n

C(a,b)のaが最大のとき、C(a,b), C(c,d)がstandard representationかどうかにかかわらず、
C(a,b)＜C(c,d)となるのは、
　C(a,b)≦dまたは「b＜C(c,d)かつa＜c」
のときである。

2つの順序数のstandard representationが一致するときのみ、両者は等しい。

3. 収束列

以下では、aは後続順序数、bは収束列のある極限順序数、
c, c'は収束列のない極限順序数、d, e, xは任意の順序数とする。
また、すべての順序数はstandard representationであるとする。

C(0,d)=d+1は後続順序数である。
C(a,d), C(b,d)は収束列のある極限順序数である。
Ω_nは収束列のない極限順序数である。

subst_cor(c,c,d)＞0のとき、C(c,d)は収束列のある極限順序数である。
subst_cor(c,c,d)=0のとき、C(c,d)は収束列のない極限順序数である。

前者関数pred(a)は後続順序数aについて定義され、
pred(C(0,d))=d

収束列b_nは収束列のある極限順序数b、自然数nについて定義され、
{C(a,d)}_0=d
{C(a,d)}_{n+1}=C(pred(a),{C(a,d)}_n)
{C(b,d)}_n=C(b_n,d)

subst_cor(c,c,d)＞0のとき、Ω=nextcor(d,subst_cor(c,c,d))とする。
　C(c,d)≧subst3(subst_arg2(C(c,d),Ω),subst_arg1(c,Ω),Ω)のとき、
　　{C(c,d)}'_0=0
　　{C(c,d)}'_{n+1}=subst2(subst_arg1(c,Ω),C(subst1(c,{C(c,d)}'_n,Ω),d),Ω)
　　{C(c,d)}_n=C(subst1(c,{C(c,d)}'_n,Ω),d)
　C(c,d)＜subst3(subst_arg2(C(c,d),Ω),subst_arg1(c,Ω),Ω)のとき、
　　{C(c,d)}'_0=0
　　{C(c,d)}'_{n+1}=subst2(subst_arg1(c,Ω),subst3(subst_arg2(C(c,d),Ω),{C(c,d)}'_n,Ω),Ω)
　　{C(c,d)}_n=C(subst1(c,{C(c,d)}'_n,Ω),d)

subst_cor(c',c,d)は収束列のない極限順序数c, c'、任意の順序数dについて定義され、
c'＜C(c,d)のとき、
　subst_cor(c',c,d)=0
Ω_n＞C(c,d)のとき、
　subst_cor(Ω_n,c,d)=n
C(c',e)＞C(c,d)かつ、
　C(c',e)=nextcor(d,n)となるn≧2が存在するとき、
　　subst_cor(C(c',e),c,d)=n
　C(c',e)=nextcor(d,n)となるn≧2が存在しないとき、
　　subst_cor(C(c',e),c,d)=subst_cor(c',c,d)

subst1(c,x,Ω)は収束列のない極限順序数c、任意の順序数xについて定義され、
subst1(Ω,x,Ω)=x
C(c,d)＜Ωのとき、
subst1(C(c,d),x,Ω)=x
C(c,d)＞Ωのとき、
subst1(C(c,d),x,Ω)=C(subst1(c,x),d,Ω)

subst2(C(c,d),x,Ω)は収束列のない極限順序数c、任意の順序数d, xについて定義され、
subst_arg1(c,Ω)=Ωのとき、
subst2(C(c,d),x,Ω)=x
subst_arg1(c,Ω)＜Ωのとき、
subst2(C(c,d),x,Ω)=C(subst1(c,subst2(subst_arg1(c,Ω),x,Ω),Ω),d)

subst3(C(c,d),x,Ω)は収束列のない極限順序数c、任意の順序数d, xについて定義され、
subst3(C(c,d),x,Ω)=C(subst1(c,x,Ω),d)

subst_arg1(c,Ω)は収束列のない極限順序数cについて定義され、
subst_arg1(Ω,Ω)=Ω
C(c,d)＜Ωのとき、
subst_arg1(C(c,d),Ω)=C(c,d)
C(c,d)＞Ωのとき、
subst_arg1(C(c,d),Ω)=subst_arg1(c,Ω)

subst_arg2(C(c,d),Ω)は収束列のない極限順序数c、任意の順序数dについて定義され、
subst_arg1(c,Ω)=Ωのとき、
subst_arg2(C(c,d),Ω)=C(c,d)
subst_arg1(c,Ω)＜Ωのとき、
subst_arg2(C(c,d),Ω)=subst_arg2(subst_arg1(c,Ω),Ω)

4. 巨大関数を作るための定義

aは後続順序数、bは収束列のある極限順序数とする。

H[0](n)=n
H[a](n)=H[pred(a)](n+1)
H[n](n)=H[b_n](n)

Ω_0=0, Ω_1=C(Ω_2,0)
X(m,0)=C(0,Ω_m)
X(m,n+1)=C(X(m,n),0)
として、H[X(n,n)](n)を考えると、nについて急激に増加する関数になる。