>>548
定義の順序はこの方がイイかも
⓪λ=0のとき
K(0)::={κ:到達不能基数}
U(0)::=∀α<∃κ∈K(0)
k(0):Ord→K(0)
①後続順序数λ+1のとき
K(λ+1)::={κ:κ=k(λ)(κ)}
U(λ+1)::=U(λ)∧∀α<∃κ∈K(λ+1)
k(λ+1):Ord→K(λ+1)
②λが極限順序数の時
K(λ)::={κ::∀μ<λ:κ=k(μ)(κ)}
U(λ)::=∀μ<λ:U(μ)∧∀α<∃κ∈K(λ)
k(λ):Ord→K(λ)
まず
K(λ)がそれ以前のk(μ)によって定義され
どの順序数にもそれより大きなK(λ)の元があると言う公理
U(λ)が定義され
それによりK(λ)がOrdと順序同型となるから
k(λ):Ord→K(λ)を得る
ひとつ心配でもあるのは極限順序数の時
K(λ)=∩K(μ)（μ<λ）にしているところだけど
U(λ)をどの順序数にもそれより大きなK(λ)の元があると言う公理にしているから
これがZFCと相容れないモノでなければ（矛盾にならなければ）
U(λ)を仮定したらK(λ)はOrdと順序同型となって
話は続いていく