~~この記事はInternet Explorerだとフリーズしやすいです。例えばGoogle Chromeが推奨です。~~

~~Internet ExplorerはFANDOMが非対応になりました。~~

Internet Explorerはサポートが終了しました。

はじめに[]

これは東方巨大数３への投稿用の記事です。以前の記事と同様FGHで\(\textrm{PTO}(\textrm{ZFC})\)相当の巨大関数を目指す試みです。

注意[]

これまでの試みとの本質的な差は基本列周りだけですが、折角なので今回は巨大数界隈でブラックボックスとして扱われがちな「チューリングマシンの対角化」や「証明可能性」等の厳密な定義を書きます。これらの概念が（形式論理の複雑な概念を既知とした上で概説されることが多いため）巨大数界隈にはあまり深く説明されていないことが超越整数システムへの不信感やチート感に繋がっていると思うので、これを機に超越整数システム全体の地位向上を目指す狙いもあります。ひとたび厳密な定義を読むことができれば（すぐにはその強さが理解出来ないものの）他の計算可能関数同様に四則演算や配列のコピー／書き換えの組み合わせだけできちんと計算できる代物であることが納得できると思います。

また「この配列の意味は何か」的なことはあまり説明しません。何故ならあくまでこの記事に登場する配列たちは定義に遡れば単なる\((0,((1),2),(3))\)みたいな配列であることが分かり、それ自体にそもそも「意味」はないからです。仮に「意味」付けを証明論の言葉で説明してしまうと唐突な未知との遭遇により混乱して「そんな概念どこにも定義してないからill-definedでは？」とか「難しい概念を知らないと計算規則さえ読むことさえ出来ないのか」とか誤解されるかもしれないからです。ただでさえ超越整数システムは「チューリングマシンの対角化？　証明可能性？　そんなものを考えたら計算可能でないよね」とか「計算可能という概念の定義とやらは満たしていることを屁理屈で示せるかもしれないけど、少なくとも計算規則を具体的に書くことは出来ないよね」とかいう感じの認識がそれなりにはびこっていると思いますので、そういった誤解は極力生じさせないように配慮した結果です。また証明論をある程度知っている人なら記法だけからその証明論での役割が想像つきやすいようにしましたので、そうなるとわざわざ証明論で「意味」付けを明記してしまうことはデメリットが勝ると考えました。というわけで、あえて分かりにくく書いているわけではないということにご留意下さい。元々分かりにくい概念を何一つごまかさずに定義しているだけです。

ここで再度強調したいのが、この記事では配列の「意味」などを一切用いずただの配列として扱い、計算規則もきちんと四則演算や配列のコピー／書き換えの繰り返しとして全て具体的に書いているということです。従って、計算規則自体は時間さえあれば証明論における「意味」付けを全く知らなくても誰でも厳密に読み解くことが出来るということです。以上を踏まえて読んで下されば、「この手の巨大数は計算規則が書き下せないので計算可能かどうか怪しい」という類の誤解を払拭できると思います。まあ冒頭にこれだけ注意が書いてあっても読み飛ばされて「どうせ曖昧にしか計算規則が書いてないんでしょう」的な解釈をされてしまう可能性は十分にありますので、過度な期待はしないことにします。

PTO(ZFC)[]

\(\textrm{PTO}(\textrm{ZFC})\)と同様\(\textrm{ZFC}\)公理系の限界を与える概念として超越整数システムがありますが、\(\textrm{PTO}(\textrm{ZFC})\)と超越整数は標語的には同じようなものでも厳密には異なるものです。例えるならば、その差は\(\omega_1^{\textrm{CK}}\)とビジービーバー関数の差と同じようなものです。

ビジービーバー関数は計算可能関数の限界を与える計算不可能関数ですが、その計算不可能性はあくまで「計算可能関数の停止性の判定機」である\(\textrm{Halt}\)という１つの非常に弱い神託機械（計算不可能関数）に依拠しています。一方で\(\omega_1^{\textrm{CK}}\)はそれより強く、「『再帰的整列順序集合の順序数型』である可算順序数全体における『非常に複雑で計算不可能な基本列』を用いて到達される「再帰的整列順序集合の順序数型」でない可算順序数」として表されるため、FGHによって超限帰納的に得られる計算不可能関数は計算可能なものから程遠い基本列で計算可能関数を対角化したものとなります。

超越整数システムは可証全域計算可能関数の限界を与える非可証全域計算可能関数です。関数の中に計算可能／計算不可能という対立があったように、計算可能関数の中にも可証全域／非可証全域という対立があります。そしてビジービーバー関数の計算不可能性があくまで「計算可能関数の停止性の判定機」という１つの弱い神託関数のみに依拠していたように、超越整数システムの非可証全域性もあくまで「計算可能関数の可証全域性の判定機」という１つの非常に弱い非可証全域計算可能関数に依拠しています。一方で\(\textrm{PTO}(\textrm{ZFC})\)は「『可証整礎再帰的整列順序集合の順序数型』であるような可算順序数全体における『非常に複雑で非可証全域な計算可能な基本列』を用いて到達される『可証整礎再帰的整列順序集合の順序数型』でない可算順序数」として恐らく表されるため、FGHによって超限帰納的に得られる非可証全域計算可能関数は可証全域計算可能なものとは程遠い基本列で可証全域計算可能関数を対角化したものとなります。

従ってFGHにおいて\(\textrm{PTO}(\textrm{ZFC})\)を直接叩けるシステムを構築してしまえば、結果的に超越整数システムを超える巨大関数が作れると考えられます。計算可能巨大関数の１つの壁である超越整数システムを前に諦観するのではなく、更にその上を目指しましょう。これまでは基本列の強さが不十分でまだFGHの意味で\(\textrm{PTO}(\textrm{ZFC})\)には到達できませんでしたが、今回こそは到達できたと思います。解析の章に厳密な証明も書きましたので、どこか誤りがあったら教えていただきますと助かります。

非常に紛らわしいので念を押しますが、\(\textrm{PTO}(\textrm{ZFC})\)の具体的な記述自体は数学のみ解決問題であり、そういうことはもちろん出来ていません。ここでは\(\textrm{PTO}(\textrm{ZFC})\)という概念の定義そのものを参考にし、「FGHを考える上では」\(\textrm{PTO}(\textrm{ZFC})\)と同等の働きをしてくれる表記系を導入しているだけです。FGH以外の文脈では当然\(\textrm{PTO}(\textrm{ZFC})\)と同じ働きをすることが保証されませんし、\(\textrm{PTO}(\textrm{ZFC})\)を極限に持つ順序数表記を構成したわけでもありません。完全に巨大数を作る目的のみに特化させた表記系を作っているだけです。ある意味で「OCFを考える上では弱到達不能基数と同じ働きをする順序数を構成したけど弱到達不能基数を構成したわけではない」系の話と同じですね。

表記系[]

細かいことは置いておいてどのような表記なのかを知りたいという人のために、今回扱う表記がどのような見た目なのかだけ説明しようと思います。表記の見た目そのものは単純で、「自然数の\(3 \times 2\)行列の配列と、自然数と、自然数の\(3 \times 2\)行列の配列、の\(3\)つ組の配列」です。そのような配列を後に順序数配列と呼んでいきます。ここでは空列も配列とみなす流儀を採用するので、例えば \begin{eqnarray*} & () & \\ & (((),0,())) & \\ & (((),1,())) & \\ & \left( \left( \left( \left( \begin{array}{cc} 0 & 0 \\ 0 & 0 \\ 0 & 0 \end{array} \right) \right) , 0 , () \right) \right) & \\ & \left( \left( \left( \left( \begin{array}{cc} 0 & 1 \\ 1 & 0 \\ 0 & 1 \end{array} \right) \right) , 0 , \left( \left( \begin{array}{cc} 0 & 0 \\ 0 & 0 \\ 0 & 0 \end{array} \right) \right) \right) \right) & \\ & \left( \left( \left( \left( \begin{array}{cc} 0 & 0 \\ 0 & 2 \\ 0 & 1 \end{array} \right) \right) , 1 , \left( \left( \begin{array}{cc} 4 & 0 \\ 1 & 0 \\ 1 & 0 \end{array} \right) \right) \right), ((),0,()) \right) & \\ & \left( ((),1,()) , \left( \left( \left( \begin{array}{cc} 0 & 0 \\ 1 & 1 \\ 0 & 0 \end{array} \right) \right) , 0 , \left( \left( \begin{array}{cc} 0 & 1 \\ 0 & 1 \\ 0 & 0 \end{array} \right) \right) \right) , ((),3,()) \right) & \\ & \left( \left( \left( \left( \begin{array}{cc} 0 & 0 \\ 0 & 0 \\ 0 & 0 \end{array} \right) , \left( \begin{array}{cc} 3 & 1 \\ 1 & 0 \\ 1 & 1 \end{array} \right) \right) , 0 , \left( \left( \begin{array}{cc} 0 & 0 \\ 0 & 0 \\ 0 & 0 \end{array} \right) \right) \right), ((),1,()) \right) & \end{eqnarray*} などが順序数配列の例となります。ちなみに対応する順序数を上からに並べると、\(0, \omega, \omega, \omega, \omega, \omega \times 2, \omega \times 3, \omega \times 2\)となります。ほとんどすべての順序数配列\(A\)に対して、\(A\)の長さを\(L\)と置くと\(A\)は\(\omega \times L\)に対応してしまいますが、ごくごく稀に有限順序数に対応するものや\(\omega^2\)を飛び出すものが紛れており、結果的に巨大基数の可算崩壊レベルすら上回るレベルの巨大順序数が現れます。

なお、順序数配列に対する基本列の定義は降下列の章で導入します。更に標準形の概念を限界関数の章で導入します。

あらすじ[]

お化けのありふれた世界では、お化け屋敷を開いてもいまいち話題性に欠けるようです。そこであなたは知り合いの河童に「一緒に巨大数屋敷を開いて一山当てないか？」と提案しました。河童の用意した設計図を頼りに、あなたは大小様々な斧を使って立派な巨大数屋敷を築き上げます。

チューリングマシンの対角化[]

超越整数システムやそれに類する計算可能関数を作る１つの手筋は、ゲーデル対応によってチューリングマシンそのものを対角化することである。その具体例としては万能チューリングマシンが知られているが、巨大関数を定義する上で万能チューリングマシンはやや煩雑なので、代わりにチューリング完全でかつ形式化が平易な計算モデルの対角化を行う。

記法と用語[]

非負整数のことをここでは自然数と呼ぶ。自然数全体の集合を\(\mathbb{N}\)と置く。配列に関する記法を導入する。まず\(S\)を集合とする。

自然数\(n\)に対し、\(S\)の要素のみを成分とする長さ\(n\)の配列^[1]全体のなす集合を\(S^n\)と置く。特に\(S^0\)は空列^[2]のみからなる集合である。ここでは空列を\(()\)と表す。「\(S\)の要素のみを成分とする長さ有限の配列」のことを単に「\(S\)の配列」と表現する。\(S\)の配列全体の集合^[3]を\(S^{< \omega}\)と置く。

\(a\)を\(S\)の配列とする。\(a\)の長さを\(\textrm{Lng}(a)\)と表す。各自然数\(i\)に対し\(a_i\)を以下のように定める：

\(i < \textrm{Lng}(a)\)ならば、\(a_i\)は\(a\)の\(i+1\)番目の成分^[4]である。
\(i \geq \textrm{Lng}(a)\)ならば、\(a_i = 0\)である。

\(a\)が添え字付きの記号や複数の文字からなる記号で表されているなどの事情で\(a_i\)という表記が判読しにくくなる時は、代わりに\([a]_i\)と表記する^[5]。\(a \neq ()\)である時、\(a\)の右端の成分を\(\textrm{Last}(a)\)と表す^[6]。

