>>113
BB(10^100)と言っても、計算可能な定義が示されてないから、計算可能な部分だけ見れば「西暦3000年1月1日の時点で最大の数」って言うのとほとんど変わらない

依存型のようなものを追加してみる
[0]_α(β) = φ(α,β)
[0]_0([0]_0) = [0]_Ω
ここまではたぶん同じ
ここから：[1] :: A → (A → A)
[1](0) = [0]_{ψ_I(0)}
いつかしっかり定義したい

※[0]_0の_0部分はわかりやすくするために名前をつけるためのものなので、[0]_0=[0]