\(S\)の配列\(a,b\)に対し、\(a\)と\(b\)をこの順に結合して得られる配列を\(a \frown b \in S^{< \omega}\)と置く。すなわち\(a \frown b\)は\(\textrm{Lng}(a \frown b) = \textrm{Lng}(a) + \textrm{Lng}(b)\)を満たしかつ\(\textrm{Lng}(a \frown b)\)未満のいかなる\(i \in \mathbb{N}\)に対しても \begin{eqnarray*} [a \frown b]_i = \left\{ \begin{array}{ll} a_i & (i < \textrm{Lng}(a)) \\ b_{i - \textrm{Lng}(a)}& (i \geq \textrm{Lng}(a)) \end{array} \right. \end{eqnarray*} を満たす唯一の配列である。

\((\mathbb{N}^3)^2\)を\(\textrm{Mat}_{3,2}\)と置く。\(A \in \textrm{Mat}_{3,2}\)と\(i,j \in \mathbb{N}\)に対し、\(A_{i,j} = [A_j]_i\)と置く。\(A\)が添え字付きの記号や複数の文字からなる記号で表されているなどの事情で\(A_{i,j}\)という表記が判読しにくくなる時は、代わりに\([a]_{i,j}\)と表記する

例えば\(\mathbb{N}^3\)は自然数の\(3\)次元ベクトル全体のなす集合であり、\(\textrm{Mat}_{3,2}\)は自然数の\(3 \times 2\)行列全体のなす集合である。各\(M \in \textrm{Mat}_{3,2}\)は配列としての成分表示を用いると \begin{eqnarray*} ((M_{0,0},M_{1,0},M_{2,0}),(M_{0,1},M_{1,1},M_{2,1})) \end{eqnarray*} と表せ、行列としての成分表示を用いると \begin{eqnarray*} \left( \begin{array}{cc} M_{0,0} & M_{0,1} \\ M_{1,0} & M_{1,1} \\ M_{2,0} & M_{2,1} \end{array} \right) \end{eqnarray*} と表せる。

\(\textrm{Mat}_{3,2}\)の要素、すなわち自然数の\(3 \times 2\)行列のことを、ここでは「コード行列」と呼ぶ^[7]。

\(\textrm{Mat}_{3,2}^{< \omega}\)の要素、すなわちコード行列の配列のことを、ここでは「コード配列」と呼ぶ。例えば空列\(()\)はコード配列である。次の実装の章において、コード配列がソースコードとして機能しコード行列がソースコードの１行として機能するような計算モデルを導入する。

実装[]

コード配列がどのようにチューリング完全な計算モデルを与えるかを説明する。チューリングマシンよりコード配列のほうが単純なデータである分、実装は煩雑になる。

\(\mathbb{N}^3\)の要素、すなわち自然数の\(3\)次元ベクトルのことを、ここでは「ポインタベクトル」と呼ぶ。

\(\mathbb{N}^{< \omega}\)の要素、すなわち自然数の配列のことを、ここでは「メモリ数列」と呼ぶ。例えば空列\(()\)はメモリ数列である。

\(M\)をメモリ数列とし、\(L = \textrm{Lng}(M)\)と置く。\(L\)未満の自然数\(p\)と\(M_p\)未満の自然数\(m\)に対し、 \begin{eqnarray*} \textrm{Sep}(M,p,m) = \left\{ \begin{array}{ll} (m,M_0-m-1) & (0 = p = L-1) \\ (m,M_0-m-1,M_1,\ldots,M_{L-1}) & (0 = p < L-1) \\ (M_0,\ldots,M_{p-1},m,M_p-m-1) & (0 < p = L-1) \\ (M_0,\ldots,M_{p-1},m,M_p-m-1,M_{p+1},\ldots,M_{L-1}) & (0 < p < L-1) \\ \end{array} \right. \end{eqnarray*} と定める。\(\ldots\)を用いずにより厳密に表すと、\(\textrm{Sep}(M,p,m)\)は以下を満たす唯一の配列である：

\(\textrm{Lng}(\textrm{Sep}(M,p,m)) = L+1\)である。
いかなる自然数\(i\)に対しても以下が成り立つ：
1. \(i < p\)ならば\(\textrm{Sep}(M,p,m)_i = M_i\)である。
2. \(i = p\)ならば\(\textrm{Sep}(M,p,m)_i = m\)である。
3. \(i = p+1\)ならば\(\textrm{Sep}(M,p,m)_i = M_p - m - 1\)である。
4. \(i > p+1\)ならば\(\textrm{Sep}(M,p,m)_i = M_{i-1}\)である。

\(M\)をメモリ数列とし、\(L = \textrm{Lng}(M)\)と置く。\(L\)未満の自然数\(p\)に対し、 \begin{eqnarray*} \textrm{Cmb}(M,p) = \left\{ \begin{array}{ll} (M_0+1,0) & (0 = p = L-1) \\ (M_0+1+M_1,0) & (0 = p = L-2) \\ (M_p+1+M_{p+1},M_{p+2},\ldots,M_{L-1}) & (0 = p < L-2) \\ (M_0,\ldots,M_{p-1},M_p+1,0) & (0 < p = L-1) \\ (M_0,\ldots,M_{p-1},M_p+1+M_{p+1},0) & (0 < p = L-2) \\ (M_0,\ldots,M_{p-1},M_p+1+M_{p+1},M_{p+2},\ldots,M_{L-1}) & (0 < p < L-2) \\ \end{array} \right. \end{eqnarray*} と定める。\(\ldots\)を用いずにより厳密に表すと、\(\textrm{Cmb}(M,p)\)は以下の性質を満たす唯一の配列である：

\(L' = \textrm{Cmb}(M,p)\)と置くと、以下が成り立つ：
1. \(p = L-1\)ならば\(L' = L+1\)である。
2. \(p = L-2\)ならば\(L' = L\)である。
3. \(p < L-2\)ならば\(L' = L-1\)である。
いかなる自然数\(i\)に対しても以下が成り立つ：
1. \(i < p\)ならば\(\textrm{Cmb}(M,p)_i = M_i\)である。
2. \(i = p\)ならば\(\textrm{Cmb}(M,p)_i = M_p + 1 + M_{p+1}\)である。
3. \(i > p\)ならば\(\textrm{Cmb}(M,p)_i = M_{i+1}\)である。

\(\Theta\)をコード配列とする。\(\Theta\)を用いてポインタベクトル\(P\)とメモリ数列\(M\)から新たなポインタベクトル\(P'\)とメモリ数列\(M'\)を以下のように定義する：

\(P_0 < \textrm{Lng}(\Theta)\)かつ\(P_1 < \textrm{Lng}(M)\)とする。
1. \(C = \Theta_{P_0}\)と置く。
2. \(x = M_{P_1}\)と置く。
3. 自然数\(j\)とメモリ数列\(M'\)を以下のように定める：
  1. \(P_2 \geq x\)とする。
    1. \(j = 0\)である。
    2. \(C_{2,j} = 0\)ならば、\(M' = M\)である。
    3. \(C_{2,j} > 0\)ならば、\(M' = \textrm{Cmb}(M,P_1)\)である。
  2. \(P_2 < x\)とする。
    1. \(j = 1\)である。
    2. \(C_{2,j} = 0\)ならば、\(M' = \textrm{Sep}(M,P_1,P_2)\)である。
    3. \(C_{2,j} > 0\)ならば、\(M' = M\)である。
4. 自然数\(p\)を以下のように定める：
  1. \(C_{1,j} = 0\)かつ\(P_1 > 0\)かつ\(P_2 = 0\)ならば、\(p = P_1-1\)である。
  2. \(C_{1,j} = 0\)かつ\(P_1 > 0\)かつ\(P_2 > 0\)ならば、\(p = P_1\)である。
  3. \(C_{1,j} = 0\)かつ\(P_1 = 0\)ならば、\(p = P_1\)である。
  4. \(C_{1,j} > 0\)かつ\(C_{2,j} > 0\)ならば、\(p = P_1\)である。
  5. \(C_{1,j} > 0\)かつ\(C_{2,j} = 0\)ならば、\(p = P_1+1\)である。
5. 自然数\(m\)を以下のように定める：
  1. \(C_{1,j} = 0\)かつ\(P_2 > 0\)ならば、\(m = P_2-1\)である。
  2. \(C_{1,j} = 0\)かつ\(P_2 = 0\)かつ\(P_1 > 0\)ならば、\(m = M_p\)である。
  3. \(C_{1,j} = 0\)かつ\(P_2 = 0\)かつ\(P_1 = 0\)ならば、\(m = P_2\)である。
  4. \(C_{1,j} > 0\)かつ\(C_{2,j} = 0\)ならば、\(m = 0\)である。
  5. \(C_{1,j} > 0\)かつ\(C_{2,j} > 0\)ならば、\(m = P_2+1\)である。
6. \(P' = (C_{0,j},p,m)\)である。
\(P_0 \geq \textrm{Lng}(\Theta)\)または\(P_1 \geq \textrm{Lng}(M)\)とする。
1. \(P' = P\)である。
2. \(M' = M\)である。

以上で\(\Theta\)による変換 \begin{eqnarray*} \textrm{App}_{\Theta} \colon \mathbb{N}^3 \times \mathbb{N}^{<\omega} & \to & \mathbb{N}^3 \times \mathbb{N}^{<\omega} \\ (P,M) & \mapsto & (P',M') \end{eqnarray*} を得る。

プログラミングで大雑把に例えると、\(M\)はメモリを表し、\(P_0\)は「今はソースコードのどの行を実行しているか」を表し、\(P_1\)と\(P_2\)は「今はメモリ上のどのアドレスを参照しているか」を表しており、\(j\)が\(0\)か\(1\)かに従って条件分岐をし、\(C_{0,j}\)は「次はソースコードのどの行を実行すればよいか」を表し、\(C_{1,j}\)は「次はどのアドレスを参照するか」を表し、\(C_{2,j}\)は「今参照しているアドレスに格納されている数値をどう書き換えるか」を表している。

\(2\)記号チューリングマシンに翻訳する際は、\(L = \textrm{Lng}(M)\)と置き、テープを表す自然数の無限列 \begin{eqnarray*} (\underbrace{1,\ldots,1}_{M_0},0,\underbrace{1,\ldots,1}_{M_1},0,\ldots,\underbrace{1,\ldots,1}_{M_{L-1}},0,0,\ldots) \end{eqnarray*} に\(M\)を変換し、ポインタベクトル\(P\)であって\(P_2 \leq M_{P_1}\)を満たすものを状態とヘッド位置を表す自然数の組\((P_0,P_2+\sum_{p = 0}^{P_1-1} (M_p+1))\)に変換すれば良い。この変換を通じてコード配列とチューリングマシンが等価な計算モデルであることは容易に確かめられる^[8]。

ちなみにこの翻訳を通じて、\(\textrm{Sep}\)は「ヘッダ位置に\(1\)があればそれを\(0\)に置き換えることで\(1\)の連続した羅列を２つに分割する」という操作に対応し、\(\textrm{Cmb}\)は「ヘッダ位置に\(0\)があればそれを\(1\)に置き換えることで\(1\)の連続した羅列２つを１つに結合する」という操作に対応する。それを踏まえると、アドレスを表すためにわざわざ\(P_1\)と\(P_2\)の２つを用いている理由が分かるだろう。それは、コード配列がチューリングマシンのように\(1\)の羅列として数値を格納しているのではなく、メモリ配列に値そのもので格納しているからである。チューリングマシンの言葉に置き換えると、\(P_2 < x\)であることは「ヘッド位置に\(1\)がある」ということを表し、\(P_2 = x\)であることは「ヘッド位置に\(0\)がある」ということを表しているのである^[9]。

なおチューリングマシンそのものではなくコード配列を用いる利点は、チューリングマシンだと厳密な定義そのものは配列の言葉で書かれておらずまた出力等の定式化もそこそこ面倒であるのに対しコード配列は配列を使うだけできっちり定義できるので、配列に対する操作で一括して単純に扱えることである。

さて、\(\textrm{App}_{\Theta}\)の定義をする際に固定していた\(\Theta\)を動かすことで、\(\textrm{App}\)自体もまた入れ子配列\((\Theta,P,M)\)に関する関数とみなすことができる。それもやはり計算可能であるため、\(\textrm{App}\)を実現するチューリングマシンなりコード配列なりを考えることもでき、それがいわゆる万能チューリングマシンである。今回は実際に\(\Theta\)を動かして\(\textrm{App}\)を適用していくので実質万能チューリングマシンを使っていることと等価であり、その意味でチューリングマシンを対角化している。

停止性[]

\(\Theta\)をコード配列とする。メモリ数列\(M\)に対し、「\(M\)を入力として\(\Theta\)が停止する」とは、\(\textrm{App}_{\Theta}^n((0,0,0),M) = \textrm{App}_{\Theta}^{n+1}((0,0,0),M)\)を満たす\(n \in \mathbb{N}\)が存在するということである。\(M\)を入力として\(\Theta\)が停止する時、\(\textrm{App}_{\Theta}^n((0,0,0),M) = \textrm{App}_{\Theta}^{n+1}((0,0,0),M)\)を満たす\(n \in \mathbb{N}\)の最小値を\(\textrm{Step}(\Theta,M)\)と書き、\((P_{\Theta,M},N_{\Theta,M}) = \textrm{App}_{\Theta}^{\textrm{Step}(\Theta,M)}((0,0,0),M) \in \mathbb{N}^3 \times \mathbb{N}^{<\omega}\)と置いた時の\(N_{\Theta,M}\)の成分の総和を\(\textrm{Output}_{\Theta}(M)\)と置き、「\(M\)を入力とする\(\Theta\)出力」と呼ぶ。

\(\textrm{Output}_{\Theta}\)は\(\mathbb{N}^{< \omega}\)の部分集合を定義域とする関数だが、その定義域の決定には一般に神託機械\(\textrm{Halt}\)を必要とし、定義域は再帰的部分集合とは限らない。

\(\mathbb{N}^{< \omega}\)の再帰的部分集合\(S\)に対し、「\(\Theta\)が\(S\)上で全域である」とは、いかなる\(M \in S\)に対しても\(M\)を入力として\(\Theta\)が停止するということであり、これはすなわち\(\textrm{Output}_{\Theta}\)の\(S\)への制限\(\textrm{Output}_{\Theta}^S\)が全域計算可能関数\(S \to \mathbb{N}\)であることに他ならない。

「\(\Theta\)が\(\mathbb{N}\)上で全域である」とは、いかなる\(n \in \mathbb{N}\)に対してもメモリ数列\((n)\)を入力として\(\Theta\)が停止するということであり、これはすなわち埋め込み \begin{eqnarray*} \mathbb{N} & \stackrel{\sim}{\to} & \mathbb{N}^1 \hookrightarrow \mathbb{N}^{< \omega} \\ n & \mapsto & (n) \end{eqnarray*} と\(\textrm{Output}_{\Theta}\)の合成写像\(\textrm{Output}_{\Theta}^{\mathbb{N}}\)が全域計算可能関数\(\mathbb{N} \to \mathbb{N}\)であることに他ならない。

例[]

コード配列\(\textrm{Id}\)を\(()\)と定める。この時、\(\textrm{Id}\)は\(\mathbb{N}^{< \omega}\)上で全域であるので特に\(\mathbb{N}\)上で全域であり、対応する全域計算可能関数\(\textrm{Output}_{\textrm{Id}}^{\mathbb{N}} \colon \mathbb{N} \to \mathbb{N}\)は恒等関数\(n \mapsto n\)に他ならない。

コード配列\(\textrm{Incr}\)を \begin{eqnarray*} \left( \left( \begin{array}{cc} 1 & 0 \\ 1 & 1 \\ 1 & 1 \end{array}\right) \right) \end{eqnarray*} と定める。この時、\(\textrm{Incr}\)は\(\mathbb{N}^{< \omega}\)上で全域であるので特に\(\mathbb{N}\)上で全域であり、対応する全域計算可能関数\(\textrm{Output}_{\textrm{Incr}}^{\mathbb{N}} \colon \mathbb{N} \to \mathbb{N}\)はインクリメント関数\(n \mapsto n+1\)に他ならない。

コード配列\(\textrm{ShiftRight}\)を \begin{eqnarray*} \left( \left( \begin{array}{cc} 0 & 0 \\ 1 & 1 \\ 0 & 1 \end{array}\right) \right) \end{eqnarray*} と定める。この時、\(\textrm{ShiftRight}\)は空列でないいかなるメモリ数列\(M\)に対しても\(M\)を入力として停止しないので、対応する計算可能関数\(\textrm{Output}_{\textrm{ShiftRight}}\)の定義域は\(\{()\}\)である。

なお、コード配列\(\Theta\)から計算可能関数\(\textrm{Output}_{\Theta}\)を定める対応は単射でないため、\(\textrm{Output}_{\Theta}\)から\(\Theta\)を復元することはできない。例えば、\(\textrm{Output}_{\Theta}\)の定義域が\(\emptyset\)であるようなコード配列\(\Theta\)は\(\textrm{ShiftRight}\)以外に無数に存在する。例えば\(\textrm{ShiftRight}\)と\(\textrm{Incr}\)を結合させたコード配列 \begin{eqnarray*} \textrm{ShiftRight} \frown \textrm{Incr} = \left( \left( \begin{array}{cc} 0 & 0 \\ 1 & 1 \\ 0 & 1 \end{array}\right), \left( \begin{array}{cc} 1 & 0 \\ 1 & 1 \\ 1 & 1 \end{array}\right) \right) \end{eqnarray*} もまた、対応する計算可能関数\(\textrm{Output}_{\textrm{ShiftRight} \frown \textrm{Incr}}\)の定義域が\(\emptyset\)となる。

さて、以下のように定めたコード行列\(\theta_{\omega}^{0},\theta_{\omega}^{1},\theta_{\omega}^{2},\theta_{\omega}^{3},\theta_{\omega}^{4},\theta_{\omega}^{5},\theta_{\omega}^{6},\theta_{\omega}^{7},\theta_{\omega}^{8},\theta_{\omega}^{9},\theta_{\omega}^{10},\theta_{\omega}^{11},\theta_{\omega}^{12}\)を用いて\((\theta_{\omega}^{0},\theta_{\omega}^{1},\theta_{\omega}^{2},\theta_{\omega}^{3},\theta_{\omega}^{4},\theta_{\omega}^{5},\theta_{\omega}^{6},\theta_{\omega}^{7},\theta_{\omega}^{8},\theta_{\omega}^{9},\theta_{\omega}^{10},\theta_{\omega}^{11},\theta_{\omega}^{12})\)と表されるコード配列\(\Theta_{\omega}\)を考える： \begin{eqnarray*} \theta_{\omega}^{0} & = & \left( \begin{array}{cc} 1 & 2 \\ 1 & 1 \\ 0 & 0 \end{array} \right) \\ \theta_{\omega}^{1} & = & \left( \begin{array}{cc} 13 & 1 \\ 1 & 1 \\ 1 & 0 \end{array} \right) \\ \theta_{\omega}^{2} & = & \left( \begin{array}{cc} 3 & 4 \\ 1 & 1 \\ 0 & 1 \end{array} \right) \\ \theta_{\omega}^{3} & = & \left( \begin{array}{cc} 13 & 1 \\ 1 & 1 \\ 0 & 0 \end{array} \right) \\ \theta_{\omega}^{4} & = & \left( \begin{array}{cc} 5 & 4 \\ 1 & 1 \\ 0 & 1 \end{array} \right) \\ \theta_{\omega}^{5} & = & \left( \begin{array}{cc} 6 & 7 \\ 0 & 1 \\ 0 & 1 \end{array} \right) \\ \theta_{\omega}^{6} & = & \left( \begin{array}{cc} 13 & 6 \\ 1 & 0 \\ 0 & 0 \end{array} \right) \\ \theta_{\omega}^{7} & = & \left( \begin{array}{cc} 8 & 9 \\ 0 & 1 \\ 0 & 1 \end{array} \right) \\ \theta_{\omega}^{8} & = & \left( \begin{array}{cc} 8 & 8 \\ 0 & 0 \\ 0 & 0 \end{array} \right) \\ \theta_{\omega}^{9} & = & \left( \begin{array}{cc} 10 & 9 \\ 0 & 1 \\ 0 & 1 \end{array} \right) \\ \theta_{\omega}^{10} & = & \left( \begin{array}{cc} 11 & 11 \\ 0 & 0 \\ 0 & 0 \end{array} \right) \\ \theta_{\omega}^{11} & = & \left( \begin{array}{cc} 12 & 11 \\ 0 & 0 \\ 0 & 1 \end{array} \right) \\ \theta_{\omega}^{12} & = & \left( \begin{array}{cc} 0 & 12 \\ 1 & 0 \\ 0 & 1 \end{array} \right) \end{eqnarray*} 定義を注意深く読み解くことで、\(\Theta_{\omega}\)が\(\mathbb{N}^2\)上で全域でありかつ\(\textrm{Output}_{\Theta_{\omega}}^{\mathbb{N}^2}\)が\(\mathbb{N}\)上の通常の順序を定めることが分かる^[10]。さらに以下のように定めたコード行列\(\varphi_{\omega}^{0},\varphi_{\omega}^{1},\varphi_{\omega}^{2},\varphi_{\omega}^{3},\varphi_{\omega}^{4},\varphi_{\omega}^{5}\)を用いて\((\varphi_{\omega}^{0},\varphi_{\omega}^{1},\varphi_{\omega}^{2},\varphi_{\omega}^{3},\varphi_{\omega}^{4},\varphi_{\omega}^{5})\)と表されるコード配列\(\Phi_{\omega}\)を考える： \begin{eqnarray*} \varphi_{\omega}^{0} & = & \left( \begin{array}{cc} 1 & 2 \\ 1 & 1 \\ 0 & 1 \end{array} \right) \\ \varphi_{\omega}^{1} & = & \left( \begin{array}{cc} 6 & 1 \\ 1 & 1 \\ 0 & 0 \end{array} \right) \\ \varphi_{\omega}^{2} & = & \left( \begin{array}{cc} 3 & 2 \\ 0 & 1 \\ 0 & 1 \end{array} \right) \\ \varphi_{\omega}^{3} & = & \left( \begin{array}{cc} 4 & 4 \\ 1 & 1 \\ 0 & 0 \end{array} \right) \\ \varphi_{\omega}^{4} & = & \left( \begin{array}{cc} 5 & 5 \\ 1 & 1 \\ 0 & 0 \end{array} \right) \\ \varphi_{\omega}^{5} & = & \left( \begin{array}{cc} 6 & 5 \\ 1 & 1 \\ 0 & 0 \end{array} \right) \end{eqnarray*} すると\(\Phi_{\omega}\)は\(\mathbb{N}^2\)上全域でありかつ \begin{eqnarray*} \textrm{Output}_{\Phi_{\omega}}(n_0,n_1) = \left\{ \begin{array}{ll} 0 & (n_0 = 0) \\ n_0-1 & (n_0 > 0) \end{array} \right. \end{eqnarray*} を満たすことが分かる。従って\(\textrm{Output}_{\Phi_{\omega}}^{\mathbb{N}^2}\)の定める二項演算は\(\textrm{Output}_{\Theta_{\omega}}^{\mathbb{N}^2}\)の定める再帰的整列順序に関する基本列系を与える。この例は後にも用いるので、命題として掲げておく。

命題（（\(\Theta_{\omega}\)と\(\Phi_{\omega}\)の基本性質）
\(\Theta_{\omega}\)は\(\mathbb{N}^2\)上で全域であり、かつ任意の\(m_0,m_1 \in \mathbb{N}\)に対し以下が同値である： \(\textrm{Output}_{\Theta_{\omega}}(m_0,m_1) = 1\)である。 \(\textrm{Output}_{\Theta_{\omega}}(m_0,m_1) = 0\)でない。 \(m_0 \leq m_1\)である。
更に\(\Phi_{\omega}\)は\(\mathbb{N}^2\)上で全域であり、かつ任意の\(m_0,m_1 \in \mathbb{N}\)に対し以下を満たす： \(m_0 = 0\)ならば\(\textrm{Output}_{\Theta_{\omega}}(m_0,m_1) = 0\)である。 \(m_0 > 0\)ならば\(\textrm{Output}_{\Theta_{\omega}}(m_0,m_1) = m_0-1\)である。

例えば\(M = (1,2)\)を入力とした時の\(\Theta_{\omega}\)の計算過程は以下のようになる：

ステップ数	メモリ数列	ポインタベクトル
0	(1,2)	(0,0,0)
1	(0,0,2)	(2,1,0)
2	(0,0,2)	(3,2,0)
3	(0,0,0,1)	(1,3,0)
4	(0,0,0,0,0)	(1,4,0)
5	(0,0,0,0,1,0)	(13,4,0)
6	(0,0,0,0,1,0)	(13,4,0)

\(M = (2,3)\)を入力とした時の\(\Theta_{\Phi}\)の計算過程は以下のようになる：

ステップ数	メモリ数列	ポインタベクトル
0	(2,3)	(0,0,0)
1	(2,3)	(2,0,1)
2	(2,3)	(2,0,2)
3	(2,3)	(3,0,1)
4	(1,0,3)	(4,1,0)
5	(1,0,3)	(5,2,0)
6	(1,0,0,2)	(5,3,0)
7	(1,0,0,0,1)	(5,4,0)
8	(1,0,0,0,0,0)	(5,5,0)
9	(1,0,0,0,0,0)	(6,6,0)
10	(1,0,0,0,0,0)	(6,6,0)

ZFC集合論の形式化[]

ゲーデル対応を用いて\(\textrm{ZFC}\)集合論の形式化を行う。また\(\textrm{FOST}\)のように最小限の言語を用いると「定義による拡大へ初等埋め込み可能であること」のようなメタ定理を繰り返し適用しないと\(\textrm{ZFC}\)集合論の論理式を現実的な文字数で記述できないが、メタ定理の適用方法には一意性がなく（その差は巨大数の定義にはどうせ\(\uparrow^4\)レベル程度の大きさで抑えられるので基本的には気にする必要がないのだが）またその適用方法も巨大数界隈にとってはブラックボックスとなっているだろうことから、最初から定義による拡大を十分に行った強力な言語を形式化する。

ただし形式言語や公理といった形式論理の用語を用いると（実際は平易な内容であっても）敬遠されてしまいやすいので、巨大数界隈における可読性を優先してここでは形式論理の用語を用いずに形式化を行う。具体的には、設計図を見ながら斧で屋敷を建築する。

もう少し詳細に流れを説明すると、入れ子になった配列を用いて屋敷配列や設計図配列や斧配列という概念を定義し、入れ子の複雑さを表す関数\(\textrm{EnumNestArray}\)の値を上から抑えた範囲内（有限個しかない）で設計図配列全体を探索し、その中でも斧配列を用いて表される「斧のみを用いる」という条件を満たすものを全て選び、それらに対応する屋敷配列からコード配列を取り出すことが出来る。そうやって取り出したコード配列に対応する計算機構はいずれも順序数表記のような働きをするため、ある意味で大量の順序数表記を自動で生成するようなシステムとなる。これにより「順序数表記という概念そのものを対角化したような表記」を得られるので、後はFGHをするだけで良い。細かいことを言うときちんと基本列が機能するように、実際はコード配列から作った順序数表記そのものでなくコード配列の配列から作った順序数表記の配列を扱うことになるが、この点がこれまでの試みと大きく異なるところであり、かつ様々な技術的困難を回避する鍵となる。

入れ子配列[]

集合\(\textrm{NestArray}\)を、以下を満たす最小の集合として定める：

いかなる\(n \in \mathbb{N}\)に対しても\(n \in \textrm{NestArray}\)である。
いかなる\(A \in \textrm{NestArray}^{< \omega}\)に対しても\(A \in \textrm{NestArray}\)である。

\(\textrm{NestArray}\)の要素を「入れ子配列」と呼ぶ。

例えば\(0\)や\((1)\)や\((2,(3),((45,6),7,(8),9))\)は入れ子配列だが、\(\omega\)や\(\{1\}\)や\(\mathbb{R}\)は入れ子配列でない。

また自然数のみを成分に持つ\(3\)次元ベクトルは入れ子配列であり、自然数のみを成分に持つ\(3 \times 2\)行列はそのようなベクトルの組であるので入れ子配列であり、コード配列はそのような行列の配列であるためやはり入れ子配列である。

\(n \in \mathbb{N}\)に対し、入れ子配列\(\textrm{EnumNestArray}(n)\)を以下のように再帰的に定める：

\(n\)が偶数であるならば、\(\textrm{EnumNestArray}(n) = \frac{n}{2}\)である。
\(n\)が奇数であるとする。
1. \(m_0 = \frac{n+1}{2}\)と置く。
2. \(2^i \leq m_0\)を満たす最大の\(i \in \mathbb{N}\)を\(a_0\)と置く。
3. \(m_1 = m_0 - 2^{a_0}\)と置く。
4. \(m_1 = 0\)ならば、\(\textrm{EnumNestArray}(n) = (\textrm{EnumNestArray}(a_0))\)である。
5. \(m_1 \neq 0\)とする。
  1. \(2^i \leq m_1\)を満たす最大の\(i \in \mathbb{N}\)を\(a_1\)と置く。
  2. \(A_0 = \textrm{EnumNestArray}(2m_1-1)\)と置く。
  3. \(A_1 = \textrm{EnumNestArray}(a_0-a_1-1)\)と置く。
  4. \(\textrm{EnumNestArray}(n) = A_0 \frown (A_1)\)である。

以上で全単射 \begin{eqnarray*} \textrm{EnumNestArray} \colon \mathbb{N} & \to & \textrm{NestArray} \\ n & \mapsto & \textrm{EnumNestArray}(n) \end{eqnarray*} を得る。

以下に\(\textrm{EnumNestArray}\)の計算例を挙げる：

\(n\)	\(\textrm{EnumNestArray}(n)\)
\(0\)	\(0 = ()\)
\(1\)	\((0)\)
\(2\)	\(1\)
\(3\)	\(((0))\)
\(4\)	\(2\)
\(5\)	\((0,0)\)
\(6\)	\(3\)
\(7\)	\((1)\)
\(8\)	\(4\)
\(9\)	\((0,(0))\)
\(10\)	\(5\)
\(35\)	\(((0),1)\)
\(36\)	\(18\)
\(99\)	\(((0),1,0)\)
\(100\)	\(50\)
\(1123\)	\(((0),1,0,((0)))\)
\(1124\)	\(562\)
\(999999\)	\((((0,0)),2,(0),0,0,0)\)
\(1000000\)	\(500000\)

略記[]

\(i\)を自然数とし、以下のように入れ子配列の略記を導入する： \begin{eqnarray*} \textrm{ConstantTerm} & = & 0 \\ \textrm{VariableTerm} & = & 1 \\ \textrm{Function} & = & 2 \\ \textrm{Schema} & = & 3 \\ \textrm{Relation} & = & 4 \\ \textrm{Formula} & = & 5 \\ \textrm{LogicalConnective} & = & 6 \\ \textrm{Quantifier} & = & 7 \end{eqnarray*}

\begin{eqnarray*} c_i & = & (\textrm{ConstantTerm},0,i) \\ c_{\mathbb{N}} & = & (\textrm{ConstantTerm},1) \end{eqnarray*}

\begin{eqnarray*} x_i & = & (\textrm{VariableTerm},0,i) \end{eqnarray*}

\begin{eqnarray*} f_{\{,\}} & = & (\textrm{Function},0) \\ f_{\{\}} & = & (\textrm{Function},1) \\ f_{(,)} & = & (\textrm{Function},2) \\ f_{\bigcup} & = & (\textrm{Function},3) \\ f_{\cup} & = & (\textrm{Function},4) \\ f_S & = & (\textrm{Function},5) \\ f_{\cap} & = & (\textrm{Function},6) \\ f_{\times} & = & (\textrm{Function},7) \\ f_{\wedge} & = & (\textrm{Function},8) \\ f_{\bullet ()} & = & (\textrm{Function},9) \\ f_{\mathcal{P}} & = & (\textrm{Function},10) \\ f_{+} & = & (\textrm{Function},11) \\ f_{-} & = & (\textrm{Function},12) \end{eqnarray*}

\begin{eqnarray*} \varphi_{\{\mid\}} & = & (\textrm{Schema},0) \end{eqnarray*}

\begin{eqnarray*} R_{=} & = & (\textrm{Relation},0) \\ R_{\in} & = & (\textrm{Relation},1) \\ R_{\subset} & = & (\textrm{Relation},2) \end{eqnarray*}

\begin{eqnarray*} F_{\perp} & = & (\textrm{Formula},0) \end{eqnarray*}

\begin{eqnarray*} L_{\wedge} & = & (\textrm{LogicalConnective},0) \\ L_{\vee} & = & (\textrm{LogicalConnective},1) \\ L_{\to} & = & (\textrm{LogicalConnective},2) \\ L_{\neg} & = & (\textrm{LogicalConnective},3) \end{eqnarray*}

\begin{eqnarray*} Q_{\forall} & = & (\textrm{Quantifier},0) \\ Q_{\exists} & = & (\textrm{Quantifier},1) \\ Q_! & = & (\textrm{Quantifier},2) \end{eqnarray*} もちろんこれらはただの配列なので「意味」はないのだが、それはさておき\(Q_!\)は便宜上導入した「一意性」を表す量化子に相当する配列である。またそれ以外の配列は一階集合論の通常の言語に包含関係や順序対や和集合などの汎用的な概念の定義式を「定義による拡大」によって予め記号として導入しているだけである。もちろんそういった背景知識を仮定せずに全ての定義を書き切るため知らなくても心配する必要はない。

項配列\(A_0,A_1,A_2,A_3,A_4\)に対し、以下のように略記を定める^[11]： \begin{eqnarray*} (R_{\neq},A_0,A_1) & = & (L_{\neg},(R_{=},A_0,A_1)) \\ (R_{\notin},A_0,A_1) & = & (L_{\neg},(R_{\in},A_0,A_1)) \\ (L_{\wedge \wedge},A_0,A_1,A_2) & = & (L_{\wedge},(L_{\wedge},A_0,A_1),A_2) \\ (L_{\leftrightarrow},A_0,A_1) & = & (L_{\wedge},(L_{\to},A_0,A_1),(L_{\to},A_1,A_0)) \\ (Q_{\exists !},A_0,A_1) & = & (L_{\wedge},(Q_{\exists},A_0,A_1),(Q_!,A_0,A_1)) \\ (Q_{\forall \forall},A_0,A_1,A_2) & = & (Q_{\forall},A_0,(Q_{\forall},A_1,A_2)) \\ (Q_{\forall \exists !},A_0,A_1,A_2) & = & (Q_{\forall},A_0,(Q_{\exists !},A_1,A_2)) \\ (Q_{\exists \forall},A_0,A_1,A_2) & = & (Q_{\exists},A_0,(Q_{\forall},A_1,A_2)) \\ (Q_{\exists \exists},A_0,A_1,A_2) & = & (Q_{\exists},A_0,(Q_{\exists},A_1,A_2)) \\ (Q_{\forall \forall \forall},A_0,A_1,A_2,A_3) & = & (Q_{\forall},A_0,(Q_{\forall \forall},A_1,A_2,A_3)) \\ (Q_{\forall \in},A_0,A_1,A_2) & = & (Q_{\forall},A_0,(L_{\to},(R_{\in},A_0,A_1),A_2)) \\ (Q_{\exists \in},A_0,A_1,A_2) & = & (Q_{\exists},A_0,(L_{\wedge},(R_{\in},A_0,A_1),A_2)) \\ (Q_{\forall \forall \in},A_0,A_1,A_2,A_3) & = & (Q_{\forall \in},A_0,A_2,(Q_{\forall \in},A_1,A_2,A_3)) \\ (Q_{\forall \exists \in},A_0,A_1,A_2,A_3) & = & (Q_{\forall \in},A_0,A_2,(Q_{\exists \in},A_1,A_2,A_3)) \\ (Q_{\exists \in \exists \in},A_0,A_1,A_2,A_3,A_4) & = & (Q_{\exists \in},A_0,A_1,(Q_{\exists \in},A_2,A_3,A_4)) \\ (Q_{\forall \forall \forall \in},A_0,A_1,A_2,A_3,A_4) & = & (Q_{\forall \in},A_0,A_3,(Q_{\forall \forall \in},A_1,A_2,A_3,A_4)) \\ \end{eqnarray*}

複雑な配列を見ると略記であることを忘れて「これの意味は何だろう？」と気になってしまうかもしれないが、これらは単なる入れ子配列の略記に過ぎないのでやはり「意味」はない。例えば入れ子配列\((Q_{\exists},x_0,(Q_{\forall},x_1,(L_{\neg},(R_{\in},x_1,x_0)))\)を略記せずに書き下すと以下のようになる： \begin{eqnarray*} & & (Q_{\exists},x_0,(Q_{\forall},x_1,(L_{\neg},(R_{\in},x_1,x_0))) \\ & = & (Q_{\exists},(\textrm{VariableTerm},0,0),(Q_{\forall},x_1,(L_{\neg},(R_{\in},x_1,(\textrm{VariableTerm},0,0)))) \\ & = & (Q_{\exists},(1,0,0),(Q_{\forall},x_1,(L_{\neg},(R_{\in},x_1,(1,0,0)))) \\ & = & (Q_{\exists},(1,0,0),(Q_{\forall},(\textrm{VariableTerm},0,1),(L_{\neg},(R_{\in},(\textrm{VariableTerm},0,1),(1,0,0)))) \\ & = & (Q_{\exists},(1,0,0),(Q_{\forall},(1,0,1),(L_{\neg},(R_{\in},(1,0,1),(1,0,0)))) \\ & = & (Q_{\exists},(1,0,0),(Q_{\forall},(1,0,1),(L_{\neg},((\textrm{Relation},1),(1,0,1),(1,0,0)))) \\ & = & (Q_{\exists},(1,0,0),(Q_{\forall},(1,0,1),(L_{\neg},((4,1),(1,0,1),(1,0,0)))) \\ & = & (Q_{\exists},(1,0,0),(Q_{\forall},(1,0,1),((\textrm{LogicalConnective},3),((4,1),(1,0,1),(1,0,0)))) \\ & = & (Q_{\exists},(1,0,0),(Q_{\forall},(1,0,1),((6,3),((4,1),(1,0,1),(1,0,0)))) \\ & = & ((\textrm{Quantifier},1),(1,0,0),((\textrm{Quantifier},0),(1,0,1),((6,3),((4,1),(1,0,1),(1,0,0)))) \\ & = & ((7,1),(1,0,0),((7,0),(1,0,1),((6,3),((4,1),(1,0,1),(1,0,0)))) \end{eqnarray*}

項配列[]

入れ子配列\(c\)が「定項配列である」とは、以下のいずれかを満たすということである：

\(c = c_i\)を満たす\(i \in \mathbb{N}\)が存在する。
\(c = c_{\mathbb{N}}\)である。

入れ子配列\(f\)が「引数\(1\)関数配列である」とは、\(f\)が\(f_{\{\}}\)か\(f_{\bigcup}\)か\(f_S\)か\(f_{\mathcal{P}}\)のいずれかと等しいということである。

入れ子配列\(f\)が「引数\(2\)関数配列である」とは、\(f\)が\(f_{\{,\}}\)か\(f_{(,)}\)か\(f_{\cup}\)か\(f_{\cap}\)か\(f_{\times}\)か\(f_{\wedge}\)か\(f_{\bullet ()}\)か\(f_{+}\)か\(f_{-}\)のいずれかと等しいということである。

部分集合\(\textrm{TermArray} \subset \textrm{NestArray}\)を、以下を満たす最小の集合として定める：

いかなる定項配列\(c\)に対しても、\(c \in \textrm{TermArray}\)である。
いかなる\(i \in \mathbb{N}\)に対しても\(x_i \in \textrm{TermArray}\)である。
いかなる引数\(1\)関数配列\(f\)と\(t \in \textrm{TermArray}\)に対しても\((f,t) \in \textrm{TermArray}\)である。
いかなる引数\(2\)関数配列\(f\)と\(t_0,t_1 \in \textrm{TermArray}\)に対しても\((f,t_0,t_1) \in \textrm{TermArray}\)である。
いかなる\(i \in \mathbb{N}\)と入れ子配列\(F\)に対しても\((\varphi_{\{\mid\}},x_i,F) \in \textrm{TermArray}\)である。

\(\textrm{TermArray}\)の要素を「項配列」と呼ぶ。

屋敷配列[]

入れ子配列\(R\)が「引数\(2\)関係配列である」とは、\(R\)が\(R_{=}\)か\(R_{\in}\)か\(R_{\subset}\)のいずれかと等しいということである。

入れ子配列\(L\)が「引数\(2\)論理結合子配列である」とは、\(L\)が\(L_{\wedge}\)か\(L_{\vee}\)か\(L_{\to}\)のいずれかと等しいということである。

入れ子配列\(Q\)が「量化子配列である」とは、\(Q\)が\(Q_{\forall}\)か\(Q_{\exists}\)か\(Q_!\)のいずれかと等しいということである。

部分集合\(\textrm{FormulaArray} \subset \textrm{NestArray}\)を、以下を満たす最小の集合として定める：

\(F_{\perp} \in \textrm{FormulaArray}\)である。
いかなる引数\(2\)関係配列\(R\)と項配列\(t_0, t_1\)に対しても\((R,t_0,t_1) \in \textrm{FormulaArray}\)である。
いかなる\(F \in \textrm{FormulaArray}\)に対しても\((L_{\neg},F) \in \textrm{FormulaArray}\)である。
いかなる引数\(2\)論理結合子配列\(L\)と\(F_0, F_1 \in \textrm{FormulaArray}\)に対しても\((L,F_0,F_1) \in \textrm{FormulaArray}\)である。
いかなる量化子配列\(Q\)と\(i \in \mathbb{N}\)と\(F \in \textrm{FormulaArray}\)に対しても\((Q,x_i,F) \in \textrm{FormulaArray}\)である。

\(\textrm{FormulaArray}\)の要素を「屋敷配列」と呼ぶ。

代入[]

\(i \in \mathbb{N}\)に対し、部分集合\(\textrm{Occur}_i \subset \textrm{NestArray}\)を、以下を満たす最小の集合として定める：

\(x_i \in \textrm{Occur}_i\)である。
いかなる\(A \in \textrm{NestArray}^{< \omega}\)に対しても、\(A_j \in \textrm{Occur}_i\)を満たす\(j \in \mathbb{N}\)が存在すれば\(A \in \textrm{Occur}_i\)である。

\(i \in \mathbb{N}\)に対し、部分集合\(\textrm{FreeOccur}_i \subset \textrm{TermArray} \cup \textrm{FormulaArray}\)を、以下を満たす最小の集合として定める：

\(x_i \in \textrm{FreeOccur}_i\)である。
いかなる引数\(1\)関数配列\(f\)と項配列\(t\)に対しても、\(t \in \textrm{FreeOccur}_i\)ならば\((f,t) \in \textrm{FreeOccur}_i\)である。
いかなる引数\(2\)関数配列\(f\)と項配列\(t_0,t_1\)に対しても、\(t_0 \in \textrm{FreeOccur}_i\)または\(t_1 \in \textrm{FreeOccur}_i\)ならば\((f,t_0,t_1) \in \textrm{FreeOccur}_i\)である。
\(j \neq i\)を満たすいかなる\(j \in \mathbb{N}\)と屋敷配列\(F\)に対しても、\(F \in \textrm{FreeOccur}_i\)ならば\((\varphi_{\{\mid\}},x_j,F) \in \textrm{FreeOccur}_i\)である。
いかなる引数\(2\)関係配列\(R\)と項配列\(t_0, t_1\)に対しても、\(t_0 \in \textrm{FreeOccur}_i\)または\(t_1 \in \textrm{FreeOccur}_i\)ならば、\((R,t_0,t_1) \in \textrm{FreeOccur}_i\)である。
いかなる屋敷配列\(F\)に対しても、\(F \in \textrm{FreeOccur}_i\)ならば\((L_{\neg},F) \in \textrm{FreeOccur}_i\)である。
いかなる引数\(2\)論理結合子配列\(L\)と屋敷配列\(F_0,F_1\)に対しても、\(F_0 \in \textrm{FreeOccur}_i\)または\(F_1 \in \textrm{FreeOccur}_i\)ならば、\((L,F_0,F_1) \in \textrm{FreeOccur}_i\)である。
いかなる量化子配列\(Q\)と\(j \in \mathbb{N}\)と屋敷配列\(F\)に対しても、\(j \neq i\)かつ\(F \in \textrm{FreeOccur}_i\)ならば、\((Q,x_j,F) \in \textrm{FreeOccur}_i\)である。

項配列\(t\)と\(i \in \mathbb{N}\)に対し、部分集合\(\textrm{Substitutable}_{t,x_i} \subset \textrm{TermArray} \cup \textrm{FormulaArray}\)を、以下を満たす最小の集合として定める：

いかなる定項配列\(c\)に対しても、\(c \in \textrm{Substitutable}_{t,x_i}\)である。
いかなる\(j \in \mathbb{N}\)に対しても\(x_j \in \textrm{Substitutable}_{t,x_i}\)である。
いかなる引数\(1\)関数配列\(f\)と項配列\(s\)に対しても、\(s \in \textrm{Substitutable}_{t,x_i}\)ならば\((f,s) \in \textrm{Substitutable}_{t,x_i}\)である。
いかなる引数\(2\)関数配列\(f\)と項配列\(s_0,s_1\)に対しても、\(s_0,s_1 \in \textrm{Substitutable}_{t,x_i}\)ならば\((f,s_0,s_1) \in \textrm{Substitutable}_{t,x_i}\)である。
いかなる\(j \in \mathbb{N}\)と屋敷配列\(F\)に対しても、\((Q_{\exists},x_j,F) \in \textrm{Substitutable}_{t,x_i}\)ならば\((\varphi_{\{\mid\}},x_j,F) \in \textrm{Substitutable}_{t,x_i}\)である。
いかなる引数\(2\)関係配列\(R\)と項配列\(s_0, s_1\)に対しても、\(s_0,s_1 \in \textrm{Substituable}_{t,x_i}\)ならば\((R,s_0,s_1) \in \textrm{Substitutable}_{t,x_i}\)である。
いかなる\(F \in \textrm{Substitutable}_{t,x_i}\)に対しても、\((L_{\neg},F) \in \textrm{Substitutable}_{t,x_i}\)である。
いかなる引数\(2\)論理結合子配列\(L\)と屋敷配列\(F_0,F_1\)に対しても、\(F_0,F_1 \in \textrm{Substitutable}_{t,x_i}\)ならば、\((L,F_0,F_1) \in \textrm{Substitutable}_{t,x_i}\)である。
いかなる量化子配列\(Q\)と屋敷配列\(F\)に対しても、\((Q,x_i,F) \in \textrm{Substitutable}_{t,x_i}\)である。
いかなる量化子配列\(Q\)と\(j \in \mathbb{N}\)と屋敷配列\(F\)に対しても、\(t \notin \textrm{Occur}_j\)または\(F \notin \textrm{FreeOccur}_i\)ならば\((Q,x_j,F) \in \textrm{Substitutable}_{t,x_i}\)である。

入れ子配列が\(\textrm{Substitutable}_{t,x_i}\)に属することを「\([t/x_i]\)可能である」という。例えば\(\textrm{Substitutable}_{x_1,x_0}\)に属さない屋敷配列の典型例として\((Q_{\exists},x_1,(L_{\neg},(R_{=},x_0,x_1))\)が挙げられる。いかにも\(\textrm{Substitutable}_{x_1,x_0}\)に属さない形をしているだろう。

項配列\(t\)と\(i \in \mathbb{N}\)と\(A \in \textrm{Substitutable}_{t,x_i}\)に対し、\(A[t/x_i] \in \textrm{TermArray} \cup \textrm{FormulaArray}\)を以下のように再帰的に定める：

\(A\)が定項配列ならば、\(A[t/x_i] = A\)である。
\(A = x_i\)ならば、\(A[t/x_i] = t\)である。
\(A = x_j\)と\(j \neq i\)を満たす\(j \in \mathbb{N}\)が存在するならば、\(A[t/x_i] = A\)である。
\(A = (f,u)\)を満たす引数\(1\)関数配列\(f\)と項配列\(u\)が存在するならば、\(A[t/x_i] = (f,u[t/x_i])\)である。
\(A = (f,u_0,u_1)\)を満たす引数\(2\)関数配列\(f\)と項配列\(u_0,u_1\)が存在するならば、\(A[t/x_i] = (f,u_0[t/x_i],u_1[t/x_i])\)である。
\(A = (\varphi_{\{\mid\}},x_i,F)\)を満たす屋敷配列\(F\)が存在するならば、\(A[t/x_i] = A\)である。
\(A = (\varphi_{\{\mid\}},x_j,F)\)かつ\(j \neq i\)を満たす\(j \in \mathbb{N}\)と屋敷配列\(F\)が存在するならば、\(A[t/x_i] = (\varphi_{\{\mid\}},x_j,F[t/x_i])\)である。
\(A = F_{\perp}\)ならば、\(A[t/x_i] = A\)である。
\(A = (R,u_0,u_1)\)を満たす引数\(2\)関係配列\(R\)と項配列\(u_0, u_1\)が存在するならば、\(A[t/x_i] = (R,u_0[t/x_i],u_1[t/x_i])\)である。
\(A = (L_{\neg},G)\)を満たす屋敷配列\(G\)が存在するならば、\(A[t/x_i] = (L_{\neg},G[t/x_i])\)である。
\(A = (L,G_0,G_1)\)を満たす引数\(2\)論理結合子配列\(L\)と屋敷配列\(G_0,G_1\)が存在するならば、\(A[t/x_i] = (L,G_0[t/x_i],G_1[t/x_i])\)である。
\(A = (Q,x_i,G)\)を満たす量化子配列\(Q\)と屋敷配列\(G\)が存在するならば、\(A[t/x_i] = A\)である。
\(A = (Q,x_j,G)\)を満たす量化子配列\(Q\)と\(i\)と異なる\(j \in \mathbb{N}\)と屋敷配列\(G\)が存在するならば、\(A[t/x_i] = (Q,x_j,G[t/x_i])\)である。

以下に\(A[x_1/x_0]\)の計算例を挙げる：

\(A\)	\(A[x_1/x_0]\)
\(c_0\)	\(c_0\)
\(x_0\)	\(x_1\)
\(x_1\)	\(x_1\)
\(x_2\)	\(x_2\)
\((f_{\bigcup},x_0)\)	\((f_{\bigcup},x_1)\)
\((f_{\{,\}},x_1,x_0)\)	\((f_{\{,\}},x_1,x_1)\)
\((f_{(,)},x_0,x_0)\)	\((f_{(,)},x_1,x_1)\)
\(F_{\perp}\)	\(F_{\perp}\)
\((R_{=},x_0,x_1)\)	\((R_{=},x_1,x_1)\)
\((R_{\in},x_2,x_0)\)	\((R_{\in},x_2,x_1)\)
\((R_{\subset},x_0,x_0)\)	\((R_{\subset},x_1,x_1)\)
\((L_{\to},(R_{=},x_0,x_1),(R_{\in},x_1,x_2))\)	\((L_{\to},(R_{=},x_1,x_1),(R_{\in},x_1,x_2))\)
\((Q_{\exists},x_0,(R_{\in},x_0,x_1))\)	\((Q_{\exists},x_0,(R_{\in},x_0,x_1))\)
\((Q_{\exists},x_1,(R_{\subset},x_0,x_1))\)	未定義（\(A\)は\([x_1/x_0]\)可能でない）
\((Q_{\exists},x_2,(R_{=},x_0,x_2))\)	\((Q_{\exists},x_2,(R_{=},x_1,x_2))\)
\((L_{\wedge},(Q_{\exists},x_0,(R_{\in},x_0,x_1)),(Q_{\exists},x_2,(R_{=},x_0,x_2)))\)	\((L_{\wedge},(Q_{\exists},x_0,(R_{\in},x_0,x_1)),(Q_{\exists},x_2,(R_{=},x_1,x_2)))\)

斧配列[]

項配列\(A_0,A_1,A_2,A_3,A_4\)に対し、以下のように略記を定める： \begin{eqnarray*} (\textrm{Cmp},A_0,A_1) & = & (Q_{\forall},A_0,(L_{\leftrightarrow},(R_{\in},A_0,(\varphi_{\{\mid\}},A_0,A_1)),A_1)) \\ (\textrm{Pair},A_0,A_1,A_2,A_3,A_4) & = & (Q_{\exists \in \exists \in},A_0,A_1,A_2,A_3,(R_{=},A_4,(f_{(,)},A_0,A_2))) \\ (\textrm{Cor},A_0,A_1,A_2) & = & (R_{\in},(f_{(,)},A_0,A_1),A_2) \\ (\textrm{Val},A_0,A_1,A_2) & = & (L_{\to},(Q_{\exists !},A_0,(\textrm{Cor},A_1,A_0,A_2)),(\textrm{Cor},A_1,(f_{\bullet ()},A_2,A_1)),A_2)) \\ (\textrm{NaN},A_0,A_1,A_2) & = & (L_{\to},(L_{\neg},(Q_{\exists !},A_0,(\textrm{Cor},A_1,A_0,A_2))),(R_{=},(f_{\bullet ()},A_2,A_1),c_0)) \\ (\textrm{Fnc},A_0,A_1,A_2,A_3) & = & (Q_{\forall \in},A_0,A_1,(Q_{\exists !},A_2,(\textrm{Cor}(A_0,A_2,A_3)))) \\ (\textrm{Map},A_0,A_1,A_2,A_3,A_4) & = & (L_{\wedge},(R_{\subset},A_0,(f_{\times},A_1,A_2)),(\textrm{Fnc},A_3,A_1,A_4,A_0)) \\ (\textrm{Choi},A_0,A_1,A_2) & = & (Q_{\forall \in},A_0,A_1,(R_{\in},(f_{\bullet ()},A_2,A_0),A_2)) \end{eqnarray*}

部分集合\(\textrm{AxArray} \subset \textrm{FormulaArray}\)を、以下を満たす最小の集合として定める：

いかなる\(i \in \mathbb{N}\)に対しても、\((Q_{\forall},x_i,(R_{=},x_i,x_i)) \in \textrm{AxArray}\)である。
いかなる項配列\(t_0,t_1\)と引数\(1\)関数配列\(f\)に対しても、\((L_{\to},(R_{=},t_0,t_1),(R_{=},(f,t_0),(f,t_1))) \in \textrm{AxArray}\)である。
いかなる項配列\(t_0,t_1,t_2\)と引数\(2\)関数配列\(f\)に対しても、\((L_{\to},(R_{=},t_0,t_1),(R_{=},(f,t_0,t_2),(f,t_1,t_2))) \in \textrm{AxArray}\)である。
いかなる項配列\(t_0,t_1,t_2\)と引数\(2\)関数配列\(f\)に対しても、\((L_{\to},(R_{=},t_1,t_2),(R_{=},(f,t_0,t_1),(f,t_0,t_2))) \in \textrm{AxArray}\)である。
\((Q_{\forall \forall},x_0,x_1,(L_{\to},(Q_{\forall},x_2,(L_{\leftrightarrow},(R_{\in},x_2,x_0),(R_{\in},x_2,x_1))),(R_{=},x_0,x_1))) \in \textrm{AxArray}\)である。
\((Q_{\forall \forall},x_0,x_1,(L_{\leftrightarrow},(R_{\subset},x_0,x_1),(Q_{\forall},x_2,(L_{\to},(R_{\in},x_2,x_0),(R_{\in},x_2,x_1))))) \in \textrm{AxArray}\)である。
いかなる\(i,j \in \mathbb{N}\)と屋敷配列\(F\)に対しても、\((L_{\to},(Q_{\exists},x_i,(L_{\leftrightarrow},(R_{\in},x_j,x_i),F)),(\textrm{Cmp},x_j,F)) \in \textrm{AxArray}\)である。
いかなる\(i,j \in \mathbb{N}\)と屋敷配列\(F\)に対しても、\(i \neq j\)ならば\((Q_{\forall},x_j,(\textrm{Cmp},x_i,(L_{\wedge},(R_{\in},x_i,x_j),F))) \in \textrm{AxArray}\)である。
\((Q_{\forall \forall \forall},x_0,x_1,x_2,(L_{\leftrightarrow},(R_{\in},x_2,(f_{\{,\}},x_0,x_1)),(L_{\vee},(R_{=},x_2,x_0),(R_{=},x_2,x_1)))) \in \textrm{AxArray}\)である。
\((Q_{\forall},x_0,(R_{=},(f_{\{\}},x_0),(f_{\{,\}},x_0,x_0))) \in \textrm{AxArray}\)である。
\((Q_{\forall \forall},x_0,x_1,(R_{=},(f_{(,)},x_0,x_1),(f_{\{,\}},(f_{\{\}},x_0),(f_{\{,\}},x_0,x_1)))) \in \textrm{AxArray}\)である。
\((Q_{\forall \forall},x_0,x_1,(L_{\leftrightarrow},(R_{\in},x_1,(f_{\bigcup},x_0)),(Q_{\exists \in},x_2,x_0,(R_{\in},x_1,x_2)))) \in \textrm{AxArray}\)である。
\((Q_{\forall \forall},x_0,x_1,(R_{=},(f_{\cup},x_0,x_1),(f_{\bigcup},(f_{\{,\}},x_0,x_1)))) \in \textrm{AxArray}\)である。
\((Q_{\forall},x_0,(R_{=},(f_S,x_0),(f_{\cup},x_0,(f_{\{\}},x_0)))) \in \textrm{AxArray}\)である。
\((Q_{\forall \forall},x_0,x_1,(R_{=},(f_{\cap},x_0,x_1),(\varphi_{\{\mid\}},x_2,(L_{\wedge},(R_{\in},x_2,x_0),(R_{\in},x_2,x_1))))) \in \textrm{AxArray}\)である。
\((Q_{\forall \forall},x_0,x_1,(R_{=},(f_{\times},x_0,x_1),(\varphi_{\{\mid\}},x_2,(\textrm{Pair},x_3,x_0,x_4,x_1,x_2)))) \in \textrm{AxArray}\)である。
\((Q_{\forall \forall},x_0,x_1,(R_{=},(f_{\wedge},x_0,x_1),(\varphi_{\{\mid\}},x_2,(\textrm{Map},x_2,x_0,x_1,x_3,x_4)))) \in \textrm{AxArray}\)である。
\((Q_{\forall \forall},x_0,x_1,(L_{\wedge},(\textrm{Val},x_2,x_0,x_1),(\textrm{NaN},x_2,x_0,x_1))) \in \textrm{AxArray}\)である。
\((Q_{\forall \forall},x_0,x_1,(L_{\leftrightarrow},(R_{\in},x_1,(f_{\mathcal{P}},x_0)),(R_{\subset},x_1,x_0))) \in \textrm{AxArray}\)である。
いかなる\(i,j,k \in \mathbb{N}\)と屋敷配列\(F\)に対しても、\(i \neq j\)かつ\(j \neq k\)かつ\(k \neq i\)ならば\((L_{\to},(Q_{\forall \exists !},x_i,x_j,F),(Q_{\forall},x_k,(\textrm{Cmp},x_j,(Q_{\exists \in},x_i,x_k,F)))) \in \textrm{AxArray}\)である。
\((Q_{\forall},x_0,(R_{\notin},x_0,c_0)) \in \textrm{AxArray}\)である。
いかなる\(i \in \mathbb{N}\)に対しても、\((R_{=},c_{i+1},(f_S,c_i)) \in \textrm{AxArray}\)である。
\((R_{\in},c_0,c_{\mathbb{N}}) \in \textrm{AxArray}\)である。
\((Q_{\forall \in},x_0,c_{\mathbb{N}},(R_{\in},(f_S,x_0),c_{\mathbb{N}})) \in \textrm{AxArray}\)である。
\((Q_{\forall},x_0,(L_{\to},(L_{\wedge},(R_{\in},c_0,x_0),(Q_{\forall \in},x_1,x_0,(R_{\in},(f_S,x_1),x_0))),(R_{\subset},c_{\mathbb{N}},x_0))) \in \textrm{AxArray}\)である。
\((Q_{\forall},x_0,(R_{=},(f_{+},x_0,c_0),x_0)) \in \textrm{AxArray}\)である。
\((Q_{\forall \forall},x_0,x_1,(R_{=},(f_{+},x_0,(f_S,x_1)),(f_S,(f_{+},x_0,x_1)))) \in \textrm{AxArray}\)である。
\((Q_{\forall \in},x_0,c_{\mathbb{N}},(R_{=},(f_{-},x_0,x_0),c_0)) \in \textrm{AxArray}\)である。
\((Q_{\forall \in},x_0,c_{\mathbb{N}},(Q_{\forall \in},x_1,x_0,(R_{=},(f_{+},x_1,(f_{-},x_0,x_1)),x_0))) \in \textrm{AxArray}\)である。
\((Q_{\forall},x_0,(L_{\to},(R_{\neq},x_0,c_0),(Q_{\exists \in},x_1,x_0,(R_{=},(f_{\cap},x_0,x_1),c_0)))) \in \textrm{AxArray}\)である。
\((Q_{\forall},x_0,(L_{\to},(R_{\notin},c_0,x_0),(Q_{\exists \in},x_1,(f_{\wedge},(f_{\bigcup},x_0),x_0),(\textrm{Choi}(x_2,x_0,x_1))))) \in \textrm{AxArray}\)である。

\(\textrm{AxArray}\)の要素を「斧配列」と呼ぶ。

設計図配列[]

\(a \in \textrm{NestArray}^3\)に対し、\(a_0,a_1,a_2 \in \textrm{NestArray}\)をそれぞれ\(\textrm{Ax}(a), \textrm{Lmm}(a), \textrm{Vrf}(a)\)と置く。

\(a \in \textrm{NestArray}^3\)であって\(() \neq \textrm{Vrf}(a) \in \textrm{FormulaArray}^{< \omega}\)であるものに対し、\(\textrm{Result}(a) = \textrm{Last}(\textrm{Vrf}(a)) \in \textrm{FormulaArray}\)と定める。

部分集合\(\textrm{BuildArray} \subset \)を、以下を満たす最小の集合として定める：

いかなる\(a \in \textrm{NestArray}^3\)に対しても、\(a\)が以下を満たすならば、\(a \in \textrm{BuildArray}\)である：
1. \(\textrm{Ax}(a), \textrm{Vrf}(a) \in \textrm{FormulaArray}^{< \omega}\)かつ\(\textrm{Vrf}(a) \neq ()\)である^[12]。
2. \(\textrm{Lmm}(a) \in \textrm{BuildArray}^{< \omega}\)である。
3. \(\textrm{Lng}(\textrm{Vrf}(a))\)未満のいかなる\(i \in \mathbb{N}\)に対しても、以下のいずれかが成り立つ：
  1. \(\textrm{Vrf}(a)_i = \textrm{Ax}(a)_j\)を満たす\(j \in \mathbb{N}\)が存在する。
  2. \(\textrm{Vrf}(a)_i = F_{\perp}\)でありかつ、\(i\)未満の\(j_0,j_1 \in \mathbb{N}\)が存在して\(\textrm{Vrf}(a)_{j_0} = (L_{\neg},\textrm{Vrf}(a)_{j_1})\)を満たす。
  3. \(\textrm{Vrf}(a)_j = F_{\perp}\)を満たす\(i\)未満の\(j \in \mathbb{N}\)が存在する。
  4. \(\textrm{Vrf}(a)_i = (L_{\neg},F)\)を満たす屋敷配列\(F\)が存在し、かつ以下を満たす\(\textrm{Lng}(\textrm{Lmm}(a))\)未満の\(k \in \mathbb{N}\)が存在する：
    1. \(\textrm{Result}(\textrm{Lmm}(a)_k) = F_{\perp}\)である。
    2. \(\textrm{Ax}(\textrm{Lmm}(a)_k)\)のいかなる成分も、\(\textrm{Ax}(a)\)の成分か\(F\)と等しい。
  5. \(\textrm{Vrf}(a)_j = (L_{\neg},(L_{\neg},\textrm{Vrf}(a)_i))\)を満たす\(i\)未満の\(j \in \mathbb{N}\)が存在する。
  6. \(\textrm{Vrf}(a)_i = (L_{\wedge},\textrm{Vrf}(a)_{j_0},\textrm{Vrf}(a)_{j_1})\)を満たす\(i\)未満の\(j_0,j_1 \in \mathbb{N}\)が存在する。
  7. \(\textrm{Vrf}(a)_j = (L_{\wedge},\textrm{Vrf}(a)_i,F)\)を満たす\(i\)未満の\(j \in \mathbb{N}\)と屋敷配列\(F\)が存在する。
  8. \(\textrm{Vrf}(a)_j = (L_{\wedge},F,\textrm{Vrf}(a)_i)\)を満たす\(i\)未満の\(j \in \mathbb{N}\)と屋敷配列\(F\)が存在する。
  9. \(\textrm{Vrf}(a)_i = (L_{\vee},\textrm{Vrf}(a)_j,F)\)を満たす\(i\)未満の\(j \in \mathbb{N}\)と屋敷配列\(F\)が存在する。
  10. \(\textrm{Vrf}(a)_i = (L_{\vee},F,\textrm{Vrf}(a)_j)\)を満たす\(i\)未満の\(j \in \mathbb{N}\)と屋敷配列\(F\)が存在する。
  11. 以下を満たす\(i\)未満の\(j \in \mathbb{N}\)と\(k_0,k_1 \in \mathbb{N}\)と屋敷配列\(F_0,F_1\)が存在する：
    1. \(\textrm{Vrf}(a)_j = (L_{\vee},F_0,F_1)\)である。
    2. \(\textrm{Ax}(\textrm{Lmm}(a)_{k_0})\)のいかなる成分も\(\textrm{Ax}(a)\)のいずれかの成分か\(F_0\)と等しい。
    3. \(\textrm{Ax}(\textrm{Lmm}(a)_{k_1})\)のいかなる成分も\(\textrm{Ax}(a)\)のいずれかの成分か\(F_1\)と等しい。
    4. \(\textrm{Vrf}(a)_i = \textrm{Result}(\textrm{Lmm}(a)_{k_0}) = \textrm{Result}(\textrm{Lmm}(a)_{k_1})\)である。
  12. 以下を満たす\(\textrm{Lng}(\textrm{Lmm}(a))\)未満の\(k \in \mathbb{N}\)と屋敷配列\(F\)が存在する：
    1. \(\textrm{Vrf}(a)_i = (L_{\to},F,\textrm{Result}(\textrm{Lmm}(a)_k))\)である。
    2. \(\textrm{Ax}(\textrm{Lmm}(a)_k)\)のいかなる成分も\(\textrm{Ax}(a)\)のいずれかの成分か\(F\)と等しい。
  13. \(\textrm{Vrf}(a)_{j_0} = (L_{\to},\textrm{Vrf}(a)_{j_1},\textrm{Vrf}(a)_i)\)を満たす\(i\)未満の\(j_0,j_1 \in \mathbb{N}\)が存在する。
  14. 以下を満たす\(h_0,h_1 \in \mathbb{N}\)と\(i\)未満の\(j \in \mathbb{N}\)と\([x_{h_1}/x_{h_0}]\)可能屋敷配列\(F\)が存在する：
    1. \(\textrm{Vrf}(a)_i = (Q_{\forall},x_{h_0},F)\)である。
    2. \(\textrm{Vrf}(a)_j = F[x_{h_1}/x_{h_0}]\)を満たす。
    3. \(\textrm{Ax}(a) \notin \textrm{Occur}_{h_1}\)かつ\(F \notin \textrm{Occur}_{h_1}\)である。
  15. 以下を満たす\(h \in \mathbb{N}\)と\(i\)未満の\(j \in \mathbb{N}\)と項配列\(t\)と\([t/x_h]\)可能屋敷配列\(F\)が存在する：
    1. \(\textrm{Vrf}(a)_i = F[t/x_h]\)である。
    2. \(\textrm{Vrf}(a)_j = (Q_{\forall},x_h,F)\)を満たす。
  16. 以下を満たす\(h \in \mathbb{N}\)と\(i\)未満の\(j \in \mathbb{N}\)と項配列\(t\)と\([t/x_h]\)可能屋敷配列\(F\)が存在する：
    1. \(\textrm{Vrf}(a)_i = (Q_{\exists},x_h,F)\)である。
    2. \(\textrm{Vrf}(a)_j = F[t/x_h]\)を満たす。
  17. 以下を満たす\(h_0,h_1 \in \mathbb{N}\)と\(\textrm{Lng}(\textrm{Lmm}(a))\)未満の\(k \in \mathbb{N}\)と\(i\)未満の\(j \in \mathbb{N}\)と\([x_{h_1}/x_{h_0}]\)可能屋敷配列\(F\)と項配列\(t\)が存在する：
    1. \(\textrm{Result}(\textrm{Lmm}(a)_k) = \textrm{Vrf}(a)_i\)である。
    2. \(F[x_{h_1}/x_{h_0}]\)が\(\textrm{Ax}(\textrm{Lmm}(a)_k)\)のいずれかの成分と等しい。
    3. \(\textrm{Ax}(a) \notin \textrm{Occur}_{h_1}\)かつ\(F \notin \textrm{Occur}_{h_1}\)かつ\(\textrm{Vrf}(a)_i \notin \textrm{Occur}_{h_1}\)である。
    4. \(\textrm{Vrf}(a)_j = (Q_{\exists},x_{h_0},F)\)である。
  18. 以下を満たす\(h_0,h_1 \in \mathbb{N}\)と\(i\)未満の\(j \in \mathbb{N}\)と\([x_{h_1}/x_{h_0}]\)可能屋敷配列\(F\)が存在する：
    1. \(\textrm{Vrf}(a)_i = (Q_!,x_{h_0},F)\)である。
    2. \(h_0 \neq h_1\)かつ\(F \notin \textrm{Occur}_{h_1}\)である。
    3. \(\textrm{Vrf}(a)_j = (Q_{\forall},x_{h_0},(Q_{\forall},x_{h_1},(L_{\to},(L_{\wedge},F,F[x_{h_1}/x_{h_0}]),(R_{=},x_{h_0},x_{h_1}))))\)である。
  19. 以下を満たす\(h \in \mathbb{N}\)と\(i\)未満の\(j_0,j_1 \in \mathbb{N}\)と項配列\(t_0,t_1\)と\([t_0/x_h]\)可能かつ\([t_1/x_h]\)可能な屋敷配列\(F\)が存在する：
    1. \(\textrm{Vrf}(a)_i = (R_{=},t_0,t_1)\)である。
    2. \(\textrm{Vrf}(a)_{j_0} = (Q_!,x_{h_0},F)\)である。
    3. \(\textrm{Vrf}(a)_{j_1} = (L_{\wedge},F[t_0/x_h],F[t_1/x_h])\)である。

\(\textrm{BuildArray}\)の要素を「設計図配列」と呼ぶ。また設計図配列\(a\)が「斧のみを用いる」とは、\(\textrm{Ax}(a)\)の各成分が斧配列であるということである。

チューリングマシンの形式化[]

チューリング完全な計算モデルであるコード配列の全域性の証明可能性を形式化し、それにより可証整礎な再帰的順序を対角化する。もちろん、ここでも形式言語や公理といった形式論理の用語は一切用いずに定式化する。

Sepの形式化[]

項配列\(A_0,A_1,A_2,A_3\)に対し、以下のように略記を定める： \begin{eqnarray*} (R_{\textrm{Sep}},A_0,A_1,A_2,A_3) & = & (L_{\wedge \wedge},(R_{\textrm{Sep}}^{1},A_0,A_1,A_3),(R_{\textrm{Sep}}^{2},A_0,A_1,A_2,A_3),(R_{\textrm{Sep}}^{3},A_0,A_1,A_3)) \\ (R_{\textrm{Sep}}^{1},A_0,A_1,A_3) & = & (Q_{\forall \in},x_{100},A_1,(R_{=},(f_{\bullet ()},A_3,x_{100}),(f_{\bullet ()},A_0,x_{100}))) \\ (R_{\textrm{Sep}}^{2},A_0,A_1,A_2,A_3) & = & (L_{\wedge},(R_{\textrm{Sep}}^{20},A_1,A_2,A_3),(R_{\textrm{Sep}}^{21},A_0,A_1,A_2,A_3)) \\ (R_{\textrm{Sep}}^{20},A_1,A_2,A_3) & = & (R_{=},(f_{\bullet ()},A_3,A_1),A_2) \\ (R_{\textrm{Sep}}^{21},A_0,A_1,A_2,A_3) & = & (R_{=},(f_{\bullet ()},A_3,(f_S,A_1)),(f_{-},(f_{\bullet ()},A_0,A_1),(f_S,A_2)))) \\ (R_{\textrm{Sep}}^{3},A_0,A_1,A_3) & = & (Q_{\forall \in},x_{100},c_{\mathbb{N}},(L_{\to},(R_{\in},A_1,x_{100}),(R_{\textrm{Sep}}^{30},A_0,A_3))) \\ (R_{\textrm{Sep}}^{30},A_0,A_3) & = & (R_{=},(f_{\bullet ()},A_3,(f_S,x_{100})),(f_{\bullet ()},A_0,x_{100})) \end{eqnarray*}

\((R_{\textrm{Sep}},A_0,A_1,A_2,A_3)\)は\(\textrm{Sep}(M,p,m)\)を形式化したものである。\((R_{\textrm{Sep}},A_0,A_1,A_2,A_3)\)に出現する各項配列は\(\textrm{Sep}(M,p,m)\)の定義における項に以下のように対応する：

項配列	項
\(c_{\mathbb{N}}\)	\(\mathbb{N}\)
\(x_{100}\)	\(M\)の添字
\(A_0\)	\(M\)
\(A_1\)	\(p\)
\(A_2\)	\(m\)
\(A_3\)	\(\textrm{Sep}(M,p,m)\)

Cmbの形式化[]

項配列\(A_0,A_1,A_2\)に対し、以下のように略記を定める： \begin{eqnarray*} (R_{\textrm{Cmb}},A_0,A_1,A_2) & = & (L_{\wedge \wedge},(R_{\textrm{Sep}}^{1},A_0,A_1,A_2),(R_{\textrm{Cmb}}^{0},A_0,A_1,A_2),(R_{\textrm{Cmb}}^{1},A_0,A_1,A_2)) \\ (R_{\textrm{Cmb}}^{0},A_0,A_1,A_2) & = & (\textrm{R}_{=},(f_{\bullet ()},A_2,A_1),(f_{+},(f_S,(f_{\bullet ()},A_0,A_1)),(f_{\bullet ()},A_0,(f_S,A_1)))) \\ (R_{\textrm{Cmb}}^{1},A_0,A_1,A_2) & = & (Q_{\forall \in},x_{100},c_{\mathbb{N}},(L_{\to},(R_{\in},A_1,x_{100}),(R_{\textrm{Sep}}^{30},A_2,A_0))) \end{eqnarray*}

\((R_{\textrm{Cmb}},A_0,A_1,A_2)\)は\(\textrm{Cmb}(M,p)\)を形式化したものである。\((R_{\textrm{Cmb}},A_0,A_1,A_2)\)に出現する各項配列は\(\textrm{Cmb}(M,p)\)の定義における項に以下のように対応する：

項配列	項
\(c_{\mathbb{N}}\)	\(\mathbb{N}\)
\(x_{100}\)	\(M\)の添字
\(A_0\)	\(M\)
\(A_1\)	\(p\)
\(A_2\)	\(\textrm{Cmb}(M,p)\)

Appの形式化[]

項配列\(A_0,A_1,A_2\)に対し、以下のように略記を定める： \begin{eqnarray*} (f_{\bullet (,)},A_0,A_1,A_2) & = & (f_{\bullet ()},(f_{\bullet ()},A_0,A_2),A_1) \\ (f_{\wedge \wedge},A_0,A_1,A_2) & = & (f_{\wedge},(f_{\wedge},A_0,A_1),A_2) \end{eqnarray*}

コード配列\(\Theta\)と\(i \in \mathbb{N}\)に対し、以下のように略記を定める^[13]： \begin{eqnarray*} F_{\textrm{App},\Theta} & = & (Q_{\forall \forall \forall},x_4,x_5,x_6,(L_{\to},F_{\textrm{App},\Theta}^{1},F_{\textrm{App},\Theta}^{2})) \\ F_{\textrm{App},\Theta}^{1} & = & (L_{\wedge \wedge},F_{\textrm{App},\Theta}^{10},F_{\textrm{App},\Theta}^{11},F_{\textrm{App},\Theta}^{12}) \\ F_{\textrm{App},\Theta}^{10} & = & (R_{=},x_4,(f_{\bullet ()},x_0,c_0)) \\ F_{\textrm{App},\Theta}^{11} & = & (R_{=},x_5,(f_{\bullet ()},x_0,c_1)) \\ F_{\textrm{App},\Theta}^{12} & = & (R_{=},x_6,(f_{\bullet ()},x_0,c_2)) \\ F_{\textrm{App},\Theta}^{2} & = & (L_{\wedge},F_{\textrm{App},\Theta}^{20},F_{\textrm{App},\Theta}^{21}) \\ F_{\textrm{App},\Theta}^{20} & = & (Q_{\forall \forall},x_7,x_8,(L_{\to},F_{\textrm{App},\Theta}^{200},F_{\textrm{App},\Theta}^{201})) \\ F_{\textrm{App},\Theta}^{200} & = & (L_{\wedge},F_{\textrm{App},\Theta}^{200,\textrm{Lng}(\Theta)},(R_{=},x_8,(f_{\bullet ()},x_1,x_5))) \\ F_{\textrm{App},\Theta}^{200,0} & = & F_{\perp} \\ F_{\textrm{App},\Theta}^{200,i+1} & = & (L_{\vee},F_{\textrm{App},\Theta}^{200,i},F_{\textrm{App},\Theta}^{2000,i}) \\ F_{\textrm{App},\Theta}^{2000,i} & = & (L_{\wedge},F_{\textrm{App},\Theta}^{20000,i},F_{\textrm{App},\Theta}^{20001,i}) \\ F_{\textrm{App},\Theta}^{20000,i} & = & (R_{=},x_4,c_i) \\ F_{\textrm{App},\Theta}^{20001,i} & = & (L_{\wedge \wedge},F_{\textrm{App},\Theta}^{200010,i},F_{\textrm{App},\Theta}^{200011,i},F_{\textrm{App},\Theta}^{200012,i}) \\ F_{\textrm{App},\Theta}^{200010,i} & =& (L_{\wedge},F_{\textrm{App},\Theta}^{2000100,i}F_{\textrm{App},\Theta}^{2000101,i}) \\ F_{\textrm{App},\Theta}^{2000100,i} & = & (R_{=},(f_{\bullet (,)},x_7,c_0,c_0),c_{[\Theta_i]_{0,0}}) \\ F_{\textrm{App},\Theta}^{2000101,i} & = & (R_{=},(f_{\bullet (,)},x_7,c_0,c_1),c_{[\Theta_i]_{0,1}}) \\ F_{\textrm{App},\Theta}^{200011,i} & =& (L_{\wedge},F_{\textrm{App},\Theta}^{2000110,i}F_{\textrm{App},\Theta}^{2000111,i}) \\ F_{\textrm{App},\Theta}^{2000110,i} & = & (R_{=},(f_{\bullet (,)},x_7,c_1,c_0),c_{[\Theta_i]_{1,0}}) \\ F_{\textrm{App},\Theta}^{2000111,i} & = & (R_{=},(f_{\bullet (,)},x_7,c_1,c_1),c_{[\Theta_i]_{1,1}}) \\ F_{\textrm{App},\Theta}^{200012,i} & =& (L_{\wedge},F_{\textrm{App},\Theta}^{2000120,i}F_{\textrm{App},\Theta}^{2000121,i}) \\ F_{\textrm{App},\Theta}^{2000120,i} & = & (R_{=},(f_{\bullet (,)},x_7,c_2,c_0),c_{[\Theta_i]_{2,0}}) \\ F_{\textrm{App},\Theta}^{2000121,i} & = & (R_{=},(f_{\bullet (,)},x_7,c_2,c_1),c_{[\Theta_i]_{2,1}}) \end{eqnarray*} \begin{eqnarray*} F_{\textrm{App},\Theta}^{201} & = & (Q_{\forall},x_9,(L_{\to},F_{\textrm{App},\Theta}^{2010},F_{\textrm{App},\Theta}^{2011})) \\ F_{\textrm{App},\Theta}^{2010} & = & (L_{\wedge},F_{\textrm{App},\Theta}^{20100},F_{\textrm{App},\Theta}^{20101}) \\ F_{\textrm{App},\Theta}^{20100} & = & (L_{\to},(R_{\in},x_6,x_8),(R_{=},x_9,c_0)) \\ F_{\textrm{App},\Theta}^{20101} & = & (L_{\to},(R_{\notin},x_6,x_8),(R_{=},x_9,c_1))) \\ F_{\textrm{App},\Theta}^{2011} & = & (Q_{\forall \forall},x_{10},x_{11},(L_{\to},F_{\textrm{App},\Theta}^{20110},F_{\textrm{App},\Theta}^{20111})) \\ F_{\textrm{App},\Theta}^{20110} & = & (L_{\wedge},F_{\textrm{App},\Theta}^{201101},F_{\textrm{App},\Theta}^{201101}) \\ F_{\textrm{App},\Theta}^{201100} & = & (R_{=},x_{10},(f_{\bullet (,)},x_7,c_1,x_9)) \\ F_{\textrm{App},\Theta}^{201101} & = & (R_{=},x_{11},(f_{\bullet (,)},x_7,c_2,x_9)) \\ F_{\textrm{App},\Theta}^{20111} & = & (Q_{\forall},x_{12},(L_{\to},F_{\textrm{App},\Theta}^{201110},F_{\textrm{App},\Theta}^{201111})) \\ F_{\textrm{App},\Theta}^{201110} & = & (L_{\wedge},F_{\textrm{App},\Theta}^{2011100},F_{\textrm{App},\Theta}^{2011101}) \\ F_{\textrm{App},\Theta}^{2011100} & = & (L_{\to},(R_{=},x_{10},c_0),F_{\textrm{App},\Theta}^{20111000}) \\ F_{\textrm{App},\Theta}^{20111000} & = & (L_{\wedge},F_{\textrm{App},\Theta}^{201110000},F_{\textrm{App},\Theta}^{201110001}) \\ F_{\textrm{App},\Theta}^{201110000} & = & (L_{\to},(R_{\neq},x_4,c_0),F_{\textrm{App},\Theta}^{2011100000}) \\ F_{\textrm{App},\Theta}^{2011100000} & = & (L_{\wedge},F_{\textrm{App},\Theta}^{20111000000},F_{\textrm{App},\Theta}^{20111000001}) \\ F_{\textrm{App},\Theta}^{20111000000} & = & (L_{\to},(R_{=},x_6,c_0),(R_{=},(f_S,x_{12}),x_5)) \\ F_{\textrm{App},\Theta}^{20111000001} & = & (L_{\to},(R_{\neq},x_6,c_0),(R_{=},x_{12},x_5))) \\ F_{\textrm{App},\Theta}^{201110001} & = & (L_{\to},(R_{=},x_4,c_0),(R_{=},x_{12},x_5)) \\ F_{\textrm{App},\Theta}^{2011101} & = & (L_{\to},(R_{\neq},x_{10},c_0),F_{\textrm{App},\Theta}^{20111010}) \\ F_{\textrm{App},\Theta}^{20111010} & = & (L_{\wedge},F_{\textrm{App},\Theta}^{201110100},F_{\textrm{App},\Theta}^{201110101}) \\ F_{\textrm{App},\Theta}^{201110100} & = & (L_{\to},(R_{\neq},x_{11},c_0),(R_{=},x_{12},x_5)) \\ F_{\textrm{App},\Theta}^{201110101} & = & (L_{\to},(R_{=},x_{11},c_0),(R_{=},x_{12},(f_S,x_5))) \end{eqnarray*} \begin{eqnarray*} F_{\textrm{App},\Theta}^{201111} & = & (Q_{\forall},x_{13},(L_{\to},F_{\textrm{App},\Theta}^{2011110},F_{\textrm{App},\Theta}^{2011111})) \\ F_{\textrm{App},\Theta}^{2011110} & = & (L_{\wedge},F_{\textrm{App},\Theta}^{20111100},F_{\textrm{App},\Theta}^{20111101}) \\ F_{\textrm{App},\Theta}^{20111100} & = & (L_{\to},(R_{=},x_{10},c_0),F_{\textrm{App},\Theta}^{201111000}) \\ F_{\textrm{App},\Theta}^{201111000} & = & (L_{\wedge},F_{\textrm{App},\Theta}^{2011110000},F_{\textrm{App},\Theta}^{2011110001}) \\ F_{\textrm{App},\Theta}^{2011110000} & = & (L_{\to},(R_{\neq},x_6,c_0),(R_{=},(f_S,x_{13}),x_6)) \\ F_{\textrm{App},\Theta}^{2011110001} & = & (L_{\wedge},F_{\textrm{App},\Theta}^{20111100010},F_{\textrm{App},\Theta}^{20111100011}) \\ F_{\textrm{App},\Theta}^{20111100010} & = & (L_{\to},(R_{\neq},x_5,c_0),(R_{=},x_{13},(f_{\bullet ()},x_1,x_{12}))) \\ F_{\textrm{App},\Theta}^{20111100011} & = & (L_{\to},(R_{=},x_5,c_0),(R_{=},x_{13},x_6)) \\ F_{\textrm{App},\Theta}^{20111101} & = & (L_{\to},(R_{\neq},x_{10},c_0),F_{\textrm{App},\Theta}^{201111010}) \\ F_{\textrm{App},\Theta}^{201111010} & = & (L_{\wedge},F_{\textrm{App},\Theta}^{2011110100},F_{\textrm{App},\Theta}^{2011110101}) \\ F_{\textrm{App},\Theta}^{2011110100} & = & (L_{\to},(R_{=},x_{11},c_0),(R_{=},x_{13},c_0)) \\ F_{\textrm{App},\Theta}^{2011110101} & = & (L_{\to},(R_{\neq},x_{11},c_0),(R_{=},x_{13},(f_S,x_6))) \\ F_{\textrm{App},\Theta}^{2011111} & = & (L_{\wedge},F_{\textrm{App},\Theta}^{20111110},F_{\textrm{App},\Theta}^{20111111}) \\ F_{\textrm{App},\Theta}^{20111110} & = & (L_{\wedge \wedge},F_{\textrm{App},\Theta}^{201111100},F_{\textrm{App},\Theta}^{201111101},F_{\textrm{App},\Theta}^{201111102}) \\ F_{\textrm{App},\Theta}^{201111100} & = & (R_{=},(f_{\bullet ()},x_2,c_0),(f_{\bullet (,)},x_7,c_0,x_9)) \\ F_{\textrm{App},\Theta}^{201111101} & = & (R_{=},(f_{\bullet ()},x_2,c_1),x_{12}) \\ F_{\textrm{App},\Theta}^{201111102} & = & (R_{=},(f_{\bullet ()},x_2,c_2),x_{13}) \\ F_{\textrm{App},\Theta}^{20111111} & = & (L_{\wedge},F_{\textrm{App},\Theta}^{201111110},F_{\textrm{App},\Theta}^{201111111}) \\ F_{\textrm{App},\Theta}^{201111110} & = & (L_{\to},(R_{\in},x_6,x_8),F_{\textrm{App},\Theta}^{2011111100}) \\ F_{\textrm{App},\Theta}^{2011111100} & = & (L_{\wedge},F_{\textrm{App},\Theta}^{20111111000},F_{\textrm{App},\Theta}^{20111111001}) \\ F_{\textrm{App},\Theta}^{20111111000} & = & (L_{\to},(R_{=},x_{11},c_0),(R_{\textrm{Sep}},x_1,x_5,x_6,x_3)) \\ F_{\textrm{App},\Theta}^{20111111001} & = & (L_{\to},(R_{\neq},x_{11},c_0),(R_{=},x_3,x_1)) \\ F_{\textrm{App},\Theta}^{201111111} & = & (L_{\to},(R_{\notin},x_6,x_8),F_{\textrm{App},\Theta}^{2011111110}) \\ F_{\textrm{App},\Theta}^{2011111110} & = & (L_{\wedge},F_{\textrm{App},\Theta}^{20111111100},F_{\textrm{App},\Theta}^{20111111101}) \\ F_{\textrm{App},\Theta}^{20111111100} & = & (L_{\to},(R_{=},x_{11},c_0),(R_{=},x_3,x_1)) \\ F_{\textrm{App},\Theta}^{20111111101} & = & (L_{\to},(R_{\neq},x_{11},c_0),(R_{\textrm{Cmb}},x_1,x_5,x_3)) \\ F_{\textrm{App},\Theta}^{21} & = & (L_{\to},F_{\textrm{App},\Theta}^{210},F_{\textrm{App},\Theta}^{211}) \\ F_{\textrm{App},\Theta}^{210} & = & (L_{\neg},(Q_{\exists \exists},x_7,x_8,F_{\textrm{App},\Theta}^{200})) \\ F_{\textrm{App},\Theta}^{211} & = & (L_{\wedge},(R_{=},x_2,x_0),(R_{=},x_3,x_1)) \end{eqnarray*}

\(F_{\textrm{App},\Theta}\)は\((M',P') = \textrm{App}_{\Theta}(M,P)\)を形式化したものである。\(F_{\textrm{App},\Theta}\)に出現する各項配列は\(\textrm{App}_{\Theta}(M,P)\)の定義における項に以下のように対応する：

項配列	項
\(c_i\)	\(i\)
\(c_{\mathbb{N}}\)	\(\mathbb{N}\)
\(x_0\)	\(P\)
\(x_1\)	\(M\)
\(x_2\)	\(P'\)
\(x_3\)	\(M'\)
\(x_4\)	\(P_0\)
\(x_5\)	\(P_1\)
\(x_6\)	\(P_2\)
\(x_7\)	\(C = \Theta_{P_0}\)
\(x_8\)	\(x = M_{P_1}\)
\(x_9\)	\(j\)
\(x_10\)	\(C_{1,j}\)
\(x_{11}\)	\(C_{2,j}\)
\(x_{12}\)	\(p\)
\(x_{13}\)	\(m\)

特筆すべきは\(x_7\)と\(C = \Theta_{P_0}\)の対応であり、\(\Theta\)の長さの有限性により\(F_{\textrm{App},\Theta}^{200,i}\)の再帰的定義を用いてメタなコード行列\(C\)の情報を項配列に反映させている。

停止性の形式化[]

コード配列\(\Theta\)に対し、以下のように略記を定める： \begin{eqnarray*} F_{\textrm{Halt},\Theta} & = & (Q_{\exists \in},x_{16},(f_{\wedge \wedge},c_{\mathbb{N}},c_3,x_{14}),F_{\textrm{Halt},\Theta}^{1}) \\ F_{\textrm{Halt},\Theta}^{1} & = & (Q_{\forall},x_{17},(L_{\to},F_{\textrm{Halt},\Theta}^{10},F_{\textrm{Halt},\Theta}^{11})) \\ F_{\textrm{Halt},\Theta}^{10} & = & (R_{=},x_{17},(\varphi_{\{\mid\}},x_{18},F_{\textrm{Halt},\Theta}^{100})) \\ F_{\textrm{Halt},\Theta}^{100} & = & (Q_{\exists \in},x_{19},c_{\mathbb{N}},(R_{\in},x_{18},(f_{\wedge},c_{\mathbb{N}},x_{19}))) \\ F_{\textrm{Halt},\Theta}^{11} & = & (Q_{\exists \in},x_{20},(f_{\wedge},x_{17},x_{14}),F_{\textrm{Halt},\Theta}^{110}) \\ F_{\textrm{Halt},\Theta}^{110} & = & (L_{\wedge \wedge},F_{\textrm{Halt},\Theta}^{1100},F_{\textrm{Halt},\Theta}^{1101},F_{\textrm{Halt},\Theta}^{1102}) \\ F_{\textrm{Halt},\Theta}^{1100} & = & (L_{\wedge},F_{\textrm{Halt},\Theta}^{11000},(R_{=},(f_{\bullet ()},x_{20},c_0),x_1)) \\ F_{\textrm{Halt},\Theta}^{11000} & = & (L_{\wedge \wedge},F_{\textrm{Halt},\Theta}^{110000},F_{\textrm{Halt},\Theta}^{110001},F_{\textrm{Halt},\Theta}^{110002}) \\ F_{\textrm{Halt},\Theta}^{110000} & = & (R_{=},(f_{\bullet (,)},x_{16},c_0,c_0),c_0) \\ F_{\textrm{Halt},\Theta}^{110001} & = & (R_{=},(f_{\bullet (,)},x_{16},c_1,c_0),c_0) \\ F_{\textrm{Halt},\Theta}^{110002} & = & (R_{=},(f_{\bullet (,)},x_{16},c_2,c_0),c_0) \\ F_{\textrm{Halt},\Theta}^{1101} & = & (Q_{\forall \forall},x_{21},x_{22},(Q_{\forall \forall},x_{23},x_{24},(F_{\textrm{Halt},\Theta}^{11010}))) \\ F_{\textrm{Halt},\Theta}^{11010} & = & (L_{\to},F_{\textrm{Halt},\Theta}^{110100},F_{\textrm{Halt},\Theta}^{110101}) \\ F_{\textrm{Halt},\Theta}^{110100} & = & (Q_{\exists \in},x_{25},x_{14},F_{\textrm{Halt},\Theta}^{1101000}) \\ F_{\textrm{Halt},\Theta}^{1101000} & = & (L_{\wedge},F_{\textrm{Halt},\Theta}^{11010000},F_{\textrm{Halt},\Theta}^{11010001}) \\ F_{\textrm{Halt},\Theta}^{11010000} & = & (L_{\wedge},(R_{=},x_{21},(f_{\bullet ()},x_{16},x_{25})),(R_{=},x_{22},(f_{\bullet ()},x_{20},x_{25}))) \\ F_{\textrm{Halt},\Theta}^{11010001} & = & (L_{\wedge},(R_{=},x_{23},(f_{\bullet ()},x_{16},(f_S,x_{25}))),(R_{=},x_{24},(f_{\bullet ()},x_{20},(f_S,x_{25})))) \\ F_{\textrm{Halt},\Theta}^{110101} & = & F_{\textrm{App},\Theta}[x_{21}/x_0][x_{22}/x_1][x_{23}/x_2][x_{24}/x_3] \\ F_{\textrm{Halt},\Theta}^{1102} & = & (Q_{\exists \exists},x_{21},x_{22},(Q_{\exists},x_{23},(F_{\textrm{Halt},\Theta}^{11020}))) \\　 F_{\textrm{Halt},\Theta}^{11020} & = & (Q_{\exists \in},x_{25},x_{14},(L_{\wedge \wedge},F_{\textrm{Halt},\Theta}^{1101000}[x_{15}/x_{24}],(R_{=},x_{21},x_{23}),(R_{=},x_{22},x_{15}))) \end{eqnarray*}

\(F_{\textrm{Halt},\Theta}\)はメモリ数列\(M\)を入力とする\(\Theta\)のステップ\(n\)未満での停止性を形式化したものである。\(F_{\textrm{Halt},\Theta}\)に出現する各項配列は\(M\)を入力とする\(\Theta\)のステップ\(n\)未満での停止性の定義における項に以下のように対応する：

項配列	項
\(c_i\)	\(i\)
\(c_{\mathbb{N}}\)	\(\mathbb{N}\)
\(x_1\)	\(M\)
\(x_{14}\)	ステップ数\(n\)
\(x_{15}\)	メモリ配列\(\textrm{App}_{\Theta}^{n-1}((0,0,0),M)_1\)
\(x_{16}\)	ポインタベクトルの配列\(\mathbb{P} = (\textrm{App}_{\Theta}^i((0,0,0),M)_0)_{i=0}^{n-1}\)
\(x_{17}\)	メモリ配列全体の集合\(\mathbb{N}^{< \omega}\)
\(x_{18}\)	メモリ配列を表す変数\(N\)
\(x_{19}\)	\(\textrm{Lng}(N)\)
\(x_{20}\)	メモリ配列の配列\(\mathbb{M} = (\textrm{App}^k((0,0,0),M)_1)_{k=0}^{n-1}\)
\(x_{21}\)	\(\mathbb{P}\)のある成分\(\textrm{App}^k((0,0,0),M)_0\)
\(x_{22}\)	\(\mathbb{M}\)のある成分\(\textrm{App}^k((0,0,0),M)_1\)
\(x_{23}\)	\(\mathbb{P}\)の成分\(\textrm{App}^{k+1}((0,0,0),M)_0\)
\(x_{24}\)	\(\mathbb{M}\)の成分\(\textrm{App}^{k+1}((0,0,0),M)_1\)
\(x_{25}\)	\(n\)未満のステップ数\(k\)

Outputの形式化[]

項配列\(A_0,A_1\)に対し、以下のように略記を導入する： \begin{eqnarray*} (R_{\textrm{Sum}},A_0,A_1) & = & (Q_{\forall \in},x_{19},c_{\mathbb{N}},(L_{\to},(R_{\in},A_0,(f_{\wedge},c_{\mathbb{N}},x_{19}))),(R_{\textrm{Sum}}^{1},A_0,A_1)) \\ (R_{\textrm{Sum}}^{1},A_0,A_1) & = & (Q_{\exists \in},x_{18},(f_{\wedge},c_{\mathbb{N}},(f_S,x_{19})),(R_{\textrm{Sum}}^{10},A_0,A_1)) \\ (R_{\textrm{Sum}}^{10},A_0,A_1) & = & (L_{\wedge \wedge},(R_{\textrm{Sum}}^{100},A_0),(R_{\textrm{Sum}}^{101},A_0),(R_{\textrm{Sum}}^{102},A_1)) \\ (R_{\textrm{Sum}}^{100},A_0) & = & (R_{=},(f_{\bullet ()},x_{18},c_0),0) \\ (R_{\textrm{Sum}}^{101},A_0) & = & (Q_{\forall \in},x_{100},x_{19},(R_{=},(f_{\bullet ()},x_{18},(f_S,x_{100})),(f_{+},(f_{\bullet ()},x_{18},x_{100}),(f_{\bullet ()},A_0,x_{100}))) \\ (R_{\textrm{Sum}}^{102},A_1) & = & (R_{=},A_1,(f_{\bullet ()},x_{18},x_{19})) \end{eqnarray*}

コード配列\(\Theta\)に対し、以下のように略記を定める： \begin{eqnarray*} F_{\textrm{Output},\Theta} & = & (Q_{\exists \in},x_{14},c_{\mathbb{N}},(Q_{\exists},x_{15},F_{\textrm{Output},\Theta}^{1})) \\ F_{\textrm{Output},\Theta}^{1} & = & (L_{\wedge \wedge},F_{\textrm{Halt},\Theta},F_{\textrm{Output},\Theta}^{10},F_{\textrm{Output},\Theta}^{11}) \\ F_{\textrm{Output},\Theta}^{10} & = & (Q_{\forall \in},x_{27},x_{14},(L_{\neg},F_{\textrm{Halt},\Theta}[x_{27}/x_{14}])) \\ F_{\textrm{Output},\Theta}^{11} & = & (R_{\textrm{Sum}},x_{15},x_{26}) \\ \end{eqnarray*}

\(F_{\textrm{Output},\Theta}\)は\(\textrm{Output}_{\Theta}(M)\)を形式化したものである。\(F_{\textrm{Output},\Theta}\)に出現する各項配列は\(\textrm{Output}_{\Theta}(M)\)の定義における項に以下のように対応する：

項配列	項
\(c_{\mathbb{N}}\)	\(\mathbb{N}\)
\(x_{14}\)	停止ステップ数\(n\)
\(x_{15}\)	メモリ配列\(\textrm{App}_{\Theta}^{n-1}((0,0,0),M)_1\)
\(x_{26}\)	出力\(\textrm{Output}_{\Theta}(M)\)
\(x_{27}\)	\(n\)未満のステップ数\(k\)

再帰的整列順序の形式化[]

項配列\(A_0, A_1\)に対し、以下のように略記を定める： \begin{eqnarray*} (F_{\textrm{Pair}},A_0,A_1) & = & (L_{\wedge},(R_{\in},x_1,(f_{\wedge},c_{\mathbb{N}},c_2)),(F_{\textrm{Pair}}^{1},A_0,A_1)) \\ (F_{\textrm{Pair}}^{1},A_0,A_1) & = & (L_{\wedge},(R_{=},(f_{\bullet ()},x_1,c_0),A_0),(R_{=},(f_{\bullet ()},x_1,c_1),A_1)) \end{eqnarray*}

コード配列\(\Theta\)と項配列\(A_0,A_1,A_2\)に対し、以下のように略記を定める： \begin{eqnarray*} (F_{\textrm{Val},\Theta},A_0,A_1,A_2) = (Q_{\forall},x_1,(L_{\to},(F_{\textrm{Pair}},A_0,A_1),F_{\textrm{Output},\Theta}[A_2/x_{26}])) \end{eqnarray*}

コード配列\(\Theta\)に対し、以下のように略記を定める： \begin{eqnarray*} F_{\textrm{RR},\Theta} = (Q_{\forall \in},x_1,(f_{\wedge},c_{\mathbb{N}},c_2),(L_{\vee},F_{\textrm{Output},\Theta}[c_0/x_{26}],F_{\textrm{Output},\Theta}[c_1/x_{26}])) \end{eqnarray*} \begin{eqnarray*} F_{\textrm{RO},\Theta} & = & (L_{\wedge},F_{\textrm{RR},\Theta},F_{\textrm{RO},\Theta}^{1}) \\ F_{\textrm{RO},\Theta}^{1} & = & (L_{\wedge \wedge},F_{\textrm{RO},\Theta}^{10},F_{\textrm{RO},\Theta}^{11},F_{\textrm{RO},\Theta}^{12}) \\ F_{\textrm{RO},\Theta}^{10} & = & (Q_{\forall \in},x_{28},c_{\mathbb{N}},(F_{\textrm{Val},\Theta},x_{28},x_{28},c_1)) \\ F_{\textrm{RO},\Theta}^{11} & = & (Q_{\forall \forall \in},x_{28},x_{29},c_{\mathbb{N}},(L_{\to},F_{\textrm{RO},\Theta}^{110},(R_{=},x_{28},x_{29}))) \\ F_{\textrm{RO},\Theta}^{110} & = & (L_{\wedge},(F_{\textrm{Val},\Theta},x_{28},x_{29},c_1),(F_{\textrm{Val},\Theta},x_{29},x_{28},c_1)) \\ F_{\textrm{RO},\Theta}^{12} & = & (Q_{\forall \forall \forall \in},x_{28},x_{29},x_{30},c_{\mathbb{N}},F_{\textrm{RO},\Theta}^{120}) \\ F_{\textrm{RO},\Theta}^{120} & = & (L_{\to},F_{\textrm{RO},\Theta}^{1200},F_{\textrm{RO},\Theta}^{1201}) \\ F_{\textrm{RO},\Theta}^{1200} & = & (L_{\wedge},(F_{\textrm{Val},\Theta},x_{28},x_{29},c_1),(F_{\textrm{Val},\Theta},x_{29},x_{30},c_1)) \\ F_{\textrm{RO},\Theta}^{1201} & = & (F_{\textrm{Val},\Theta},x_{28},x_{30},c_1) \end{eqnarray*} \begin{eqnarray*} F_{\textrm{RWO},\Theta} & = & (L_{\wedge \wedge},F_{\textrm{RO},\Theta},F_{\textrm{RWO},\Theta}^{1},F_{\textrm{RWO},\Theta}^{2}) \\ F_{\textrm{RWO},\Theta}^{1} & = & (Q_{\forall \forall \in},x_{28},x_{29},c_{\mathbb{N}},(L_{\vee},F_{\textrm{RWO},\Theta}^{10},F_{\textrm{RWO},\Theta}^{11})) \\ F_{\textrm{RWO},\Theta}^{10} & = & (F_{\textrm{Val},\Theta},x_{28},x_{29},c_1) \\ F_{\textrm{RWO},\Theta}^{11} & = & (F_{\textrm{Val},\Theta},x_{29},x_{28},c_1) \\ F_{\textrm{RWO},\Theta}^{2} & = & (Q_{\forall \in},x_{31},(f_{\wedge},c_{\mathbb{N}},c_{\mathbb{N}}),(Q_{\exists \in},x_{32},c_{\mathbb{N}},F_{\textrm{RWO},\Theta}^{20})) \\ F_{\textrm{RWO},\Theta}^{20} & = & (F_{\textrm{Val},\Theta},(f_{\bullet ()},x_{31},x_{32}),(f_{\bullet ()},x_{31},(f_S,x_{32})),c_1) \end{eqnarray*}

\(F_{\textrm{RR},\Theta}\)、\(F_{\textrm{RO},\Theta}\)、\(F_{\textrm{RWO},\Theta}\)はそれぞれ\(\textrm{Output}_{\Theta}^{\mathbb{N}^2}\)が再帰的二項関係、再帰的順序、再帰的整列順序であることを形式化したものである。\(F_{\textrm{RR},\Theta}\)、\(F_{\textrm{RO},\Theta}\)、\(F_{\textrm{RWO},\Theta}\)に出現する各項配列は\(M\)が再帰的二項関係、再帰的順序、再帰的整列順序であることの定義における項に以下のように対応する：

項配列	項
\(c_i\)	\(i\)
\(c_{\mathbb{N}}\)	\(\mathbb{N}\)
\(x_1\)	長さ\(2\)のメモリ配列（自然数の組）\(M\)
\(x_{26}\)	\(\textrm{Output}_{\Theta}(M)\)
\(x_{28}, x_{29}, x_{30}\)	自然数を表す変数
\(x_{31}\)	数列\(a = (a_k)_{k = 0}^{\infty}\)
\(x_{32}\)	\(a\)の添字\(k\)

ちなみに今回は再帰的整列順序の形式化を用いたが、巨大数の定義に実際に用いる性質は基本列による展開の整礎性のみである。なので最初から整礎な基本列を形式化する方が効率的なのだが、そう変えたところでほんの少ししか増大度が上がらないと思われる上に、再帰的整列順序を用いた方が順序数表記の構造を持つという利点がある。ただし基本列の形式化を用いた方が下からの評価が証明しやすいので微妙なところである。詳しくは強い健全性という公理の直後の説明を参照すること。

降下列の形式化[]

コード配列\(\Theta, \Theta'\)に対し、以下のように略記を定める： \begin{eqnarray*} F_{\textrm{DS},\Theta,\Theta'} & = & (L_{\wedge},F_{\textrm{RWO},\Theta},F_{\textrm{DS},\Theta,\Theta'}^{1}) \\ F_{\textrm{DS},\Theta,\Theta'}^{1} & = & (Q_{\forall \forall \forall \in},x_{26},x_{28},x_{29},c_{\mathbb{N}},(F_{\textrm{DS},\Theta,\Theta'}^{10})) \\ F_{\textrm{DS},\Theta,\Theta'}^{10} & = & (L_{\to},(F_{\textrm{Val},\Theta'},x_{28},x_{29},x_{26}),F_{\textrm{DS},\Theta,\Theta'}^{100}) \\ F_{\textrm{DS},\Theta,\Theta'}^{100} & = & (L_{\vee},F_{\textrm{DS},\Theta,\Theta'}^{1000},F_{\textrm{DS},\Theta,\Theta'}^{1001}) \\ F_{\textrm{DS},\Theta,\Theta'}^{1000} & = & (F_{\textrm{Val},\Theta},x_{28},x_{26},c_0)) \\ F_{\textrm{DS},\Theta,\Theta'}^{1001} & = & (L_{\wedge},(R_{=},x_{28},x_{26}),F_{\textrm{DS},\Theta,\Theta'}^{10010}) \\ F_{\textrm{DS},\Theta,\Theta'}^{10010} & = & (Q_{\forall \in},x_{30},c_{\mathbb{N}},(F_{\textrm{Val},\Theta},x_{26},x_{30},c_1)) \end{eqnarray*}

\(F_{\textrm{DS},\Theta,\Theta'}\)は\(\textrm{Output}_{\Theta}^{\mathbb{N}^2}\)が再帰的整列順序でありかつ\(\textrm{Output}_{\Theta'}^{\mathbb{N}^2}\)がその順序に関して降下する再帰的二項演算であることを形式化したものである。より強く\(\textrm{Output}_{\Theta'}^{\mathbb{N}^2}\)が基本列をなすことを形式化することもできるが、FGHを考える上では基本列である必要がないので基本列の形式化は行わない。基本列とは限らない降下列に伴うFGHはさほど強くないが、後で特定の範囲内（有限）で全ての降下列を探索してFGHの合成をする予定であるため、結果的に基本列もその中に入ることから強さが十分保証されることに注意する。\(F_{\textrm{DS},\Theta,\Theta'}\)に出現する各項配列は\(\textrm{Output}_{\Theta}^{\mathbb{N}^2}\)が再帰的整列順序でありかつ\(\textrm{Output}_{\Theta'}^{\mathbb{N}^2}\)がその順序に関して降下する再帰的二項演算であることの定義における項に以下のように対応する：

項配列	項
\(c_i\)	\(i\)
\(c_{\mathbb{N}}\)	\(\mathbb{N}\)
\(x_{26}\)	\(\textrm{Output}_{\Theta'}(M)\)
\(x_{28}, x_{29}, x_{30}\)	自然数を表す変数

巨大数の構成[]

入れ子配列\(a\)が「降下列配列」であるとは、\(\textrm{Lng}(a) = 3\)でありかつ\(a_0,a_2\)がコード配列でありかつ\(a_1 \in \mathbb{N}\)であるということである。後に降下列配列と降下列付き順序数との対応を厳密に定義するが、理解しやすくするためにここで一旦「降下列付きの再帰的順序数に対応する」等の曖昧な表現を用いて大雑把なイメージを予め与えておく。

\((\Theta,k,\Phi)\)を降下列配列とし、\(\textrm{Output}_{\Theta}^{\mathbb{N}^2}\)が\(\mathbb{N}\)上の再帰的整列順序を定め、\(\textrm{Output}_{\Phi}^{\mathbb{N}^2}\)がそれに関する基本列を定めると仮定する。\((\Theta,\Phi)\)は降下列付きの再帰的順序数\(\alpha\)に対応するが、これは可算無限順序数であるので、このままでは\(1\)や\(2\)のような有限順序数へ対応させることが出来ず望ましい対応でない。そこで降下列配列はコード配列の組だけでなく別のデータ\(k \in \mathbb{N}\)も用いるのである。\(k\)から\(\textrm{Output}_{\Phi}^{\mathbb{N}^2}\)の定める降下列を繰り返し取って到達できる自然数全体を考える。すると、\(\textrm{Output}_{\Theta}^{\mathbb{N}^2}\)が定める\(\mathbb{N}\)上の再帰的整列順序のそこへの制限はやはり再帰的整列順序をなすので、それは有限かもしれない降下列付きの再帰的順序数\(\alpha_k\)を定める。こうして順序数への望ましい対応を得る。

ここで、降下列配列の配列を「順序数配列」と呼ぶ。ただFGHを考えたいだけであれば降下列配列を用いればよいのだが、きちんと限界関数が基本列と適切な意味^[14]で整合的になるよう技術的な工夫として順序数配列を用いる。順序数配列に対応させる順序数は単に、各成分の降下列配列に対応する順序数の和である。ちなみにこれまでの手法はある意味で、順序数配列でも降下列配列でもなくコード配列の集合に基本列を定めており、結果的に限界関数が基本列と整合的でなかった。今回新たに順序数配列を用いるようにしたことで初めて限界関数が基本列と整合的になったので、単なる通常の配列化以上にシステムが強力になったと言える。

降下列[]

ここで、コード配列の例で導入した\(\Theta_{\omega}\)と\(\Phi_{\omega}\)を用いる。\(k \in \mathbb{N}\)に対し\(a_{\omega}^{k} = (\Theta_{\omega},k,\Phi_{\omega})\)と置く。

\(A\)を順序数配列とし、\(n \in \mathbb{N}\)とする。順序数配列\(A[n]\)を以下のように再帰的に定める：

\(L = \textrm{Lng}(A)\)と置く。
\(L = 0\)ならば、\(A[n] = A\)である。
\(L > 0\)とする。
1. \((\Theta,k,\Phi) = A_{L-1}\)と置く。
2. \(n\)以下の各\(i \in \mathbb{N}\)に対し、\(b_i \in \mathbb{N}\)を以下のように再帰的に定める：
  1. \(i = 0\)とする。
    1. \(A_{L-1} \neq a_{\omega}^{k}\)ならば、\(b_i = 0\)である。
    2. \(A_{L-1} = a_{\omega}^{k}\)ならば、\(b_i = 1\)である。
  2. \(i > 0\)とする。
    1. \(b_{i-1} > 0\)ならば、\(b_i = b_{i-1}\)である。
    2. \(b_{i-1} = 0\)とする。
      1. \(\textrm{EnumNestArray}(i)\)が斧のみを用いる設計図配列でないならば、\(b_i = 0\)である。
      2. \(\textrm{EnumNestArray}(i)\)が斧のみを用いる設計図配列であるとする。
        \(\textrm{Result}(\textrm{EnumNestArray}(i)) \neq F_{\textrm{DS},\Theta,\Phi}\)であるならば、\(b_i = 0\)である。
        
        \(\textrm{Result}(\textrm{EnumNestArray}(i)) = F_{\textrm{DS},\Theta,\Phi}\)であるならば、\(b_i = i\)である。
3. \(b_n = 0\)ならば、\(A[n] = (A_i)_{L=0}^{L-2} \frown (a_{\omega}^{n})\)である。
4. \(b_n > 0\)とする。
  1. \(k' = \textrm{Output}_{\Phi}(k,n)\)と置く。
  2. \(k' = k\)とする。
    1. \(A_{L-1} = a_{\omega}^{k}\)ならば、\(A[n] = (A_i)_{i=0}^{L-2}\)である。
    2. \(A_{L-1} \neq a_{\omega}^{k}\)ならば、\(A[n] = (A_i)_{L=0}^{L-2} \frown (a_{\omega}^{n})\)である。
  3. \(k' \neq k\)ならば、\(A[n] = (A_i)_{L=0}^{L-2} \frown ((\Theta,k',\Phi))\)である。

やや場合分けが煩雑だが、大雑把には\(\textrm{Output}_{\Theta}^{\mathbb{N}^2}\)が\(\mathbb{N}\)上の再帰的整列順序を定めかつ\(\textrm{Output}_{\Phi}^{\mathbb{N}^2}\)がその降下列を定めかつ\(k\)が\(\textrm{Output}_{\Theta}^{\mathbb{N}^2}\)に関する最小要素でない場合にのみ\(k\)を\(\textrm{Output}_{\Phi}^{\mathbb{N}^2}\)で降下させ、そうでない場合は適当に調整するという操作を設計図配列を用いて形式化したものである。実際にこの降下列が望ましい性質を満たすことを確認するには標準自然数を用いた細かい議論が必要であるため、それは解析の章に回すこととする。

FGH[]

順序数配列の配列を「急増加関数配列」と呼ぶ。これは引数\(1\)関数配列等とは関係のない概念で、順序数配列ではなく急増加関数配列をここで用いるのは関数の合成を算術的に記述するためである。こうすることで、（本来は集合論の概念である）急増加関数階層を数列の言葉に翻訳して計算可能性を明確にすることができる。

急増加関数配列\(\mathbb{A}\)と\(n \in \mathbb{N}\)に対し、\(\langle \mathbb{A}, n \rangle \in \mathbb{N}\)を以下のように再帰的に定める：

\(L = \textrm{Lng}(\mathbb{A})\)と置く。
\(L = 0\)ならば、\(\langle \mathbb{A}, n \rangle = n\)である。
\(L > 0\)とする。
1. \(A = \mathbb{A}_{L-1}\)と置く。
2. \(A = ()\)ならば、\(\langle \mathbb{A}, n \rangle = \langle (\mathbb{A}_i)_{i=0}^{L-2}, n+1 \rangle\)である。
3. \(A \neq ()\)とする。
  1. \(n\)以下の各\(i \in \mathbb{N}\)に対し、急増加関数配列\(\mathbb{B}_i\)を以下のように再帰的に定める：
    1. \(i = 0\)ならば、\(\mathbb{B}_i = (\mathbb{A}_i)_{i=0}^{L-2}\)である。
    2. \(i > 0\)ならば、\(\mathbb{B}_i = \mathbb{B}_{i-1} \frown (A[n])\)である。
  2. \(\langle \mathbb{A}, n \rangle = \langle \mathbb{B}_n, n \rangle\)である。

例えば\(\mathbb{A}\)が１つの順序数配列\(A\)を用いて\((A)\)と表せる場合を考えれば、\(\langle (A), n \rangle = \langle (\underbrace{A[n],\ldots,A[n]}_n), n \rangle = \underbrace{\langle (A[n]), \cdots \langle (A[n])}_n, n \underbrace{\rangle \cdots \rangle}_n\)と展開されることから\(A\)に対応する関数に\(n\)を代入したものが\(A[n]\)に対応する関数を\(n\)個合成したものに\(n\)を代入したものとして処理されることが理解できるであろう。

限界関数[]

\(n \in \mathbb{N}\)に対し、順序数配列\(A_{\textrm{Lim}}^{n}\)を以下のように再帰的に定める：

\(n = 0\)ならば、\(A_{\textrm{Lim}}^{n} = ()\)である。
\(n > 0\)とする。
1. \(a = \textrm{EnumNestArray}(n)\)と置く。
2. \(a\)が降下列配列でないならば、\(A_{\textrm{Lim}}^{n} = A_{\textrm{Lim}}^{n-1} \frown (a_{\omega}^{n})\)である。
3. \(a\)が降下列配列であるならば、\(A_{\textrm{Lim}}^{n} = A_{\textrm{Lim}}^{n-1} \frown (a)\)である。

\(n \in \mathbb{N}\)に対し、急増加関数配列\(\mathbb{A}_{\textrm{LIM}}^{n}\)を以下のように再帰的に定める：

\(n = 0\)ならば、\(\mathbb{A}_{\textrm{LIM}}^{n} = ()\)である。
\(n > 0\)とする。
1. \(n\)未満の各\(i \in \mathbb{N}\)に対し、急増加関数配列\(\mathbb{A}_i\)を以下のように再帰的に定める：
  1. \(i = 0\)ならば、\(\mathbb{A}_i = (A_{\textrm{Lim}}^{n})\)である。
  2. \(i > 0\)ならば、\(\mathbb{A}_i = \mathbb{A}_{i-1} \frown \mathbb{A}_0\)である。
2. \(\mathbb{A}_{\textrm{LIM}}^{n} = \mathbb{A}_{n-1}\)である。

計算可能関数 \begin{eqnarray*} \textrm{Lim} \colon \mathbb{N} & \to & \mathbb{N} \\ n & \mapsto & \textrm{Lim}(n) \end{eqnarray*} を\(\textrm{Lim}(n) = \langle (A_{\textrm{Lim}}^{n}), n \rangle\)と定め、計算可能関数 \begin{eqnarray*} \textrm{LIM} \colon \mathbb{N} & \to & \mathbb{N} \\ n & \mapsto & \textrm{LIM}(n) \end{eqnarray*} を\(\textrm{Lim}(n) = \langle \mathbb{A}_{\textrm{LIM}}^{n}, n \rangle\)と定める。要するに\(\textrm{Lim}\)は順序数配列を用いた降下列系付き表記系に伴うFGHの限界関数で、\(\textrm{LIM}\)は等式\(\textrm{LIM}(n) = \textrm{Lim}^n(n)\)により特徴づけられる「限界関数を超えた関数」である。

また巨大数の定義には使わないが、せっかくなので表記系の項としての順序数配列に対し標準形の概念を導入しておく。以下を満たす最小の部分集合を\(OT \subset \textrm{NestArray}\)と定める：

いかなる\(n \in \mathbb{N}\)に対しても\(A_{\textrm{Lim}}^{n} \in OT\)である。
いかなる\(A \in OT\)と\(n \in \mathbb{N}\)に対しても\(A[n] \in OT\)である。

順序数配列が「標準形」であるとは、\(OT\)に属するということである。

\(\mathbb{A}\)には大小関係を原始再帰的関係として与えないので通常の意味での順序数表記をなさないが、順序数への対応自体は評価の章で具体的に定める。もっとも、巨大数界隈で順序数表記と称されている多くの表記系も大小関係が原始再帰的関係として与えられていない（ことに製作者が気付いていないことが多い）ので、ここでの「通常の意味」とは「数学における通常の意味」とするのが正しいかもしれない。単に順序数への対応が書けるというだけでは順序数表記にならないという点に注意が必要である。よくある誤解として「順序数に送った後で順序数としての大小関係を使えば良い」という主張があるが、それは原始再帰的関係として与えていないので順序数表記の定義は満たさないのである。

命名[]

\(\textrm{LIM}(100 \uparrow^{100} 100)\)を

さあ盟友、ついに巨大数屋敷の完成だ！　この屋敷の機能を説明しよう。まず１つ目は設計図の判定機能。文字列を読み込むと、それがこれらの斧だけを用いて巨大数屋敷を建てることができる設計図なのか否かを自動で判定してくれるんだ。次に２つ目が設計図の解析機能。巨大数屋敷の設計図を読み込むと、その屋敷に計算できる巨大関数を教えてくれるのさ。そして肝心の３つ目の機能が巨大関数の計算機能。ひとたび自然数を入力すると、それを文字数の上限とした範囲内にある全文字列を探索し、それぞれを設計図の判定機能に読み込ませることで有効な設計図のみを残して列挙し、更に設計図の解析機能に読み込ませることでそれらが計算できる巨大関数を入手し、それら全てをまとめ上げることで新たな巨大関数を計算できるんだ！　え？　それで本当に巨大な関数が得られるのかって？　相変わらず盟友は疑り深いなあ。でもいいさ、この巨大数屋敷自体の設計図がここにある。これを解析機能に読み込ませれば、どれほど巨大な関数を計算できるのかを教えてくれるからね。え？　この設計図の文字数？　そんなものを知って何になるんだい？

と名付ける^[15]。これを東方巨大数３のエントリーとする。

解析[]

\(\textrm{LIM}\)の解析を行う。また一般に算術で定義された順序数表記の整礎性などを証明する際には集合論を用いるように、ここから先は算術だけではなく\(\textrm{ZFC}\)集合論を用いる。当然公理などを使う必要があるため、証明に興味がない人は読まなくて良い。

メタ理論[]

\(\textrm{Lim}\)等を定義している\(\textrm{ZFC}\)集合論を\(T\)と置き、\(T\)のメタ理論を\(MT\)と置く。\(MT\)が具体的にどのような算術を含むかはあまり議論に関係ないので、ここでは適当に入れ子配列等が定義でき（つまり素因数分解ができ）かつ入れ子配列の木構造に関する数学的帰納法が適用可能であり（つまり帰納法の公理図式\(\textrm{Ind}(\varepsilon_0)\)を定理に含み）かつ\(T\)が\(\Sigma_1\)健全である（つまり\(T\)で停止性が証明可能な計算は実際に停止する）程度に強い算術を\(MT\)が内包しているとする。\(T\)の\(\Sigma_1\)健全性は\(T\)の無矛盾性を導くことに注意する。

\(\textrm{Output}\)や斧のみを用いる設計図配列等の定義文には配列と算術しか使っていないため、配列を素因数分解等で算術的に導入することで\(MT\)でも全く同じ定義をすることが出来る。ただし配列の性質を\(MT\)と\(T\)で揃えるため、\(() = 0\)が成り立つように導入することにする。\(MT\)で定義された概念を\(T\)で定義された概念と区別するために、「メタ」という接頭辞を付けて表す。

メタ入れ子配列\(A\)に対し、\(T\)の入れ子配列\(\ulcorner A \urcorner\)の定義文を以下のようにメタ再帰的に定める：

\(A\)が自然数であるとする。
1. \(A = 0\)ならば、\(\ulcorner A \urcorner\)は\(T\)の項\(0\)である。
2. \(A > 0\)ならば、\(\ulcorner A \urcorner\)は\(T\)の項\(\ulcorner A-1 \urcorner + 1\)である。
\(A\)が自然数でないとする。
1. \(L = \textrm{Lng}(A)\)と置く^[16]。
2. \(\ulcorner A \urcorner\)は\(T\)の項\(\ulcorner (A_i)_{i=0}^{L-2} \urcorner \frown (\ulcorner A_{L-1} \urcorner)\)である。

ただしこのようなメタ再帰が可能である背景には\(MT\)が帰納法の公理図式\(\textrm{Ind}(\varepsilon_0)\)を定理に含むことを要請しているからである。

メタ命題（（メタ入れ子配列の等式の遺伝性）
任意のメタ入れ子配列\(A_0 = A_1\)に対し、以下が成り立つ： \(A_0 = A_1\)ならば、「\(\ulcorner A_0 \urcorner = \ulcorner A_1 \urcorner\)である」ということが\(T\)で証明可能である。 \(A_0 \neq A_1\)ならば、「\(\ulcorner A_0 \urcorner \neq \ulcorner A_1 \urcorner\)である」ということが\(T\)で証明可能である。

証明：: １つ目の主張は\(\ulcorner A_0 \urcorner\)と\(\ulcorner A_1 \urcorner\)が同じ定義文を持つことから即座に従う。２つ目の主張は\(\textrm{Ind}(\varepsilon_0)\)から即座に従う。□

メタ命題（（メタ入れ子配列の性質の遺伝性）
任意のメタ入れ子配列\(A\)に対し、以下が成り立つ： \(A\)がメタコード配列（メタ屋敷配列、メタ斧配列、メタ設計図配列、メタ順序数配列、etc）であるならば、「\(\ulcorner A \urcorner\)がコード配列（屋敷配列、斧配列、設計図配列、順序数配列、etc）である」ということが\(T\)で証明可能である。 \(A\)がメタコード配列（メタ屋敷配列、メタ斧配列、メタ設計図配列、メタ順序数配列、etc）でないならば、「\(\ulcorner A \urcorner\)がコード配列（屋敷配列、斧配列、設計図配列、順序数配列、etc）でない」ということが\(T\)で証明可能である。

ちなみに\(T\)の無矛盾性からメタ入れ子配列の性質の遺伝性の主張の「ならば」部分を「同値」に変更したものも成り立つ。

証明：: \(\ulcorner \ \urcorner\)の定義と\(\textrm{Ind}(\varepsilon_0)\)から即座に従う。□

メタ系（設計図配列とメタ設計図配列の関係）
任意のメタ自然数\(n\)に対し、\(\textrm{EnumNestArray}(n)\)が斧のみを用いるメタ設計図配列ならば、\(T\)の論理式「\(\textrm{EnumNestArray}(\ulcorner n \urcorner)\)は斧のみを用いる設計図配列でありかつ\(\ulcorner \textrm{Result}(\textrm{EnumNestArray}(n)) \urcorner = \textrm{Result}(\textrm{EnumNestArray}(\ulcorner n \urcorner))\)」が\(T\)で証明可能である。

証明：: \(\textrm{EnumNestArray}(\ulcorner n \urcorner) = \ulcorner \textrm{EnumNestArray}(n) \urcorner\)が\(T\)で証明可能であることは\(\ulcorner \ \urcorner\)の定義から即座に従う。よって「\(\textrm{EnumNestArray}(\ulcorner n \urcorner)\)が斧のみを用いる設計図配列であることが\(T\)で証明可能である」ということはメタ入れ子配列の性質の遺伝性より従う。

\begin{eqnarray*} & & \ulcorner \textrm{Result}(\textrm{EnumNestArray}(n)) \urcorner = \textrm{Result}(\ulcorner \textrm{EnumNestArray}(n) \urcorner) \\ & = & \textrm{Result}(\textrm{EnumNestArray}(\ulcorner n \urcorner)) \end{eqnarray*} が\(T\)で証明可能であることは\(\ulcorner \ \urcorner\)の定義から即座に従う。従って\(\wedge\)導入則より従う。□

さて、\(\ulcorner a \urcorner\)が斧のみを用いる設計図配列であることが\(T\)で証明可能である時、\(T\)の無矛盾性とメタ入れ子配列の性質の遺伝性より\(a\)は斧のみを用いるメタ設計図配列である。この時\(a\)は自然に\(T\)における証明木に対応する。実際、\(\textrm{Ax}(a)\)の各成分はメタ斧配列であるため\(T\)の公理や定義文に自然に対応し、\(\textrm{Vrf}(a)\)は\(T\)の推論規則に自然に対応し、\(\textrm{Lmm}(a)\)は（\(\to\)除去や\(\neg\)導入等の推論規則の適用時に用いる）\(T\)の補題の証明木に対応する。これにより、\(T\)で何かを証明するためには\(MT\)で斧のみを用いる適切なメタ設計図配列を構成すれば十分となる。

メタ入れ子配列\(F\)とメタ自然数\(n\)に対し、自由変項\(k\)に関する\(T\)の論理式\(\textrm{IsBuildOf}_{F,n}\)を以下のようにメタ再帰的に定める：

\(n = 0\)ならば、\(\textrm{IsBuildOf}_{F,n}\)は\(T\)の論理式\(0 \neq 0\)である。
\(n > 0\)とする。
1. \(\textrm{EnumNestArray}(n-1)\)が斧のみを用いるメタ設計図配列でないならば、\(\textrm{IsBuildOf}_{F,n}\)は\(T\)の論理式\(\textrm{IsBuildOf}_{F,n-1}\)である。
2. \(\textrm{EnumNestArray}(n-1)\)が斧のみを用いるメタ設計図配列であるならば、\(\textrm{IsBuildOf}_{F,n}\)は\(T\)の論理式「\(\textrm{IsBuildOf}_{F,n-1}\)または『\(k = \ulcorner n-1 \urcorner\)かつ\(\textrm{Result}(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)) = \ulcorner F \urcorner\)』」である。

命題（屋敷配列の建築可能性とメタ屋敷配列のメタ建築可能性の関係）
\(F\)をメタ入れ子配列とし、\(n\)をメタ自然数とする。任意の\(k \in \mathbb{N}\)に対し、以下が同値である： \(k\)は\(\ulcorner n \urcorner\)未満かつ\(\textrm{EnumNestArray}(k)\)は斧のみを用いる設計図配列でありかつ\(\textrm{Result}(\textrm{EnumNestArray}(k)) = \ulcorner F \urcorner\)である。 \(\textrm{IsBuildOf}_{F,n}\)である。

証明：: 設計図配列とメタ設計図配列の関係より、「任意の\(k \in \mathbb{N}\)に対し、『\(k\)は\(\ulcorner n \urcorner\)未満かつ\(\textrm{EnumNestArray}(k)\)は斧のみを用いる設計図配列でありかつ\(\textrm{Result}(\textrm{EnumNestArray}(k)) = \ulcorner F \urcorner\)である』ということと『\(\textrm{IsBuildOf}_{F,n}\)である』ということが同値である」ということが\(T\)で証明可能であることは\(n\)に関するメタ帰納法から即座に従う。□

可証性[]

\(n \in \mathbb{N}\)とする。降下列配列\(a\)が「\(n\)可証」であるとは、\((\Theta,k,\Phi) = a\)と置くと以下を満たす\(n\)未満の\(i \in \mathbb{N}\)が存在するということである：

\(\textrm{EnumNestArray}(i)\)が斧のみを用いる設計図配列である。
\(\textrm{Result}(\textrm{EnumNestArray}(i)) = F_{\textrm{DS},\Theta,\Phi}\)である。

降下列配列\(a\)が「可証」であるとは、\(a\)が\(n\)可証である\(n \in \mathbb{N}\)が存在するということである。

コード配列\(\Theta\)が「整列」であるとは、\(\Theta\)が\(\mathbb{N}^2\)上で全域であり、かつ\(\textrm{Output}_{\Theta}^{\mathbb{N}^2}\)が\(\mathbb{N}\)上の整列順序を定める、すなわち\(\mathbb{N}\)上の二項関係\(\{(a,b) \in \mathbb{N}^2 \mid \textrm{Output}_{\Theta}((a,b)) = 1\}\)が\(\mathbb{N}\)上の整列順序であるということである。

もし「任意の可証降下列配列\((\Theta,k,\Phi)\)に対して\(\Theta\)が整列である」ということが\(T\)で証明可能であれば話は早いが、そうはいかないように定義されていることが\(\textrm{LIM}\)の強さの理由である。代わりに使えるのが以下の命題である。

命題（可証整列性と整列性の関係）
\((\Theta,k,\Phi)\)をメタ降下列配列とし、\(n\)をメタ自然数とする。\(\ulcorner (\Theta,k,\Phi) \urcorner\)が\(\ulcorner n \urcorner\)可証であるならば、以下が成り立つ： \(\ulcorner \Theta \urcorner\)は整列であり、\(\ulcorner \Phi \urcorner\)は全域である。任意の\(m_0,m_1 \in \mathbb{N}\)に対し、以下が成り立つ： \(m_0 \neq \textrm{Output}_{\ulcorner \Phi \urcorner}(m_0,m_1)\)ならば、\(\textrm{Output}_{\ulcorner \Theta \urcorner}(m_0,\textrm{Output}_{\ulcorner \Phi \urcorner}(m_0,m_1)) = 0\)である。 \(m_0 = \textrm{Output}_{\ulcorner \Phi \urcorner}(m_0,m_1)\)ならば、任意の\(m_2 \in \mathbb{N}\)に対し\(\textrm{Output}_{\ulcorner \Theta \urcorner}(m_0,m_2) = 1\)である。

証明：

「\(\ulcorner \Theta \urcorner\)は整列であり、\(\ulcorner \Phi \urcorner\)は全域であり、任意の\(m_0,m_1 \in \mathbb{N}\)に対し『\(m_0 \neq \textrm{Output}_{\Phi}(m_0,m_1)\)ならば、\(\textrm{Output}_{\Theta}(m_0,\textrm{Output}_{\Phi}(m_0,m_1)) = 0\)である』かつ『\(m_0 = \textrm{Output}_{\Phi}(m_0,m_1)\)ならば、任意の\(m_2 \in \mathbb{N}\)に対し\(\textrm{Output}_{\Theta}(m_0,m_2) = 1\)である。』」という命題を\(P\)と置き、「\(\ulcorner (\Theta,k,\Phi) \urcorner\)が\(\ulcorner n \urcorner\)可証であるならば、\(P\)である」という命題を\(Q\)と置く。\(Q\)が\(T\)で証明可能であることを\(n\)に関するメタ帰納法で示す。

\(n = 0\)とする。

「\(\ulcorner n \urcorner\)未満の自然数が存在しない」ということが\(T\)で証明可能であるため、「\(\ulcorner (\Theta,k,\Phi) \urcorner\)が\(\ulcorner n \urcorner\)可証でない」ということが\(T\)で証明可能である。特に爆発律から\(P\)は\(T\)に「\(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)\)は斧のみを用いる設計図配列でありかつ\(\textrm{Result}(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)) = F_{\textrm{DS},\ulcorner \Theta \urcorner, \ulcorner \Phi \urcorner}\)である」ということを公理として追加した理論で証明可能であり、演繹定理から\(Q\)が\(T\)で証明可能である。

\(n > 0\)とする。

排中律より「\(\ulcorner (\Theta,k,\Phi) \urcorner\)が\(\ulcorner n-1 \urcorner\)可証整列であるかまたは\(\ulcorner (\Theta,k,\Phi) \urcorner\)が\(\ulcorner n-1 \urcorner\)可証整列でない」ということが\(T\)で証明可能である。

メタ帰納法の仮定より、「\(\ulcorner (\Theta,k,\Phi) \urcorner\)が\(\ulcorner n-1 \urcorner\)可証整列であるならば\(\ulcorner \Theta \urcorner\)は整列である」ということが\(T\)で証明可能である。

屋敷配列の建築可能性とメタ屋敷配列のメタ建築可能性の関係より「\(\ulcorner (\Theta,k,\Phi) \urcorner\)が\(\ulcorner n-1 \urcorner\)可証整列でないかつ\(\ulcorner (\Theta,k,\Phi) \urcorner\)が\(\ulcorner n \urcorner\)可証整列であるならば、\(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)\)は斧のみを用いる設計図配列でありかつ\(\textrm{Result}(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)) = F_{\textrm{DS},\ulcorner \Theta \urcorner, \ulcorner \Phi \urcorner}\)である」ということが\(T\)で証明可能である。

従って\(\vee\)除去則より、「\(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)\)は斧のみを用いる設計図配列でありかつ\(\textrm{Result}(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)) = F_{\textrm{DS},\ulcorner \Theta \urcorner, \ulcorner \Phi \urcorner}\)であるならば\(P\)である」が\(T\)で証明可能であることを示せばよい。

まず\(\textrm{EnumNestArray}(n-1)\)が斧のみを用いるメタ設計図配列でないと仮定する。

メタ入れ子配列の性質の遺伝性より、「\(\ulcorner \textrm{EnumNestArray}(n-1)\)が斧のみを用いる設計図配列でない」ということが\(T\)で証明可能である。特に爆発律から\(P\)は\(T\)に「\(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)\)は斧のみを用いる設計図配列でありかつ\(\textrm{Result}(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)) = F_{\textrm{DS},\ulcorner \Theta \urcorner, \ulcorner \Phi \urcorner}\)である」ということを公理として追加した理論で証明可能であり、演繹定理から「\(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)\)は斧のみを用いる設計図配列でありかつ\(\textrm{Result}(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)) = F_{\textrm{DS},\ulcorner \Theta \urcorner, \ulcorner \Phi \urcorner}\)であるならば\(P\)である」が\(T\)で証明可能である。

次に\(\textrm{EnumNestArray}(n-1)\)が斧のみを用いるメタ設計図配列であると仮定する。

\(\ulcorner \ \urcorner\)の定義より、「\(\ulcorner F_{\textrm{DS},\Theta,\Phi} \urcorner = F_{\textrm{DS},\ulcorner \Theta \urcorner, \ulcorner \Phi \urcorner}\)である」ということと「\(\ulcorner \textrm{Result}(\textrm{EnumNestArray}(n-1)) \urcorner = \textrm{Result}(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner))\)である」ということが\(T\)で証明可能である。

まず\(\textrm{Result}(\textrm{EnumNestArray}(n-1)) \neq F_{\textrm{DS},\Theta,\Phi}\)と仮定する。

メタ入れ子配列の等式の遺伝性より、「\(\ulcorner \textrm{Result}(\textrm{EnumNestArray}(n-1)) \urcorner \neq \ulcorner F_{\textrm{DS},\Theta,\Phi} \urcorner\)である」ということが\(T\)で証明可能である。従って「\(\textrm{Result}(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)) \neq F_{\textrm{DS},\ulcorner \Theta \urcorner, \ulcorner \Phi \urcorner}\)である」ということが\(T\)で証明可能である。特に爆発律から\(P\)は\(T\)に「\(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)\)は斧のみを用いる設計図配列でありかつ\(\textrm{Result}(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)) = F_{\textrm{DS},\ulcorner \Theta \urcorner, \ulcorner \Phi \urcorner}\)である」ということを公理として追加した理論で証明可能であり、演繹定理から「\(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)\)は斧のみを用いる設計図配列でありかつ\(\textrm{Result}(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)) = F_{\textrm{DS},\ulcorner \Theta \urcorner, \ulcorner \Phi \urcorner}\)であるならば\(P\)である」が\(T\)で証明可能である。

次に\(\textrm{Result}(\textrm{EnumNestArray}(n-1)) = F_{\textrm{DS},\Theta,\Phi}\)と仮定する。

斧のみを用いるメタ設計図配列\(\textrm{EnumNestArray}(n-1)\)に対応する\(T\)の証明木は\(P\)のゲーデル数を入れ子配列で表示した\(F_{\textrm{DS},\Theta,\Phi}\)を帰結するので、\(P\)は\(T\)で証明可能である。特に\(P\)は\(T\)に「\(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)\)は斧のみを用いる設計図配列でありかつ\(\textrm{Result}(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)) = F_{\textrm{DS},\ulcorner \Theta \urcorner, \ulcorner \Phi \urcorner}\)である」ということを公理として追加した理論でも証明可能であり、演繹定理から「\(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)\)は斧のみを用いる設計図配列でありかつ\(\textrm{Result}(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)) = F_{\textrm{DS},\ulcorner \Theta \urcorner, \ulcorner \Phi \urcorner}\)であるならば\(P\)である」が\(T\)で証明可能である。

以上より、いずれの場合も「\(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)\)は斧のみを用いる設計図配列でありかつ\(\textrm{Result}(\textrm{EnumNestArray}(\ulcorner n-1 \urcorner)) = F_{\textrm{DS},\ulcorner \Theta \urcorner, \ulcorner \Phi \urcorner}\)であるならば\(P\)である」が\(T\)で証明可能である。□

停止性[]

計算可能関数\(f\)に対し、その定義域を\(\textrm{Dom}(f)\)と置く。急増加関数配列全体のなす部分集合を\(\textrm{FGH} \subset \textrm{NestArray}\)と置く。\(\textrm{FGH} \times \mathbb{N}\)上の計算可能部分関数\((A,n) \mapsto \langle A, n \rangle\)を\(\mathcal{F}\)と置く。全域性\(\textrm{Dom}(\mathcal{F}) = \textrm{FGH} \times \mathbb{N}\)を証明できれば話が早いが、そうは問屋が卸さない。代わりに示すのが以下の定理である：

定理（メタ急増加関数配列による切片の基本性質）
\(\mathbb{A}\)をメタ急増加関数配列とし、\(n\)をメタ自然数とする。この時\((\ulcorner \mathbb{A} \urcorner, \ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)である。

ここで、計算可能関数の定義域という概念の定義から(\textrm{Dom}(\mathcal{F})\)は「\(\mathcal{F}\)の計算が停止する入力全体の集合」に他ならないが、計算が停止するとはすなわち\(\mathcal{F}\)の計算を実行するチューリングマシンが停止するということである。今回はチューリングマシンの停止性という概念の定義を説明していないが、それは対応するコード配列の停止性と等価であることが容易に従うため、ここでは代わりにコード配列の停止性を考えることとする。

メタ急増加関数配列の基本性質を示すための準備として、いくつかのメタ補題を用意する。

メタ補題（有限順序数に伴う急増加関数階層が形式化と整合的であること）
有限順序数に伴う急増加関数階層\((f_i)_{i=0}^{\infty}\)に関して、以下が成り立つ： \((f_i)_{i=0}^{\infty}\)の全域性が\(MT\)で証明可能である。 \(n,k\)をメタ自然数とする。この時「\(((\ulcorner a_{\omega}^{k} \urcorner), \ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle (\ulcorner a_{\omega}^{k} \urcorner), \ulcorner n \urcorner \rangle = \ulcorner f_k(n) \urcorner\)である」ということが\(T\)で証明可能である。

証明：

１つ目の主張はメタ帰納法により即座に従う。「いかなるメタ自然数\(n\)に対しても『\(((\ulcorner a_{\omega}^{k} \urcorner), \ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle (\ulcorner a_{\omega}^{k} \urcorner), \ulcorner n \urcorner \rangle = \ulcorner f_k(n) \urcorner\)である』ということが\(T\)で証明可能である」ということを\(k\)に関するメタ帰納法で示す。

\(k = 0\)ならば、\(\mathcal{F}\)の定義から即座に従う。

\(k > 0\)とする。

メタ帰納法の仮定より、いかなるメタ自然数\(n\)に対しても「\(((\ulcorner a_{\omega}^{k-1} \urcorner), \ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle (\ulcorner a_{\omega}^{k-1} \urcorner), \ulcorner n \urcorner \rangle = \ulcorner f_{k-1}(n) \urcorner\)である」ということが\(T\)で証明可能である。

\(n\)をメタ自然数とする。\(n\)未満の各メタ自然数\(i\)に対し、メタ急増加関数配列\(B_i\)を以下のように再帰的に定める：

\(i = 0\)ならば、\(B_i = ()\)である。
\(i > 0\)ならば、\(B_i = B_{i-1} \frown (a_{\omega}^{k})[n]\)である。

\(k > 0\)と\(\Theta_{\omega}\)と\(\Phi_{\omega}\)の基本性質より、\((a_{\omega}^{k})[n] = (a_{\omega}^{k-1}) \neq (a_{\omega}^{k})\)である。従って\(\mathcal{F}\)の定義から「\(((\ulcorner a_{\omega}^{k} \urcorner),\ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle (\ulcorner a_{\omega}^{k} \urcorner), \ulcorner n \urcorner \rangle = \ulcorner f_k(n) \urcorner\)である」ということと「\((\ulcorner B_n \urcorner,\ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle \ulcorner B_n \urcorner, \ulcorner n \urcorner \rangle = \ulcorner f_k(n) \urcorner\)である」ということの同値性が\(T\)で証明可能である。

「いかなるメタ自然数\(h\)に対しても『\((\ulcorner B_n \urcorner,\ulcorner h \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle \ulcorner B_n \urcorner, \ulcorner h \urcorner \rangle = \ulcorner f_{k-1}^n(h) \urcorner \)である』ということが\(T\)で証明可能である」ということを\(n\)に関するメタ帰納法で示す。

\(n = 0\)ならば、\(B_n = ()\)であるため上での議論より従う。

\(n = 1\)ならば、\(B_n = (a_{\omega}^{k})[n] = (a_{\omega}^{k-1})\)であるので、上での議論より従う。

\(n > 1\)とする。

メタ帰納法の仮定よりいかなるメタ自然数\(h\)に対しても『\((\ulcorner B_{n-1} \urcorner,\ulcorner h \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle \ulcorner B_{n-1} \urcorner, \ulcorner h \urcorner \rangle = \ulcorner f_{k-1}^{n-1}(h) \urcorner\)である』ということが\(T\)で証明可能である。

上での議論よりいかなるメタ自然数\(h\)に対しても『\((\ulcorner B_1 \urcorner,\ulcorner h \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle \ulcorner B_1 \urcorner, \ulcorner h \urcorner \rangle = \ulcorner f_{k-1}(h) \urcorner\)である』ということが\(T\)で証明可能であるので、特に\(\forall\)除去則により『\((\ulcorner B_1 \urcorner,\ulcorner f_{k-1}^{n-1}(h) \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle \ulcorner B_1 \urcorner, \ulcorner f_{k-1}^{n-1}(h) \urcorner \rangle = \ulcorner f_{k-1}^n(h) \urcorner\)である』ということが\(T\)で証明可能である。

以上より、\(\mathcal{F}\)の定義からいかなるメタ自然数\(h\)に対しても『\((\ulcorner B_n \urcorner,\ulcorner h \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle \ulcorner B_n \urcorner, \ulcorner h \urcorner \rangle = \ulcorner f_{k-1}^n(h) \urcorner\)である』ということが\(T\)で証明可能である。

\(\forall\)除去則により『\((\ulcorner B_n \urcorner,\ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle \ulcorner B_n \urcorner, \ulcorner n \urcorner \rangle = \ulcorner f_{k-1}^n(n) \urcorner\)である』ということが\(T\)で証明可能である。\(f_{k-1}^n(n) = f_k(n)\)であることからメタ入れ子配列の等式の遺伝性 (1)より『\((\ulcorner B_n \urcorner,\ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle \ulcorner B_n \urcorner, \ulcorner n \urcorner \rangle = \ulcorner f_k(n) \urcorner\)である』ということが\(T\)で証明可能である。

従って「\(((\ulcorner a_{\omega}^{k}) \urcorner,\ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(langle (\ulcorner a_{\omega}^{k} \urcorner), \ulcorner n \urcorner \rangle = \ulcorner f_k(n) \urcorner\)である」ということは\(T\)で証明可能である。□

メタ補題（標準自然数をゲーデル数に持つ降下列配列が標準自然数を出力すること）
\(a\)をメタ降下列配列とし、\(n\)をメタ自然数とする。この時「\((((\ulcorner a \urcorner)), \ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle ((\ulcorner a \urcorner)), \ulcorner n \urcorner \rangle = \ulcorner m \urcorner\)である」ということが\(T\)で証明可能であるメタ自然数\(m\)が存在する。

ちなみにそのような\(m\)の一意性は\(T\)の無矛盾性から従うが、今回は一意性を使わないので存在性だけ示す。

証明：: \((\Theta,k,\Phi) = a\)と置く。; \(n\)以下の各メタ自然数\(i\)に対し、メタ自然数\(b_i\)を以下のようにメタ再帰的に定める：

\(i = 0\)とする。
1. \(a \neq a_{\omega}^{k}\)ならば、\(b_i = 0\)である。
2. \(a = a_{\omega}^{k}\)ならば、\(b_i = 1\)である。
\(i > 0\)とする。
1. \(b_{i-1} > 0\)ならば、\(b_i = b_{i-1}\)である。
2. \(b_{i-1} = 0\)とする。
  1. \(\textrm{EnumNestArray}(i)\)が斧のみを用いるメタ設計図配列でないならば、\(b_i = 0\)である。
  2. \(\textrm{EnumNestArray}(i)\)が斧のみを用いるメタ設計図配列であるとする。
    1. \(\textrm{Result}(\textrm{EnumNestArray}(i)) \neq F_{\textrm{DS},\Theta,\Phi}\)であるならば、\(b_i = 0\)である。
    2. \(\textrm{Result}(\textrm{EnumNestArray}(i)) = F_{\textrm{DS},\Theta,\Phi}\)であるならば、\(b_i = i\)である。

\(b_n = 0\)とする。

メタ入れ子配列の性質の遺伝性から、「\(\ulcorner n \urcorner\)未満の任意の\(i \in \mathbb{N}\)に対し\(\textrm{EnumNestArray}(i)\)が設計図配列であるならば\(\textrm{Result}(\textrm{EnumNestArray}(i)) \neq F_{\textrm{DS},\ulcorner \Theta \urcorner,\ulcorner \Phi \urcorner}\)である」ということが\(T\)で証明可能である。従って\((a)[n] = (a_{\omega}^{k})\)となるので、有限順序数に伴う急増加関数階層が形式化と整合的であることより従う。: \(b_n > 0\)とする。

\(a = a_{\omega}^{k}\)であるならば、有限順序数に伴う急増加関数階層が形式化と整合的であることより従う。

\(a \neq a_{\omega}^{k}\)とする。

\(\ulcorner \ \urcorner\)の定義より「\(\ulcorner a_{\omega}^{k} \urcorner = a_{\omega}^{\ulcorner k \urcorner}\)である」ということが\(T\)で証明可能であり、\(a \neq a_{\omega}^{k}\)よりメタ入れ子配列の等式の遺伝性から「\(\ulcorner a \urcorner \neq \ulcorner a_{\omega}^{k} \urcorner\)である」ということが\(T\)で証明可能である。

\(b_n\)の定義より\(b_n \leq n\)であり、かつ\(b_n\)未満の任意のメタ自然数\(i\)に対し\(\textrm{EnumNestArray}(i)\)がメタ設計図配列であるならば\(\textrm{Result}(\textrm{EnumNestArray}(i)) \neq F_{\textrm{DS},\Theta,\Phi}\)であり、かつ\(\textrm{EnumNestArray}(b_n)\)がメタ設計図配列でありかつ\(\textrm{Result}(\textrm{EnumNestArray}(b_n)) = F_{\textrm{DS},\Theta,\Phi}\)である。

従ってメタ入れ子配列の性質の遺伝性から、「\(\ulcorner b_n \urcorner \leq \ulcorner n \urcorner\)であり、かつ\(\ulcorner b_n \urcorner\)未満の任意の\(i \in \mathbb{N}\)に対し\(\textrm{EnumNestArray}(i)\)が設計図配列であるならば\(\textrm{Result}(\textrm{EnumNestArray}(i)) \neq F_{\textrm{DS},\ulcorner \Theta \urcorner,\ulcorner \Phi \urcorner}\)であり、かつ\(\textrm{EnumNestArray}(\ulcorner b_n \urcorner)\)が設計図配列でありかつ\(\textrm{Result}(\textrm{EnumNestArray}(\ulcorner b_n \urcorner)) = F_{\textrm{DS},\ulcorner \Theta \urcorner,\ulcorner \Phi \urcorner}\)である」ということが\(T\)で証明可能である。

特に「\(\ulcorner a \urcorner\)が\(\ulcorner n \urcorner\)可証である」ということと「任意の\(k' \in \mathbb{N}\)と\(\ulcorner b_n \urcorner\)以上の任意の\(n' \in \mathbb{N}\)に対し\(((\ulcorner \Theta \urcorner,k',\ulcorner \Phi \urcorner))[n'] = ((\ulcorner \Theta \urcorner,\textrm{Output}_{\ulcorner \Phi \urcorner}(k',n'),\ulcorner \Phi \urcorner))\)である」ということが\(T\)で証明可能となる。

従って可証整列性と整列性の関係から以下が\(T\)で証明可能である：

\(\ulcorner \Theta \urcorner\)は整列であり、\(\ulcorner \Phi \urcorner\)は全域である。
任意の\(m_0,m_1 \in \mathbb{N}\)に対し、以下が成り立つ：
1. \(m_0 \neq \textrm{Output}_{\ulcorner \Phi \urcorner}(m_0,m_1)\)ならば、\(\textrm{Output}_{\ulcorner \Theta \urcorner}(m_0,\textrm{Output}_{\Phi}(m_0,m_1)) = 0\)である。
2. \(m_0 = \textrm{Output}_{\ulcorner \Phi \urcorner}(m_0,m_1)\)ならば、任意の\(m_2 \in \mathbb{N}\)に対し\(\textrm{Output}_{\ulcorner \Theta \urcorner}(m_0,m_2) = 1\)である。

従って\(\textrm{Output}_{\ulcorner \Theta \urcorner}^{\mathbb{N}^2}\)の整礎性による超限帰納法から、「任意の\(k' \in \mathbb{N}\)と\(\ulcorner b_n \urcorner\)以上の任意の\(n' \in \mathbb{N}\)に対し\((((\ulcorner \Theta \urcorner,k',\ulcorner \Phi \urcorner)),n') \in \textrm{Dom}(\mathcal{F})\)である」ということが\(T\)で証明可能である。特に\(\forall\)除去則により、「\((((\ulcorner a \urcorner)),\ulcorner n\urcorner) \in \textrm{Dom}(\mathcal{F})\)である」ということが\(T\)で証明可能である。

\(T\)が\(\Sigma_1\)健全であることから、\(MT\)において\(\langle ((a)), n \rangle\)の計算は有限回の計算ステップで停止し、特に\(((a),n) \in \textrm{Dom}(\mathcal{F})\)である。\(\ulcorner \ \urcorner\)の定義から「\(\langle ((\ulcorner a \urcorner)), \ulcorner n \urcorner \rangle = \ulcorner \langle ((a)), n \rangle \urcorner\)である」ということが\(T\)で証明可能である^[17]。□

メタ補題（標準自然数をゲーデル数に持つ順序数配列が標準自然数を出力すること）
\(A\)をメタ順序数配列とし、\(n\)をメタ自然数とする。この時「\(((\ulcorner A \urcorner), \ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle (\ulcorner A \urcorner), \ulcorner n \urcorner \rangle = \ulcorner m \urcorner\)である」ということが\(T\)で証明可能であるメタ自然数\(m\)が存在する。

証明：

メタ自然数\(L\)に関するメタ命題「\(\textrm{Lng}(A) = L\)を満たすいかなるメタ順序数配列\(A\)とメタ自然数\(n\)に対しても、『\(((\ulcorner A \urcorner), \ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle (\ulcorner A \urcorner), \ulcorner n \urcorner \rangle = \ulcorner m \urcorner\)である』ということが\(T\)で証明可能であるメタ自然数\(m\)が存在する」ということを\(L\)に関するメタ帰納法で示す。

\(L = 0\)ならば、\(\mathcal{F}\)の定義より「\(((\ulcorner A \urcorner), \ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle (\ulcorner A \urcorner), \ulcorner n \urcorner \rangle = \ulcorner n \urcorner\)である」ということが\(T\)で証明可能である。

\(L = 1\)ならば、標準自然数をゲーデル数に持つ降下列配列が標準自然数を出力することより従う。

\(L > 1\)とする。

メタ帰納法の仮定より、『\(((\ulcorner (A_i)_{i=1}^{L-1} \urcorner), \ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle (\ulcorner A \urcorner), \ulcorner n \urcorner \rangle = \ulcorner m' \urcorner\)である』ということが\(T\)で証明可能であるメタ自然数\(m'\)が存在し、『\(((\ulcorner (A_0) \urcorner), \ulcorner m' \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle (\ulcorner A \urcorner), \ulcorner m' \urcorner \rangle = \ulcorner m \urcorner\)である』ということが\(T\)で証明可能であるメタ自然数\(m\)が存在する。特に『\(((\ulcorner A \urcorner), \ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle (\ulcorner A \urcorner), \ulcorner n \urcorner \rangle = \ulcorner m \urcorner\)である』ということが\(T\)で証明可能である。□

メタ急増加関数配列の基本性質の証明：

\(L\)をメタ自然数とする。「\(\textrm{Lng}(\mathbb{A}) = L\)を満たすいかなるメタ急増加関数配列\(\mathbb{A}\)とメタ自然数\(n\)に対しても、『\((\ulcorner \mathbb{A} \urcorner, \ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle \ulcorner \mathbb{A} \urcorner, \ulcorner n \urcorner \rangle = \ulcorner m \urcorner\)である』ということが\(T\)で証明可能であるメタ自然数\(m\)が存在する」ということを\(L\)に関するメタ帰納法で示す。

\(L = 0\)ならば、\(\mathcal{F}\)の定義より\(\textrm{Lng}(A) = L\)を満たすいかなるメタ急増加関数配列\(\mathbb{A}\)とメタ自然数\(n\)に対しても、「\((\ulcorner \mathbb{A} \urcorner, \ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle \ulcorner \mathbb{A} \urcorner, \ulcorner n \urcorner \rangle = \ulcorner n \urcorner\)である」ということが\(T\)で証明可能である。

\(L > 0\)とする。

\(\mathbb{A}\)を\(\textrm{Lng}(A) = L\)を満たすメタ急増加関数配列とし、\(n\)をメタ自然数とする。メタ帰納法の仮定より、「\((\ulcorner (\mathbb{A}_i)_{i=1}^{L-1} \urcorner, \ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle \ulcorner (\mathbb{A}_i)_{i=1}^{L-1} \urcorner, \ulcorner n \urcorner \rangle = \ulcorner m' \urcorner\)である」ということが\(T\)で証明可能であるメタ自然数\(m'\)が存在する。

標準自然数をゲーデル数に持つ順序数配列が標準自然数を出力することより、「\((\ulcorner (\mathbb{A}_0) \urcorner, \ulcorner m' \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle \ulcorner (\mathbb{A}_0) \urcorner, \ulcorner m' \urcorner \rangle = \ulcorner m \urcorner\)である」ということが\(T\)で証明可能であるメタ自然数\(m\)が存在する。

\(\mathcal{F}\)の定義から、「\((\ulcorner \mathbb{A} \urcorner, \ulcorner n \urcorner) \in \textrm{Dom}(\mathcal{F})\)かつ\(\langle \ulcorner \mathbb{A} \urcorner, \ulcorner n \urcorner \rangle = \ulcorner m \urcorner\)である」ということが\(T\)で証明可能である。□

系（限界関数の値のwell-defined性）
\(n\)をメタ自然数とする。この時、\(\ulcorner n \urcorner \in \textrm{Dom}(\textrm{Lim})\)かつ\(\ulcorner n \urcorner \in \textrm{Dom}(\textrm{LIM})\)である。

証明：: \(A_{\textrm{Lim}}\)と\(\mathbb{A}_{\textrm{LIM}}\)の定義より、メタ急増加関数配列の基本性質から即座に従う。□

これにより、いかなるメタ自然数\(n\)に対しても\(\textrm{LIM}(\ulcorner n \urcorner)\)のwell-defined性が\(T\)で証明可能であることが従う。注意が必要なのは、この議論から従うのは

\(\textrm{LIM}(0)\)がwell-definedである。
\(\textrm{LIM}(1)\)がwell-definedである。
\(\textrm{LIM}(2)\)がwell-definedである。
\(\vdots\)
\(\textrm{LIM}(100)\)がwell-definedである。
\(\vdots\)
\(\textrm{LIM}(100 \uparrow^{100} 100)\)がwell-definedである。
\(\vdots\)

という無限個の命題がいずれも\(T\)で証明可能であるというだけで、\(\textrm{LIM}\)の全域性である「いかなる\(n \in \mathbb{N}\)に対しても\(\textrm{LIM}(n)\)がwell-definedであること」が\(T\)で証明可能であるということは従わないということである^[18]。

これは\(\textrm{PA}\)でCantor標準形に伴うWainer階層に関して

\(f_{\varepsilon_0}(0)\)がwell-definedである。
\(f_{\varepsilon_0}(1)\)がwell-definedである。
\(f_{\varepsilon_0}(2)\)がwell-definedである。
\(\vdots\)

が証明できるのに「いかなる\(n \in \mathbb{N}\)に対しても\(f_{\varepsilon_0}(n)\)がwell-definedであること」が証明できないことや、\(\Pi_1^1 \textrm{-CA}_0\)でBuchholzの\(\psi\)関数と順序数表記に伴う基本列に関して

\(f_{\psi_0(\Omega_{\omega}(0))}(0)\)がwell-definedである。
\(f_{\psi_0(\Omega_{\omega}(0))}(1)\)がwell-definedである。
\(f_{\psi_0(\Omega_{\omega}(0))}(2)\)がwell-definedである。
\(\vdots\)

が証明できるのに「いかなる\(n \in \mathbb{N}\)に対しても\(f_{\psi_0(\Omega_{\omega}(0))}(n)\)がwell-definedであること」が証明できないことと類似の現象で、\(n\)ごとに命題の証明の構造が著しく変化していくため\(\forall\)導入則がそのままでは適用可能でないということである。

評価[]

\(\alpha\)を\(\textrm{PTO}(\textrm{ZFC})\)未満の可算無限順序数とする。定義から、順序数型が\(\alpha\)であるような\(\mathbb{N}\)上の再帰的整列順序を定めるチューリングマシンであって、「形式化された\(\textrm{ZFC}\)集合論で整列順序性が証明可能である」すなわち「整列順序性のゲーデル数を帰結する形式化された\(\textrm{ZFC}\)集合論の証明木のゲーデル数が存在する」という条件を満たすものが存在する。

コード配列システムのチューリング完全性と、斧配列と設計図配列を用いた\(\textrm{ZFC}\)集合論の形式化により、順序数型が\(\alpha\)であるような\(\mathbb{N}\)上の再帰的整列順序を定めるコード配列\(\Theta\)であって、「\(\textrm{EnumNestArray}(i)\)が設計図配列であり\(\textrm{Result}(\textrm{EnumNestArray}(i)) = F_{\textrm{RWO},\Theta}\)を満たす\(i \in \mathbb{N}\)が存在する」という条件を満たすものが存在する。また\(\alpha = 1 + \alpha\)であることから、\(\Theta\)を取り替えることで再帰的整列順序に関する最小要素が計算可能となるように\(\Theta\)を選ぶことが出来る。最小要素の計算可能性から\(\Theta\)に対しては「\(\textrm{Output}_{\Phi}^{\mathbb{N}^2}\)が全域でありかつ\(\textrm{Output}_{\Theta}^{\mathbb{N}^2}\)に関する基本列系を定め、\(\textrm{EnumNestArray}(j)\)が設計図配列でありかつ\(\textrm{Result}(\textrm{EnumNestArray}(j)) = F_{\textrm{DS},\Theta,\Phi}\)を満たす\(j \in \mathbb{N}\)が存在する」という条件を満たすコード配列\(\Phi\)が存在することが初等的に分かる。そのような条件を満たすいかなる\(\Phi\)といかなる\(k \in \mathbb{N}\)に対しても、降下列配列\((\Theta,k,\Phi)\)に伴う計算可能関数\(\langle ((\Theta,k,\Phi)) , n \rangle\)の増大度は次の意味で\(\textrm{Lim}(n)\)で抑えられる：

命題（限界関数の評価）
上記の条件を満たす降下列配列\((\Theta,k,\Phi)\)に対し、以下が成り立つ：任意の\(n \in \mathbb{N}\)に対し、\((((\Theta,k,\Phi)),n) \in \textrm{Dom}(\mathcal{F})\)である。任意の\(n,j \in \mathbb{N}\)に対し、\(\textrm{EnumNestArray}(j)\)が設計図配列でありかつ\(\textrm{Result}(\textrm{EnumNestArray}(j)) = F_{\textrm{DS},\Theta,\Phi}\)かつ\(n \geq j\)であるならば、\(\langle ((\Theta,k,\Phi)), n \rangle = f_{\alpha'}(n)\)である。ただし\(\alpha'\)は\(\mathbb{N}\)上の整列順序\(\textrm{Output}_{\Theta}^{\mathbb{N}^2}\)の\(\{h \in \mathbb{N} \mid \textrm{Output}_{\Theta}(h,k) = 1\}\)への制限の順序数型であり、FGHは基本列系\(\textrm{Output}_{\Phi}^{\mathbb{N}^2}\)の制限に伴うものである。 \(m \in \mathbb{N}\)が\(\textrm{EnumNestArray}(m) = (\Theta,k,\Phi)\)を満たすならば、任意の\(n \in \mathbb{N}\)に対し、\(n \geq m\)かつ\(n \in \textrm{Dom}(\textrm{Lim})\)ならば\(\langle ((\Theta,k,\Phi)), n \rangle \leq \textrm{Lim}(n)\)である。

証明：: １つ目の主張と２つ目の主張は\(\mathcal{F}\)の定義と\(\Phi\)の条件から即座に従う。３つ目の主張は、任意の\(n \in \mathbb{N}\)に対し\(n \geq m\)かつ\(n \in \textrm{Dom}(\textrm{Lim})\)ならば\((A_{\textrm{Lim}}^{n})_m = (\Theta,k,\Phi)\)であるので\(\textrm{Lim}(n) = \langle ((A_{\textrm{Lim}}^{n})_h)_{h=j+1}^{n}), \langle ((\Theta,k,\Phi)), \langle ((A_{\textrm{Lim}}^{n})_h)_{h=0}^{j-1}), n \rangle \rangle \rangle\)であることから即座に従う。□

ここで、\(\alpha\)が\(\textrm{PTO}(\textrm{ZFC})\)未満であることから、\(\alpha + 2\)もまた\(\textrm{PTO}(\textrm{ZFC})\)未満である。従って限界関数の評価から\(\textrm{Lim}\)の定義域における増大度が、\(\alpha\)とその上の再帰的基本列であって降下性が証明可能であるものに伴うFGHより真に大きいということが分かる。

以上のことから、\(\textrm{LIM}(100 \uparrow^{100} 100)\)の大きさをある程度下から抑えることが出来る。実際フェルミ推定により、地球に存在する電子の個数は\(100 \uparrow^2 5\)で抑えられるため、これまで地球上で書かれてきた数学の論文の総文字数もそれで抑えられ、それらに含まれる略記を全て展開した文字数は\(2^{100 \uparrow^2 5} < 100 \uparrow^2 6\)で抑えられる。従ってそれらに含まれる形式証明の証明木に対応する設計図配列を\(\textrm{EnumNestArray}\)の逆写像で写したものは\(2 \uparrow^2 (100 \uparrow^2 6) < 100 \uparrow^3 3\)で抑えられる。特に、巨大基数の可算崩壊等で得られる基本列付き巨大順序数として記述されることが\(\textrm{ZFC}\)公理系で既に証明されている^[19]ものに関しては、それに付随するFGHが\(\textrm{Lim}(100 \uparrow^3 3)\)で抑えられる。\(\textrm{Lim}\)と\(\textrm{LIM}\)は初速が遅く、小さい入力値においてはWainer階層におけるFGHに関して\(f_{\omega+1}\)で十分抑えられる程度の増え方しかしないが、このように\(100 \uparrow^3 3\)程度に大きい入力値であれば十分早く増えていくことが分かる。

さて、ここまでの緩い評価は超越整数システムでも可能なことであるので、もう少し強い評価を与えたい。そのために、\(T\)に公理を追加した体系を用意する。例えば\(T\)に追加の公理として\(\textrm{ZFC}\)集合論の健全性を課すとどうなるかを考える。つまり\(MT\)に\(T\)の\(\Sigma_1\)健全性を課したように、\(T\)内で斧配列や設計図配列を用いて形式化した\(\textrm{ZFC}\)集合論の健全性を課すということである。この時、任意の可証降下列配列\((\Theta,k,\Phi)\)に対して、\(\Theta\)と\(\Phi\)が\(\mathbb{N}^2\)上で全域なコード配列となり更に\(\textrm{Output}_{\Theta}^{\mathbb{N}^2}\)が\(\mathbb{N}\)上の関係を定める。しかしながら\(\Theta\)が整列であるかどうかや、\(\textrm{Output}_{\Theta}^{\mathbb{N}^2}\)の定める関係に関して\(\textrm{Output}_{\Phi}^{\mathbb{N}^2}\)が降下列をなすことが従うかどうかはよく分からない^[20]。そこで今回はより強く、以下の公理を直接課すこととする：

公理（強い健全性）
任意の可証降下列配列\((\Theta,k,\Phi)\)に対し、以下が成り立つ： \(\Theta\)は整列であり、\(\Phi\)は全域である。任意の\(m_0,m_1 \in \mathbb{N}\)に対し、以下が成り立つ： \(m_0 \neq \textrm{Output}_{\Phi}(m_0,m_1)\)ならば、\(\textrm{Output}_{\Theta}(m_0,\textrm{Output}_{\Phi}(m_0,m_1)) = 0\)である。 \(m_0 = \textrm{Output}_{\Phi}(m_0,m_1)\)ならば、任意の\(m_2 \in \mathbb{N}\)に対し\(\textrm{Output}_{\Theta}(m_0,m_2) = 1\)である。

強い健全性は可証整列性と整列性の関係を一般化した公理だが、例えば\(\textrm{ZFC}\)集合論の\(\omega\)無矛盾性を公理に課せば\(\Theta\)の整列性を弱めた「\(\textrm{Out}_{\Theta}^{\textrm{N}^2}\)は\(\mathbb{N}\)上の全順序であって、かつ\(\textrm{Out}_{\Theta}^{\textrm{N}^2}\)の無限降下列を定める計算可能数列は存在しない」ということが従うように思うので、さほど病的な公理ではないと考えられる。なお今回は再帰的整列順序の形式化を用いたので整列性に関する強い健全性を課す必要があったが、代わりに基本列の形式化を用いる場合は基本列の停止性に関する健全性を課すだけで十分となるので、強い健全性ではなく単に\(\omega\)無矛盾性を課すだけで良くなる。一方でその場合は後で定義する\(O\)という順序数への対応がill-definedになるため順序数に対するFGHではうまく下から評価できなくなるという不利益がある。つまり再帰的整列順序と基本列のどちらの形式化を使うほうがより巨大関数として良いものになるかは、評価において仮定の少なさと結果の綺麗さを重視するか、の問題である。

\(T\)に強い健全性を公理として追加した体系を\(T'\)と置く。

\(a\)を降下列配列とする。順序数\(o(a)\)を以下のように定める：

\((\Theta,k,\Phi) = a\)と置く。
\(a = a_{\omega}^{k}\)ならば、\(o(a) = 1+k\)である。
\(a \neq a_{\omega}^{k}\)とする。
1. \(a\)が可証でないならば、\(o(a) = \omega\)である。
2. \(a\)が可証であるとする。
  1. 強い健全性より\(\Theta\)は整列である。
  2. 以下を満たす最小の部分集合を\(\Sigma_a \subset \mathbb{N}\)と定める：
    1. \(k \in \Sigma_a\)である。
    2. いかなる\(k' \in \Sigma_a\)と\(n \in \mathbb{N}\)に対しても\(\textrm{Output}_{\Phi}(k',n) \in \Sigma_a\)である。
  3. \(\textrm{Output}_{\Theta}^{\mathbb{N}^2}\)の定める\(\mathbb{N}\)上の整列順序の\(\Sigma_a\)への制限の順序数型を\(\alpha\)と置く。
  4. \(o(a) = \omega + \alpha\)である。

定義から\(o(a)\)は\(\textrm{PTO}(\textrm{ZFC})\)未満の順序数である。

\(A\)を順序数配列とする。順序数\(O(A)\)を以下のように定める；

\(L = \textrm{Lng}(A)\)と置く。
\(L = 0\)ならば、\(O(A) = 0\)である。
\(L > 0\)ならば、\(O(A) = O((A_i)_{i=0}^{L-2}) + o(A_{L-1})\)である。

\(o\)の性質から\(O(A)\)は\(\textrm{PTO}(\textrm{ZFC})\)未満の順序数である。ただし\(o\)や\(O\)は単射ではなく非常に複雑であり、また計算可能関数のように算術で記述できるものですらない。

さて、降下列の定義からいかなる順序数配列\(A\)と\(n \in \mathbb{N}\)に対しても\(O(A[n]) \in O(A)\)である。従って順序数の整礎性から、\(T'\)において\(\mathcal{F}\)の全域性が証明可能である。特に以下が従う：

定理（限界関数の全域性）
\(\textrm{Lim}\)と\(\textrm{LIM}\)の全域性は\(T'\)で証明可能である^[21]。

\(O\)の定義から\((O(A_{\textrm{Lim}}^{n}))_{n=0}^{\infty}\)は狭義単調増大列であり、上の議論からその極限は\(\textrm{PTO}(\textrm{ZFC})\)となる。\(\textrm{PTO}(\textrm{ZFC}) + 2\)の基本列系 \begin{eqnarray*} S \colon (\textrm{PTO}(\textrm{ZFC}) + 2) \times \mathbb{N} & \to & \textrm{PTO}(\textrm{ZFC}) + 1 \\ (\beta,n) & \mapsto & S(\beta,n) \end{eqnarray*} を以下のように定める：

\(\beta = \textrm{PTO}(\textrm{ZFC}) + 1\)ならば、\(S(\beta,n) = \textrm{PTO}(\textrm{ZFC})\)である。
\(\beta = \textrm{PTO}(\textrm{ZFC})\)ならば、\(S(\beta,n) = O(A_{\textrm{Lim}}^{n})\)である。
\(\beta \in \textrm{PTO}(\textrm{ZFC})\)とする。
1. 順序数の整礎性から、以下を満たす\(m \in \mathbb{N}\)がただ１つ存在する：
  1. \(O(A_{\textrm{Lim}}^{m}) \notin \beta\)である。
  2. 任意の\(h \in \mathbb{N}\)に対し、\(h < m\)ならば\(O(A_{\textrm{Lim}}^{h}) \in \beta\)である。
2. \(m = 0\)ならば、\(S(\beta,n) = 0\)である。
3. \(m > 0\)とする。
4. \(O(A_{\textrm{Lim}}^{m-1}) + 1 = \beta\)ならば、\(S(\beta,n) = O(A_{\textrm{Lim}}^{m-1})\)である。
5. \(O(A_{\textrm{Lim}}^{m-1}) + 1 \in \beta\)とする。
  1. \(a = \textrm{EnumNestArray}(m)\)と置く。
  2. \(O(A_{\textrm{Lim}}^{m-1}) + 1 \in \beta\)より、順序数の整礎性と加法の右連続性から\(O(A_{\textrm{Lim}}^{m-1}) + 1 + \gamma = \beta\)を満たす順序数\(\gamma\)がただ１つ存在する。
  3. \(\gamma \in \omega\)ならば、\(S(\beta,n) = O(A_{\textrm{Lim}}^{m-1}) + \gamma\)である。
  4. \(\gamma \notin \omega\)とする。
    1. \(a\)が降下列配列でないならば、\(O(A_{\textrm{Lim}}^{m-1}) \in O(A_{\textrm{Lim}}^{m-1}) + 1 + m = O(A_{\textrm{Lim}}^{m-1}) + o(a_{\omega}^{m}) = O(A_{\textrm{Lim}}^{m})\)であるので、\(\gamma \in m+1 \in \omega\)となり矛盾する。従って\(a\)は降下列配列である。
    2. \(a\)が可証でないならば、\(O(A_{\textrm{Lim}}^{m-1}) \in O(A_{\textrm{Lim}}^{m-1}) + \omega = O(A_{\textrm{Lim}}^{m-1}) + o(a) = O(A_{\textrm{Lim}}^{m})\)であるので、\(\gamma \in \omega\)となり矛盾する。従って\(a\)は可証である。
    3. \((\Theta,k,\Phi) = a\)と置く。
    4. 強い健全性より\(\Theta\)は整列である。\(\textrm{Output}_{\Theta}^{\mathbb{N}^2}\)の定める\(\mathbb{N}\)上の整列順序\(\textrm{Output}_{\Theta}^{\mathbb{N}^2}\)の\(\Sigma_a\)への制限の順序数型を\(\alpha\)と置く。
    5. \(O(A_{\textrm{Lim}}^{m-1}) + 1 + \gamma = \beta \subset O(A_{\textrm{Lim}}^{m}) = O(A_{\textrm{Lim}}^{m-1}) + o(a)\)かつ\(\gamma \notin \omega\)より\(\omega \in 1 + \gamma \subset o(a) = \omega + \alpha\)であるので、\(1 + \gamma = \omega + \delta\)を満たす\(\alpha\)以下の順序数\(\delta\)がただ１つ存在する。\(\delta \subset \alpha\)より、\(\textrm{Output}_{\Theta}^{\mathbb{N}^2}\)の切片\(\{h \in \Sigma_a \mid \textrm{Output}_{\Theta}^{\mathbb{N}^2}(h,i) = 1\}\)への制限の順序数型が\(\delta\)であるような\(i \in \Sigma_a\)がただ１つ存在する。
    6. \(\textrm{Output}_{\Theta}^{\mathbb{N}^2}\)の切片\(\{h \in \Sigma_a \mid \textrm{Output}_{\Theta}^{\mathbb{N}^2}(h,\textrm{Output}_{\Phi}(i,n)) = 1\}\)への制限の順序数型を\(\epsilon\)と置く。
    7. \(S(\beta,n) = O(A_{\textrm{Lim}}^{m-1}) + \omega + \epsilon\)である。

この基本列系を用いることで、限界関数をFGHで厳密に評価することが可能となる。

定理（限界関数のFGHによる記述）
\(S\)に伴うFGHに関して、\(T'\)で以下が証明可能である： \(\textrm{Lim} = f_{\textrm{PTO}(\textrm{ZFC})}\)である。 \(\textrm{LIM} = f_{\textrm{PTO}(\textrm{ZFC})+1}\)である。

証明：: いかなる\(n \in \mathbb{N}\)に対しても\(\textrm{PTO}(\textrm{ZFC})[n] = O(A_{\textrm{Lim}}^{n})\)であるので、\(\textrm{Lim}(n) = \langle (A_{\textrm{Lim}}^{n}), n \rangle\)かつ\(f_{\textrm{PTO}(\textrm{ZFC})}(n) = f_{\textrm{PTO}(\textrm{ZFC})[n]}(n) = f_{O(A_{\textrm{Lim}}^{n})}(n)\)である。従っていかなる\(n \in \mathbb{N}\)に対しても\(\langle (A_{\textrm{Lim}}^{n}), n \rangle = f_{O(A_{\textrm{Lim}}^{n})}(n)\)となることを示せば良い。そのためにはいかなる\(m \in \mathbb{N}^{< \omega}\)に対しても\(O((A_{\textrm{Lim}}^{n})[m]) = O((A_{\textrm{Lim}}^{n}))[m]\)が成り立つことを示せば良い。ただし\([m]\)は\(L = \textrm{Lng}(m)\)と置いた時の演算子の配列\(([m_i])_{i=0}^{L-1}\)の左結合的適用を表す。このことは\(S\)の定義から\(L\)に関する帰納法より即座に従う。□

限界関数のFGHによる記述の証明において重要なことは、一般の順序数項に対して定義した降下列が\(O\)を通じて実際に基本列とみなせることである。また順序数配列全体においては\(O\)が単射ではなかったが、標準形順序数配列のみからなる部分集合\(OT\)に\(O\)を制限したものは単射となる。ただし標準形順序数配列に対する大小関係には特に原始再帰的翻訳を与えていないので、これは通常の意味での順序数表記でない。あくまで、集合論の中で定義される\(O\)という写像を用いて大小関係が定義されるだけである。また\(OT\)に備わっている降下列系が実際に基本列をなすことは、やはり\(O\)を通じて初めて言えることなので、\(O\)を定義するために\(T'\)を用いたことから通常の\(\textrm{ZFC}\)公理系で言えるわけではないことにも注意が必要である。

脚注[]

↑ 集合論の言葉で表すと、「長さ\(n\)の配列」とは\(n\)を定義域とする写像のことです。また写像の定義には「グラフと終域の組」を使うものと「グラフそのもの」を使うものの２通りの流儀があり前者の方が主流と推測していますが、空列を終域によらず同じ記号\(()\)で表したい都合、後者の流儀を採用します。
↑ 集合論の言葉で表すと、\(0\)すなわち\(\emptyset\)を定義域とする写像のことです。
↑ つまり\(\bigcup_{n \in \mathbb{N}} S^n\)のことです。
↑ 集合論の言葉で表すと配列は写像なので、\(a_i\)とは単に\(a(i)\)のことです。
↑ \((a)_i\)とすると\(a\)と\((a)\)のどちらを考えているのかが紛らわしいです。
↑ つまり\(L = \textrm{Lng}(a)\)と置くと\(\textrm{Last}(a) = a_{L-1} \in S\)です。
↑ ちなみにコード行列としては\(2,3\)行目が\(0,1\)のみからなるもの以外考える必要がないのですが、考えても問題はないので記述を簡単にするためにそのような制約は課しません。
↑ 既存の計算モデルとして名前がついているかもしれませんが、知らないのでご存知の人は教えて下さい。
↑ \(P_2 > x\)の場合は直接的な翻訳がありませんが、\(P_2 \leq x\)である状態から何回\(\textrm{App}\)を適用しても\(P_2 > x\)にならないため、少なくとも今回の巨大数の定義では全く気にしなくて良いです。
↑ つまり自然数\(n_0,n_1\)に対し、\(n_0 \leq n_1\)ならば\(\textrm{Output}_{\Theta_{\omega}}^{\mathbb{N}^2}(n_0,n_1) = 1\)となり、\(n_0 > n_1\)ならば\(\textrm{Output}_{\Theta_{\omega}}^{\mathbb{N}^2}(n_0,n_1) = 0\)となるということです。
↑ 以下の等式の左辺は１つの記号ではありませんが、左辺の文字列をまるごと右辺の入れ子配列の略記とするということです。以下も同様の略記を導入します。
↑ 最終的には\(\textrm{Ax}(a)\)が斧配列であるもの以外は必要ないのですが、設計図配列という概念自体はその再帰的定義の仕方からそのような制約が課されていないものも考える必要があります。
↑ 数式環境を３つに分けないと何故か正しく出力されませんでした。数式環境にも行数の制限があるのでしょうか？
↑ 限界関数を定める際に使う「表記の限界を表す列」の隣り合う項が降下列の繰り返しによって到達可能であるという意味です。例えばクリーネの\(O\)表記は、それに元々備わっている基本列構造に関してはこれを満たしませんが、順序数への対応を用いて定義し直した基本列に関してはこれを満たします。従ってFGHを考えてその限界関数を定める場合は、前者だと\(\omega_1^{\textrm{CK}}\)未満のFGHを対角化しただけのものになりますが、後者だときっちり\(\omega_1^{\textrm{CK}}\)に対してFGHを考えたものになります。
↑ 略して「巨大数屋敷数」です。
↑ \(A \neq 0 = ()\)であるので、\(L > 0\)となります。
↑ \(\langle ((a)), n \rangle\)の計算の各ステップにおける変数（ここでは急増加関数配列と自然数）を並べた配列に\(\ulcorner \ \urcorner\)を適用したものが\(\langle ((\ulcorner a \urcorner)), \ulcorner n \urcorner \rangle\)の計算の各ステップにおける変数を並べた配列となることが\(T\)で証明可能となるからです。実際、各ステップで\(\mathcal{F}\)の定義式の条件を満たすことが\(T\)で証明可能であり、ステップ数のメタな有限性からその証明を並べたものが\(T\)での証明を与えます。
↑ 実際に証明可能でないのかどうかを調べるのは面倒くさそうなので特に考えていません。
↑ 巨大基数の可算崩壊自体は巨大基数公理が必要ですが、\(\textrm{ZFC}\)公理系で議論し直す時は巨大基数の「再帰的類似」と呼ばれる非再帰的可算順序数のある崩壊で得られる再帰的順序数（これは\(\textrm{ZFC}\)公理系で定義できる）であって、巨大基数公理の下では巨大基数の可算崩壊と一致することが証明可能であるものを使います。
↑ 深くは考えていません。
↑ \(\textrm{Lim}\)は理論\(T\)を対角化して構成したものであり\(T'\)を対角化して構成したものではないことに気を付けましょう。

[1] 集合論の言葉で表すと、「長さ\(n\)の配列」とは\(n\)を定義域とする写像のことです。また写像の定義には「グラフと終域の組」を使うものと「グラフそのもの」を使うものの２通りの流儀があり前者の方が主流と推測していますが、空列を終域によらず同じ記号\(()\)で表したい都合、後者の流儀を採用します。

[2] 集合論の言葉で表すと、\(0\)すなわち\(\emptyset\)を定義域とする写像のことです。

[3] つまり\(\bigcup_{n \in \mathbb{N}} S^n\)のことです。

[4] 集合論の言葉で表すと配列は写像なので、\(a_i\)とは単に\(a(i)\)のことです。

[5] \((a)_i\)とすると\(a\)と\((a)\)のどちらを考えているのかが紛らわしいです。

[6] つまり\(L = \textrm{Lng}(a)\)と置くと\(\textrm{Last}(a) = a_{L-1} \in S\)です。

[7] ちなみにコード行列としては\(2,3\)行目が\(0,1\)のみからなるもの以外考える必要がないのですが、考えても問題はないので記述を簡単にするためにそのような制約は課しません。

[8] 既存の計算モデルとして名前がついているかもしれませんが、知らないのでご存知の人は教えて下さい。

[9] \(P_2 > x\)の場合は直接的な翻訳がありませんが、\(P_2 \leq x\)である状態から何回\(\textrm{App}\)を適用しても\(P_2 > x\)にならないため、少なくとも今回の巨大数の定義では全く気にしなくて良いです。

[10] つまり自然数\(n_0,n_1\)に対し、\(n_0 \leq n_1\)ならば\(\textrm{Output}_{\Theta_{\omega}}^{\mathbb{N}^2}(n_0,n_1) = 1\)となり、\(n_0 > n_1\)ならば\(\textrm{Output}_{\Theta_{\omega}}^{\mathbb{N}^2}(n_0,n_1) = 0\)となるということです。

[11] 以下の等式の左辺は１つの記号ではありませんが、左辺の文字列をまるごと右辺の入れ子配列の略記とするということです。以下も同様の略記を導入します。

[12] 最終的には\(\textrm{Ax}(a)\)が斧配列であるもの以外は必要ないのですが、設計図配列という概念自体はその再帰的定義の仕方からそのような制約が課されていないものも考える必要があります。

[13] 数式環境を３つに分けないと何故か正しく出力されませんでした。数式環境にも行数の制限があるのでしょうか？

[14] 限界関数を定める際に使う「表記の限界を表す列」の隣り合う項が降下列の繰り返しによって到達可能であるという意味です。例えばクリーネの\(O\)表記は、それに元々備わっている基本列構造に関してはこれを満たしませんが、順序数への対応を用いて定義し直した基本列に関してはこれを満たします。従ってFGHを考えてその限界関数を定める場合は、前者だと\(\omega_1^{\textrm{CK}}\)未満のFGHを対角化しただけのものになりますが、後者だときっちり\(\omega_1^{\textrm{CK}}\)に対してFGHを考えたものになります。

[15] 略して「巨大数屋敷数」です。

[16] \(A \neq 0 = ()\)であるので、\(L > 0\)となります。

[17] \(\langle ((a)), n \rangle\)の計算の各ステップにおける変数（ここでは急増加関数配列と自然数）を並べた配列に\(\ulcorner \ \urcorner\)を適用したものが\(\langle ((\ulcorner a \urcorner)), \ulcorner n \urcorner \rangle\)の計算の各ステップにおける変数を並べた配列となることが\(T\)で証明可能となるからです。実際、各ステップで\(\mathcal{F}\)の定義式の条件を満たすことが\(T\)で証明可能であり、ステップ数のメタな有限性からその証明を並べたものが\(T\)での証明を与えます。

[18] 実際に証明可能でないのかどうかを調べるのは面倒くさそうなので特に考えていません。

[19] 巨大基数の可算崩壊自体は巨大基数公理が必要ですが、\(\textrm{ZFC}\)公理系で議論し直す時は巨大基数の「再帰的類似」と呼ばれる非再帰的可算順序数のある崩壊で得られる再帰的順序数（これは\(\textrm{ZFC}\)公理系で定義できる）であって、巨大基数公理の下では巨大基数の可算崩壊と一致することが証明可能であるものを使います。

[20] 深くは考えていません。

[21] \(\textrm{Lim}\)は理論\(T\)を対角化して構成したものであり\(T'\)を対角化して構成したものではないことに気を付けましょう。

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

PTO(ZFC)を超えたFGH

目次

はじめに[]

注意[]

PTO(ZFC)[]

表記系[]

あらすじ[]

チューリングマシンの対角化[]

記法と用語[]

実装[]

停止性[]

例[]

ZFC集合論の形式化[]

入れ子配列[]

略記[]

項配列[]

屋敷配列[]

代入[]

斧配列[]

設計図配列[]

チューリングマシンの形式化[]

Sepの形式化[]

Cmbの形式化[]

Appの形式化[]

停止性の形式化[]

Outputの形式化[]

再帰的整列順序の形式化[]

降下列の形式化[]

巨大数の構成[]

降下列[]

FGH[]

限界関数[]

命名[]

解析[]

メタ理論[]

可証性[]

停止性[]

評価[]

脚注[]