超越整数観察日記

Mathematical Logic Advent Calendar 2020の3日目投稿用の記事です。有名な巨大数の概念である超越整数についての概要とその拡張について解説します。巨大数について詳しくなくても自然演繹の基礎を知っていれば読める内容だと思います。ただし超越整数はシンプルな見た目の定義な割にそれが実際に（形式的に）意味するところを解釈するのはあまり簡単ではないので、１つ１つ用語を注意しながら解説していきます。

なお僕は数理論理学の教科書を読んだことがないので、複数の流儀が存在する色々な用語についてどういう流儀が主流なのかは知りません。なのでかなり自己流な流儀になっているかもしれませんが、流儀に幅のある部分はきちんと定義は書くようにするのでそれを念頭に置いて下さい。またなるべく証明を書いていますが議論が何かしら間違っていたらこの記事のコメントやtwitterで教えて下さると助かります。

定義

超越整数は数理論理学で有名な数学者Harvey Friedmanの考案した概念です。自然数\(n\)が超越整数であるとは、

任意のチューリングマシン\(M\)に対し、\(M\)の停止性が\(\textrm{ZFC}\)公理系で\(2^{1000}\)文字以下で証明可能ならば、\(M\)は\(n\)ステップ以内に停止する

ということです。特に\(n\)が超越整数ならば\(n\)以上の任意の自然数が超越整数となるので、最小の超越整数を考えることが自然となります。

さて、最小の超越整数が\(\textrm{ZFC}\)公理系においてwell-definedであるか否かを説明します。その前に、well-defined性に言及するためにはそもそも定義文を形式化する必要がありますので、それを固定するところから始めます。そのためにそもそも定義文とは何かについて復習しましょう。

定義文

定義文については微妙な流儀の幅がありますので、ここで導入する流儀はあくまで僕流の１つの流儀だということにご留意下さい。以前

• ユーザーブログ:P進大好きbot/形式論理のお勉強（その４）

で解説した定義文の流儀と変数の明示方法が変わっていますが趣旨はだいたい同じです。

\(L\)を\(1\)階述語論理の言語とし、\(f\)を\(L\)論理式とし、\(T\)を\(L\)論理式とします。\(f\)が\(T\)における定義文であるとは、\(L\)の変数記号\(x\)が存在して\(\exists ! x(f(x))\)が\(T\)で証明可能な閉論理式であるということです。特に\(\exists ! x(f(x))\)が閉であるという仮定からこのような\(x\)は定義文\(f\)に対し一意です。

\(T\)が矛盾する場合は自由変数を持つか否かに関係なく任意の論理式が爆発律により証明可能なので、自由変数を高々１つしか含まない任意の\(L\)論理式が\(T\)における定義文になります。一方で閉論理式を\(\exists ! x\)で量化した閉論理式は、\(T\)において領域がシングルトンでない（つまり\(\exists x(\exists y(x \neq y))\)が証明可能である）限り\(T\)で反証可能になるため、\(T\)が無矛盾であるならば定義文は閉論理式でなく、すなわち定義文には自由変数が常に一意に存在します。

例えば\(L\)が\(1\)階算術の言語、\(T\)がペアノ算術の公理系\(\textrm{PA}\)であるとします。\(x\)と\(y\)をメタに相異なる\(L\)の変数記号であるとすると、\(x = y\)や\(x =x \land y = 0\)は自由変数が一意でないので今回の流儀においては\(T\)の定義文となりませんし、\(\exists x(x = x)\)や\(\exists x(y = S(x))\)は\(T\)が無矛盾である限り\(T\)において定義文とはなりません。一方で\(x = 0\)や\(y \neq 0 \land \forall x(y \neq S(S(x)))\)は\(T\)における定義文となります。

それでは超越整数を形式化（概念の定義を論理式として解釈）し、その上で「最小の超越整数」という概念が\(\textrm{ZFC}\)公理系においてwell-definedである（つまり「自然数\(n\)が最小の超越整数である」という述語が形式的に論理式として解釈されそれが\(\textrm{ZFC}\)公理系において定義文となる）ことを説明します。

形式化

まず超越整数の定義を復習しましょう。自然数\(n\)が超越整数であるとは、任意のチューリングマシン\(M\)に対し、\(M\)の停止性が\(\textrm{ZFC}\)公理系で\(2^{1000}\)文字以下で証明可能ならば、\(M\)は\(n\)ステップ以内に停止するということです。

今回は最小の超越整数のwell-defined性を問うための公理系として\(\textrm{ZFC}\)公理系を考えています。すると\(\textrm{ZFC}\)公理系の中で更に「\(\textrm{ZFC}\)公理系において\(2^{1000}\)文字以下で証明可能」という自己言及的な文を考えているのでベリーのパラドックス を連想するかもしれません。しかし数理論理学においては自然数（もしくは適当な集合から具体的に構成される言語）を用いて論理式をコードする方法（ゲーデル対応）が知られており、「～において証明可能」などの文字列操作に関する基本的な言明は自然数などに関する論理式として解釈するという暗黙の了解があります。このようにメタな概念を自然に論理の中に（項や定義文として）落とし込んで議論することをここでは大雑把に「形式化」と呼ぶことにします。

ゲーデル対応の方法は一意でなくゲーデル対応次第で微妙に性質が違ったりすることはあるので「ゲーデル対応の方法をきっちり１つに固定してくれないと困る」という人もいると思いますので、そういう人は僕が具体的に構成した

• ユーザーブログ:P進大好きbot/PTO(ZFC)を超えたFGH#ZFC集合論の形式化（\(\textrm{ZFC}\)公理系をHenkin拡大した体系を配列の入れ子により形式化した理論\(\textrm{AxArray}\)）
• ユーザーブログ:P進大好きbot/高階集合論を超えた1階述語論理#形式言語（\(\textrm{ZFC}\)公理系に余計な定数記号・関数記号・関係記号を添加した体系を可算順序数により形式化した理論\(\textrm{ZFC}_{\ulcorner L \urcorner}\)）

のどちらかの部分体系とそれに対応する言語とゲーデル対応を使って下さい。今\(\textrm{ZFC}\)公理系が２種類用いられていて少し紛らわしいので、最小の超越整数のwell-defined性を問うための公理系である\(\textrm{ZFC}\)公理系を\(MT\)と置きその言語を\(ML\)と置き、\(MT\)の中でゲーデル対応を用いて形式化された\(\textrm{ZFC}\)公理系を\(T\)と置きその言語を\(L\)と置くことにします。つまり\(MT\)においては\(L\)論理式の\(T\)における証明可能性（および\(2^{1000}\)文字以内での証明可能性）が形式化できているわけです。具体的には論理式や証明という概念がゲーデル対応によりゲーデル数と呼ばれる自然数として形式化され、与えられた自然数\(n\)が\(T\)における論理式や証明のゲーデル数であるという述語が意味を持ち、論理式の証明可能性はその証明のゲーデル数であるような自然数の存在として形式化されます。

さて、まだ終わりではありません。何故なら自然数\(n\)が超越整数であることの定義を\(T\)を用いて書き直すと、

任意のチューリングマシン\(M\)に対し、\(M\)の停止性が\(T\)で\(2^{1000}\)文字以下で証明可能ならば

という言明が含まれるわけですが、\(MT\)の項である\(M\)は\(L\)に属さないため、「\(M\)の停止性」がそのままでは\(L\)論理式にならず、\(T\)における\(2^{1000}\)文字以下での証明可能性に直接意味がないからです。数理論理学においては\(MT\)の項である自然数\(n\)を形式化して\(T\)の項である自然数\(\ulcorner n \urcorner\)を構成する方法が知られており、かつチューリングマシンであって状態と字母が自然数であるものを自然数に単射に対応させる方法（コード化）が知られています。これらを組み合わせることで、\(MT\)の項である任意のチューリングマシン\(M\)であって状態と字母が自然数であるものはまず\(MT\)の項である自然数にコード化され、そのコードは形式化により\(T\)の項である自然数に対応し、その自然数は\(T\)の項であるチューリングマシン\(\ulcorner M \urcorner\)であって状態と字母が自然数であるもののコードであることが\(T\)で証明可能であることが\(MT\)で証明可能となります。これにより、「チューリングマシン\(M\)の停止性が～において…文字以下で証明可能」などの停止性に関する基本的な言明は自然数などに関する論理式として解釈するという暗黙の了解があります。

「任意のチューリングマシンを考えているはずなのに状態と字母が自然数であるものしかコード化していないのは問題ではないか」と思うかもしれませんが任意のチューリングマシンは状態と字母が自然数であるであるチューリングマシンと等価である（停止性が同値で停止する場合の停止ステップ数が等しく出力も一致する）ので、こういう形式化の文脈で「任意のチューリングマシン」と言った時は暗黙に「状態と字母が自然数である任意のチューリングマシン」に置き換えて解釈します。ここでも以下「状態と字母が自然数であるチューリングマシン」は長いので常に「チューリングマシン」と書くことにします。

チューリングマシンのコード化の方法は一意でなくコード化次第で微妙に性質が違ったりすることはあるので「コード化の方法をきっちり１つに固定してくれないと困る」という人もいると思います。そういう人は僕が具体的に構成した

• ユーザーブログ:P進大好きbot/PTO(ZFC)を超えたFGH#チューリングマシンの形式化（チューリング完全な計算モデルを行列ベースの言語で形式化したもの）

を代わりに使って下さい。プログラミング言語で例えるとコード化という操作は、各文字を予め相異なる正整数に対応させておいてそれを用いてプログラミング言語の関数の定義となるソースコードである文字列を正整数列に変換するようなものですね。

以上で、超越整数という概念の定義に用いる諸概念の形式化が終わりました。これにて「自然数\(n\)は超越整数である」という述語が\(MT\)の中で（つまり\(ML\)論理式として）

任意のチューリングマシン\(M\)に対し、\(\ulcorner M \urcorner\)の停止性が\(T\)で\(2^{1000}\)文字以下で証明可能であるならば、\(M\)は\(n\)ステップ以内で停止する

と定式化できました。これを満たす\(n \in \mathbb{N}\)の最小値が最小の超越整数というわけです。

Well-defined性

それでは「自然数\(n\)は最小の超越整数である」という述語に対応する\(ML\)論理式を\(\textrm{IsMinTransInt}(n)\)と置きます。最小の超越整数が\(MT\)でwell-definedであること、すなわち\(ML\)論理式\(\exists ! n \in \mathbb{N}(\textrm{IsMinTransInt}(n))\)が\(MT\)における定義文であることを確認します。

まず\(L\)は\(\textrm{ZFC}\)公理系の言語なので、定数記号や関数記号を持たず、関係記号も\(\in\)のみ（もしくは\(\in\)と\(=\)のみ）です。従って、\(2^{1000}\)文字以下の\(L\)論理式は変数の書き換えの差を除けば高々有限個しか存在しません。そのため、\(T\)で\(2^{1000}\)文字以下で証明可能な\(L\)論理式も高々有限個しか存在しません。従って、\(T\)で\(2^{1000}\)文字以下で停止性が証明可能なチューリングマシン\(M\)全体の集合\(S\)は、\(MT\)において定義される有限集合です。

すると「\(S\)の各元は\(\textrm{ZFC}\)公理系で停止性が示せるから有限ステップで停止して」と言いたいところですがそれは議論が飛躍しています。\(MT\)の項であるチューリングマシン\(M\)に対し、「\(M\)が停止する」という\(ML\)論理式と「\(T\)で\(\ulcorner M \urcorner\)の停止性が証明可能である」という\(ML\)論理式は同じ論理式ではないので、それらの関係を明確にする必要があります。実際、

任意のチューリングマシン\(M\)に対し、\(\ulcorner M \urcorner\)の停止性が\(T\)で証明可能ならば、\(M\)は停止する

という\(ML\)論理式は\(T\)の\(\Sigma_1\)健全性と呼ばれる非自明なものです。それどころか\(T\)の\(\Sigma_1\)健全性は\(T\)の無矛盾性（つまり\(\textrm{Con}(T)\)）を含意するため、ゲーデルの不完全性定理により\(MT\)が無矛盾であるならば\(MT\)は\(T\)の\(\Sigma_1\)健全性が証明可能ではありません。

ここで役に立つのが、「\(2^{1000}\)文字以下」という制限です。\(T\)の\(\Sigma_1\)健全性

任意のチューリングマシン\(M\)に対し、\(\ulcorner M \urcorner\)の停止性が\(T\)で証明可能ならば、\(M\)は停止する

が\(MT\)で証明できなかったとしても、それより弱い\(ML\)論理式

任意のチューリングマシン\(M\)に対し、\(\ulcorner M \urcorner\)の停止性が\(T\)で\(2^{1000}\)文字以下で証明可能ならば、\(M\)は停止する

なら実は\(MT\)で証明可能であることが「メタに証明可能」となるのです。ここで「メタに証明可能」と書きましたが、これは\(MT\)にとっての更なるメタ理論で証明可能であるということです。\(T\)がメタ理論\(MT\)を持っていたのと同様に\(MT\)も（病的に弱すぎない）メタ理論\(MMT\)を持つと考えて、

「任意のチューリングマシン\(M\)に対し、\(\ulcorner M \urcorner\)の停止性が\(T\)で\(2^{1000}\)文字以下で証明可能ならば、\(M\)は停止する」という\(ML\)論理式の\(MT\)での証明可能性

を\(MMT\)で証明できる、というわけです。実際に証明してみましょう。

まず\(MMT\)において「\(MT\)における\(2^{1000}\)文字以下の証明のゲーデル数全体の集合」を\(X\)と置くと、\(X\)が有限集合であるということを（\(MMT\)が病的に弱すぎなければ）\(MMT\)は証明可能です。\(MT\)の項であるチューリングマシンが形式化によって\(T\)の項であるチューリングマシンに対応させられたことと同様に、\(MMT\)の項である自然数が形式化によって\(T\)の項である自然数に対応させられます。特に\(X\)の有限性から、\(X\)に属するゲーデル数を列挙して\(n_0, \ldots, n_k\)（\(k\)は\(MMT\)の項である自然数）と置きそれらの形式化である\(MT\)の項であるゲーデル数も同じ記号で書くことにすれば

自然数\(n\)は、\(n = n_0\)または……または\(n = n_k\)である

という（有限長の）述語\(P_X(n)\)を\(MT\)の中で（つまり\(ML\)論理式として）定義することが出来ます。この述語\(P_X(n)\)はその構成から

自然数\(n\)は\(T\)における\(2^{1000}\)文字以下の証明のゲーデル数である

という\(ML\)論理式と同値であることが\(MT\)において証明可能となります。

というわけで、

任意のチューリングマシン\(M\)に対し、\(\ulcorner M \urcorner\)の停止性が\(T\)で\(2^{1000}\)文字以下で証明可能であるならば、\(M\)は停止する

という\(ML\)論理式が

任意のチューリングマシン\(M\)に対し、ある\(n \in \mathbb{N}\)が存在して『\(n = n_0\)または……または\(n = n_k\)』かつ『\(n\)は\(\ulcorner M \urcorner\)の停止性の証明のゲーデル数』であるならば、\(M\)は停止する

という\(ML\)論理式と同値であることが\(MT\)で証明可能であるということが\(MMT\)で証明可能になります。この\(MT\)での証明が実際に手や計算機で書き下せればより良いのですが、後者の\(ML\)論理式自体がものすごく長く、書き下そうにも恐らく観測可能宇宙に存在する粒子を全てインクに変えてもインクが足りないと推測されます。仕方ないので、\(MT\)での証明可能性はあくまで\(MMT\)で証明可能である、という主張となります。いくら有限の証明とはいえ、現実的に書き下せないのですから仕方ありません。

以上より

「任意のチューリングマシン\(M\)に対し、ある\(n \in \mathbb{N}\)が存在して『\(n = n_0\)または……または\(n = n_k\)』かつ『\(n\)は\(\ulcorner M \urcorner\)の停止性の証明のゲーデル数』であるならば、\(M\)は停止する」という\(ML\)論理式が\(MT\)で証明可能である

ということが\(MMT\)で証明可能であれば良いことが分かりました。そのためには単純な場合分けにより、\(MMT\)の項である\(k\)以下の各自然数\(i\)に対し

「任意のチューリングマシン\(M\)に対し、\(n_i\)が\(\ulcorner M \urcorner\)の停止性の\(T\)における証明のゲーデル数であるならば、\(M\)は停止する」という\(ML\)論理式が\(MT\)で証明可能である

ということが\(MMT\)で証明可能であれば良いです。ここで、

\(n_i\)が\(\ulcorner M_i \urcorner\)の停止性の\(MT\)における証明のゲーデル数であるようなチューリングマシン\(M_i\)が存在する

が成り立つか否かで\(MMT\)において場合分けをしましょう。

そのような\(M_i\)が存在すると仮定すると、\(MMT\)の項であるチューリングマシン\(M_i\)の形式化として得られる\(MT\)の項であるチューリングマシンを同じく\(M_i\)と書くことにすると、

「任意のチューリングマシン\(M\)に対し、\(n_i\)が\(\ulcorner M \urcorner\)の停止性の\(T\)における証明のゲーデル数であるならば、\(M = M_i\)である」という\(ML\)論理式が\(MT\)において証明可能である

ということが\(MMT\)において証明可能ですが、\(M_i\)が停止することの\(MT\)における証明は既にゲーデル数\(n_i\)に対応するものとして与えられているので、

「任意のチューリングマシン\(M\)に対し、\(n_i\)が\(\ulcorner M \urcorner\)の停止性の証明のゲーデル数であるならば、\(M\)は停止する」という\(ML\)論理式が\(MT\)において証明可能である

ということが\(MMT\)において証明可能となります。

逆にそのような\(M_i\)が存在しないとすると、ゲーデル数\(n_i\)に対応する証明の末尾（つまりそれが\(MT\)において証明する\(ML\)論理式）はチューリングマシンの停止性ではない\(ML\)論理式となり、そのゲーデル数を\(m_i\)と置くと、\(MMT\)の項である自然数\(m_i\)の形式化として得られる\(MT\)の項である自然数\(\ulcorner m_i \urcorner\)はチューリングマシンの停止性ではない\(L\)論理式のゲーデル数となり、かつ\(MMT\)の項である自然数\(n_i\)の形式化として得られる\(MT\)の項である自然数\(\ulcorner n_i \urcorner\)は\(T\)における証明のゲーデル数でありその証明の末尾（つまりそれが\(T\)において証明する\(L\)論理式）のゲーデル数は\(\ulcorner m_i \urcorner\)と一致するため、\(\ulcorner n_i \urcorner\)はチューリングマシンの停止性の証明のゲーデル数ではないことになり、従って

「任意のチューリングマシン\(M\)に対し、\(n_i\)は\(\ulcorner M \urcorner\)の停止性の\(T\)における証明のゲーデル数でない」という\(ML\)論理式が\(MT\)において証明可能である

ということが\(MMT\)において証明可能となりますので

「任意のチューリングマシン\(M\)に対し、\(n_i\)が\(\ulcorner M \urcorner\)の停止性の証明のゲーデル数であるならば、\(M\)は停止する」という\(ML\)論理式が\(MT\)において証明可能である

ということが\(MMT\)において証明可能となります。

以上より、いずれの場合も

「任意のチューリングマシン\(M\)に対し、\(n_i\)が\(\ulcorner M \urcorner\)の停止性の証明のゲーデル数であるならば、\(M\)は停止する」という\(ML\)論理式が\(MT\)において証明可能である

ということが\(MMT\)において証明可能であることが分かりましたので、

「任意のチューリングマシン\(M\)に対し、\(\ulcorner M \urcorner\)の停止性が\(T\)で\(2^{1000}\)文字以下で証明可能であるならば、\(M\)は停止する」という\(ML\)論理式が\(MT\)において証明可能である

ということが\(MMT\)において証明可能です。以上より、\(ML\)論理式\(\exists ! n \in \mathbb{N}(\textrm{IsMinTransInt}(n))\)が\(MT\)における定義文となることが\(MMT\)において証明可能です。□

さて、以上で任意の\(M \in S\)に対し\(M\)が停止するということが分かったので、その停止ステップ数を\(\textrm{HaltTime}(M)\)と置きます。写像 \begin{eqnarray*} \textrm{HaltTime} \colon S \to \mathbb{N} \end{eqnarray*} は定義域\(S\)が有限集合であるので、その像は\(\mathbb{N}\)の有限部分集合となります。\(\mathbb{N}\)の有限部分集合が上限を持つことは\(MT\)において証明可能であり、それが最小の超越整数であることもまた定義から\(MT\)において証明可能です。以上より、最小の超越整数が\(MT\)においてwell-definedであることが分かりました。

既存の拡張

それでは最小の超越整数の拡張となる概念を紹介していきます。

関数化

まず自然に考えられる拡張は、最小の超越整数の定義におけるマジックナンバー\(2^{1000}\)を変数\(n\)に変えて関数とするものです。つまり部分写像 \begin{eqnarray*} \textrm{TransInt} \colon \mathbb{N} & \to & \mathbb{N} \\ n & \mapsto & \textrm{TransInt}(n) \end{eqnarray*} を「\(\ulcorner M \urcorner\)の停止性が\(T\)で\(n\)文字以下で証明可能であるチューリングマシン\(M\)の停止ステップ数の上限」と定めます。ここで「写像」ではなく「部分写像」と呼んでいるのは、定義域が\(\mathbb{N}\)の部分集合である写像という意味です。では実際の定義域はどう指定するのかと言うと、

\(\ulcorner M \urcorner\)の停止性が\(T\)で\(n\)文字以下で証明可能であるチューリングマシン\(M\)の停止ステップ数

全体の集合が有限であるような\(n \in \mathbb{N}\)全体の集合とします。こうして定まる部分写像\(\textrm{TransInt} \colon \mathbb{N} \to \mathbb{N}\)が計算可能部分関数であることは、万能チューリングマシンなどを使って容易に確認することが出来ます。

さて、\(\textrm{TransInt}\)が全域であること、つまり\(\textrm{TransInt}\)の定義域が\(\mathbb{N}\)全体と一致することが\(MT\)で示せるかどうかが気になりますね。\(MT\)の項である自然数\(n\)と計算可能部分関数\(f \colon \mathbb{N} \to \mathbb{N}\)（またはチューリングマシン等の計算モデル）に関する述語

\(n\)が\(f\)の定義域に属する

を\(f(n) \downarrow\)と書くことにすると、\(\textrm{TransInt}\)の全域性は

\(\forall n \in \mathbb{N}(\textrm{TransInt}(n) \downarrow)\)

という\(ML\)論理式になります。先程示したのは\(\textrm{TransInt}(2^{1000}) \downarrow\)が\(MT\)で証明可能であることですね。\(\textrm{TransInt}\)の全域性の\(MT\)における証明が仮に存在したとして、それを書き下すことは恐らく現実的に難しいので、\(MT\)における証明可能性を\(MMT\)の中で示せるかどうかを考えましょう。論理式で書くと

\(MMT \vdash MT \vdash \forall n \in \mathbb{N}(\textrm{TransInt}(n) \downarrow)\)

かどうかということです。これは\(MT\)が矛盾することを\(MMT\)が証明可能であれば当然成り立ちますが、そうでないならば難しいでしょう。もし\(MT\)が\(T\)の\(\Sigma_1\)健全性を示せることを\(MMT\)が示せるならばこれが成り立つことは\(2^{1000}\)に対する議論の大部分が簡潔になり一気に証明することが出来ますが、\(MMT\)が病的に弱すぎなければゲーデルの不完全性定理が成り立ってしまい、\(MT\)が矛盾することを\(MMT\)が証明可能でないならば\(MT\)が\(T\)の\(\Sigma_1\)健全性を示せないからです。ではこれよりもう少し弱い主張を考えましょう。

まず先程説明した\(\textrm{TransInt}(2^{1000}) \downarrow\)が\(MT\)で証明可能であることの\(MMT\)における証明ではマジックナンバー\(2^{1000}\)の性質は使いませんでした。実際、\(2^{1000}\)に限らず\(MMT\)の項である自然数\(n\)の形式化で得られる\(MT\)の項\(\ulcorner n \urcorner\)については\(\textrm{TransInt}(\ulcorner n \urcorner)\)が\(MT\)で証明可能であることが\(MMT\)で証明可能です。論理式で書くと、

\(MMT \vdash \forall n \in \mathbb{N}(MT \vdash \textrm{TransInt}(\ulcorner n \urcorner) \downarrow)\)

ということです。「全ての\(n \in \mathbb{N}\)に対して証明可能なんだったら全域でしょう？」と思うかもしれませんが、この論理式の\(n\)は\(MMT\)の項である自然数として量化されているだけで、\(MT\)において量化されているわけではありません。\(MT\)はあくまで\(MMT\)の中で形式化されているだけなので、その中の\(\mathbb{N}\)が"\(MMT\)の項である自然数の形式化で得られる自然数のみからなる"というわけではないです。そもそもこの言明自体\(ML\)論理式にすらならない非形式的なものです。

今回扱った２つの論理式

\(MMT \vdash MT \vdash \forall n \in \mathbb{N}(\textrm{TransInt}(n) \downarrow)\)

\(MMT \vdash \forall n \in \mathbb{N}(MT \vdash \textrm{TransInt}(\ulcorner n \urcorner) \downarrow)\)

を比べてみると、形式化\(\ulcorner \ \urcorner\)を無視すれば違うのは\(\forall n \in \mathbb{N}\)の位置（\(MMT\)と\(MT\)のどちらで量化子を考えているか）だけです。たったこれだけの違いでも成り立ちそうか否かがガラッと変わってしまうのは面白いですね。証明論的順序数と急増加関数を知っている人でしたら、\(\varepsilon_0 = \textrm{PTO}(\textrm{PA})\)を思い浮かべると分かりやすいかもしれません。底\(\omega\)のカントール標準形の基本列に関する\(f_{\varepsilon_0}\)を考えると、これは\(\textrm{PA}\)で全域性が証明可能ではありません。一方で各自然数\(n\)に対しては\(f_{\varepsilon_0}(n)\)が\(\varepsilon_0\)未満の順序数と同じ基本列に対応する急増加関数で表せ、その全域性は\(\textrm{PA}\)で証明可能であるため、結果的に\(f_{\varepsilon_0}(n)\)を計算する過程の停止性が\(\textrm{PA}\)で証明可能となります。今回は\(\textrm{PA}\)ではなく\(\textrm{ZFC}\)で同じようなことが起きているわけです。

TR関数

そこで\(\textrm{ZFC}\)よりもっと一般の理論を用いたらどうなるか、を考えたのがふぃっしゅさんのTR関数です。先程は\(T\)を（\(MT\)の中で形式化された）\(\textrm{ZFC}\)公理系としましたが、今回は算術を含む（病的に弱すぎはしない）一般の理論とし、部分写像 \begin{eqnarray*} \textrm{TR}(T,n) \colon \mathbb{N} & \to & \mathbb{N} \\ n & \mapsto & \textrm{TR}(T,n) \end{eqnarray*} を「\(\ulcorner M \urcorner\)の停止性が\(T\)で\(n\)文字以下で証明可能であるチューリングマシン\(M\)の停止ステップ数の上限」と定めます。つまり\(\textrm{TR}(\textrm{ZFC},n)\)が先程解説した\(\textrm{TransInt}(n)\)となるわけです。\(T\)の\(\Sigma_1\)健全性が\(MT\)で証明可能ならば\(\textrm{TR}(T,n)\)の全域性が\(MT\)で証明可能ですが、\(T\)が\(\textrm{ZFC}\)より真に強い場合は定義域がどうなるかすら不明です。何故なら、\(\textrm{TransInt}(\ulcorner n \urcorner) \downarrow\)が\(MT\)で証明可能であったのは\(T\)も\(MT\)も同じゲーデル対応で形式化された\(\textrm{ZFC}\)公理系だったことが非常に強く聞いており、例えば\(T\)が\(\textrm{ZFC}\)に到達不能基数の存在を追加した公理系の場合は\(T\)で\(n\)文字以下で\(\ulcorner M \urcorner\)の停止性が証明可能なチューリングマシン\(M\)が\(MT\)において実際に停止するかどうか不明となってしまいます。

なので\(\textrm{TR}(T,n)\)の定義域が十分広いことを期待しながら\(T\)を強めたい場合は、\(MT\)も一緒に強める必要があるわけです。そうなるともはや関数の値が定義される体系が\(\textrm{ZFC}\)公理系ですらなくなるので、\(\textrm{ZFC}\)公理系で自然数を定義して性質を調べたい人には少し不満かもしれません。それでもあまり公理の選択を気にしない人には魅力的な拡張となるでしょう。ふぃっしゅさんは\(T\)として特に\(\textrm{ZFC}\)公理系に階層内階層基数\(\textrm{I}0\)の存在を追加した公理系\(\textrm{ZFC}+\textrm{I}0\)を考えた\(\textrm{TR}(\textrm{ZFC}+\textrm{I}0,n)\)をΙ0関数と名付けました。

巨大数屋敷

巨大数屋敷は僕自身が定義したもので、停止性の証明可能なチューリングマシンを使うTR関数と違い、整礎性の証明可能な再帰的\(2\)項関係を使ったものです。巨大数屋敷はTR関数と違う以下の3点を売りとしています：

1. \(\textrm{TransInt}\)の直接的な拡張にはなっていない点
2. 計算アルゴリズムを書き下している点
3. 整礎\(2\)項関係を使っているため（順序数表記にはなりませんが）\(\textrm{PTO}(T)\)までの順序数に標準的に対応させられる点

なお元の定義では\(T\)が\(\textrm{ZFC}\)公理系の場合しか扱っていませんでしたが、英語版の概説記事ではTR関数と同様により一般の\(T\)で定義を説明しています。\(T\)が\(\textrm{ZFC}\)公理系の場合はやはり\(\textrm{TransInt}\)と同様の方法で\(2^{1000}\)などを代入した際の停止性（出力のwell-defined性）が\(MT\)において（\(MT\)を\(\textrm{ZFC}\)公理系より強めることなく）証明可能です。

\(\textrm{TransInt}\)はあまりに強く、例えば\(\textrm{ZFC}\)公理系で全域性が証明可能であるいかなる計算可能関数を支配することが分かります。そのため\(\textrm{ZFC}\)公理系の範疇で\(\textrm{TransInt}\)を超えるには\(\textrm{TransInt}\)を直接拡張する以外に道があまりないのですが、そこを別のアプローチで挑戦してみた感じです。実際に\(\textrm{TransInt}\)を超えているかどうかは分かりませんし超えたとしても\(\textrm{TransInt}\)のイテレーションで超えられてしまうとは思いますが、\(\textrm{TransInt}\)を直接拡張せずに超えられていればそれは１つの進歩となると考えています。

新しい拡張

やはり\(\textrm{TransInt}\)を超えているかどうか分からないことが巨大数屋敷の不満なところです。一方で\(T\)を強くするTR関数では\(MT\)を強くしない限り定義域が不明になってしまいます。いくらでも\(MT\)を強めて良いとしてしまうともはや公理をどう強めていくかだけの話になってしまうので、それはここではしないことにします。あくまで\(MT\)を\(\textrm{ZFC}\)公理系に固定して考えた時、どのように\(\textrm{TransInt}\)を超えていけるでしょうか？　今回は\(T\)を\(\textrm{ZFC}\)より強めながら、それでも\(MT\)を強めずに定義域をきちんと決定できるように工夫をしてみます。具体的には、\(MT\)の項である自然数\(n\)ごとに\(MT\)の中で形式化された\(\textrm{ZFC}\)公理系の拡大の列\((T_{n,m})_{m \in \mathbb{N}}\)を

\(MMT \vdash \forall n, m \in \mathbb{N}(MT \vdash TR(T_{\ulcorner n \urcorner,\ulcorner m \urcorner},\ulcorner n \urcorner) \downarrow)\)

を満たすように構成します。その構成は、ふぃっしゅさん考案の「既に得られている全域関数に対するオラクルを組み込んで関数のクラスを広げていく」ふぃっしゅ数バージョン4と似通っていて、「各点でのwell-defined性が既に保証された計算可能関数に対する全域性を公理として組み込んで関数のクラスを広げていく」という流れです。つまり今回定義しようとしている関数は、ふぃっしゅさんの代表作品であるふぃっしゅ数バージョン4とTR関数を組み合わせたような関数となっています。もちろんふぃっしゅ数バージョン4と違いオラクル等は用いないので、きちんと計算可能な関数が得られることに注意しましょう。

公理系の族

とりあえず後で\(MT\)は\(\textrm{ZFC}\)としますが、今回はそれを使わないので、\(MMT\)の中で形式化された適当な（算術を含み病的には弱すぎない）理論とします。\(MMT\)において\(MT\)を形式化した方法と同じ方法で\(MT\)において\(MT\)自身を形式化した理論を\(T\)と置き、その言語を\(L\)と置き、\(T\)において\(L\)を形式化した言語を\(FL\)と置きます。\(MT\)の項であるチューリングマシン\(M\)に対し、\(L\)論理式\(\forall k \in \mathbb{N}(\ulcorner M \urcorner(k) \downarrow)\)を\(\textrm{Total}_L(M)\)と置きます。同様に、\(T\)の項であるチューリングマシン\(M\)に対し、\(FL\)論理式\(\forall k \in \mathbb{N}(\ulcorner M \urcorner(k) \downarrow)\)を\(\textrm{Total}_{FL}(M)\)と置きます。

\(n\)を\(MT\)の項である自然数とします。\(MT\)において形式化された言語\(L\)上の理論\(T_{n,m}\)と\(T\)において形式化された言語\(FL\)上の理論\(FT_{n,m}\)を以下のように再帰的に定めます：

1. \(m = 0\)ならば、\(T_{n,m} := T\)であり、\(FT_{n,m}\)は\(T\)において形式化された\(T\)自身である。
2. \(m \neq 0\)とする。
   1. \(MT\)の項であるチューリングマシン\(M\)が「\((n,m)\)各点停止する」とは、以下の２条件を満たすということである：
      1. \(M\)の状態と字母は\(n\)以下の自然数である。
      2. \(T_{n,m-1}\)において\(n\)文字以下で\(L\)論理式\(\forall k \in \mathbb{N}(FT_{n,m-1} \vdash \ulcorner \ulcorner M \urcorner \urcorner(\ulcorner k \urcorner) \downarrow)\)が証明可能である。
   2. \((n,m)\)各点停止するチューリングマシン全体を\(P_{n,m}\)と置く。
   3. \(P_{n,m}\)の濃度を\(c_{n,m} \in \omega\)と置き、コード化により\(P_{n,m}\)を数え上げた列を\(M_{n,m,0}, \ldots, M_{n,m,c_{n,m}-1}\)と置く。
   4. \(T_{n,m} := T \cup \{\textrm{Total}_L(M) \mid M \in PT_{n,m}\}\)と定める。
   5. \(FT_{n,m} := FT \cup \{\textrm{Total}_{FL}(\ulcorner M_{n,m,0} \urcorner), \ldots, \textrm{Total}_{FL}(\ulcorner M_{n,m,c_{n,m}-1} \urcorner)\}\)と定める。

巨大関数

\(MT\)において計算可能部分写像 \begin{eqnarray*} f_{MT} \colon \mathbb{N} & \to & \mathbb{N} \\ n & \mapsto & f_{MT}(n) \end{eqnarray*} を「\(T_{n,n}\)において\(n\)文字以下で\(\ulcorner M \urcorner\)の停止性が証明可能であるチューリングマシン\(M\)の停止ステップ数の上限」と定めます。

念押しで\(MT\)において計算可能部分写像 \begin{eqnarray*} F_{MT} \colon \mathbb{N} & \to & \mathbb{N} \\ n & \mapsto & F_{MT}(n) \end{eqnarray*} を\(f_{MT}^n(n)\)と定義します。

もちろんチューリングマシンを使ったところは他の計算モデルでも構いません。今回の手法は\(MT\)の選び方や形式化の仕方、計算モデルやコード化の仕方を動かすごとに計算可能部分関数が得られます。

特に、巨大数屋敷で導入した計算モデルと\(\textrm{ZFC}\)公理系の形式化\(\textrm{AxArray}\)を使えばコード化やゲーデル対応が一意でないという問題も解決できます。そうして定義し直した\(f_{\textrm{ZFC}}\)や\(f_{\textrm{ZFC}+\textrm{I}0}\)をそれぞれ記号を変え\(\textrm{lim}_{\textrm{ZFC}}\)や\(\textrm{lim}_{\textrm{ZFC}L+\textrm{I}0}\)と書いて区別してみればより厳密ですね。

最小の超越整数の関数化\(\textrm{TransInt}(n)\)同様に、\(f_{MT}(n)\)に計算アルゴリズムを与えることが出来ます。まず\(T_{n,m}\)を文字列の集合として再帰的に定められることは定義から問題がありませんね。すると、\(L\)論理式のみからなる列であって総文字数が\(n\)以下であるもの全体は有限個なので、その中から\(T_{n,n}\)における\(n\)文字以下の証明全体を取り出すことが出来ます。それら有限個の証明それぞれに対し、証明の末尾の文字列である\(L\)論理式を確認することでチューリングマシンの停止性の証明のみを取り出すこともできますし、そのチューリングマシンのコードを取り出すことも出来ます。コードさえ取り出せれば、万能チューリングマシンを使うことでそのチューリングマシンを実際に動かすことができます。というわけで、取り出した有限個の全てのコードに対し同時に万能チューリングマシンを用いて対応するチューリングマシンを動かし、それら全てが停止したステップ数を出力すれば良いです。問題になるのが、実際にそれらが全て停止するか否かです。それらを全て停止させて初めて\(f_{MT}\)が出力を返すので、それらが全て停止するなら\(f_{MT}(n)\)の計算も停止しますが、そうでないなら\(f_{MT}(n)\)の計算は停止しません。それでは困るのですが、\(f_{MT}(n)\)が\(\textrm{TransInt}(n)\)等と同様に各点でwell-definedとなることを次の章で説明をします。

Well-defined性

以下、やはり\(MMT\)と\(MT\)は病的には弱すぎないとします。更に\(MT\)の\(\omega\)無矛盾性の下で、\(f_{MT}\)の各点でのwell-defined性を\(MT\)が証明可能であることを\(MMT\)が証明可能であることを示します。

定理（\(f_{MT}\)の各点におけるwell-defined性）
「\(MT\)が\(\omega\)無矛盾ならば、任意の\(n \in \mathbb{N}\)に対し\(MT \vdash f_{MT}(\ulcorner n \urcorner) \downarrow\)である」ということが\(MMT\)で証明可能である。

いくつかの補題を用いて定理を証明していきます。もちろん\(MT\)が\(\textrm{ZFC}\)や\(\textrm{ZFC}+\textrm{I}0\)である時は、\(f_{MT}\)を\(\lim_{\textrm{ZFC}}\)や\(\lim_{\textrm{ZFC}+\textrm{I}0}\)に置き換えた主張も全く同様に証明することが出来ます。

補題1（\(\Sigma_1\)健全拡大からのreduction）
「任意のチューリングマシン\(M\)と\(n \in \mathbb{N}\)と\(MT\)の拡大\(MT'\)に対し、\(MT'\)が\(\Sigma_1\)健全かつ\(MT' \vdash \ulcorner M \urcorner (\ulcorner n \urcorner) \downarrow\)ならば、\(MT \vdash \ulcorner M \urcorner (\ulcorner n \urcorner) \downarrow\)である」ということが\(MMT\)で証明可能である。

証明

\(MT'\)が\(\Sigma_1\)健全かつ\(MT' \vdash \ulcorner M \urcorner (\ulcorner n \urcorner) \downarrow\)より、\(M(n) \downarrow\)である。従って\(M(n)\)の計算過程を\(ML\)論理式に対応させることで、\(\ulcorner M \urcorner(\ulcorner n \urcorner) \downarrow\)の\(MT\)における証明を得る。□

ここで\(MMT\)の項であるチューリングマシン\(M\)に対し、\(ML\)論理式\(\forall k \in \mathbb{N}(\ulcorner M \urcorner(k) \downarrow)\)を\(\textrm{Total}_{ML}(M)\)と置きます。

補題2（\(\omega\)無矛盾性の遺伝性）
「チューリングマシンの任意の集合\(S\)に対し、\(MT\)が\(\omega\)無矛盾かつ任意の\(M \in S\)と\(k \in \mathbb{N}\)に対し\(MT \vdash \ulcorner M \urcorner (\ulcorner k \urcorner) \downarrow\)ならば、\(MT \cup \{\textrm{Total}_{ML}(M) \mid M \in S\}\)は\(\omega\)無矛盾である」ということが\(MMT\)で証明可能である。

証明

任意の\(M \in S\)に対し、\(M\)が\(\mathbb{N}\)上全域であることを示す。\(k \in \mathbb{N}\)とする。\(MT\)が\(\omega\)無矛盾かつ\(MT \vdash \ulcorner M \urcorner (\ulcorner k \urcorner) \downarrow\)であるので、ある\(i \in \mathbb{N}\)が存在して\(MT\)は\(\ulcorner M \urcorner (\ulcorner k \urcorner)\)の計算が\(\ulcorner i \urcorner\)ステップ以下で停止することが証明可能である。\(M(k)\)の計算が\(i\)ステップ以下で停止しないと仮定すると、\(M(k)\)の計算過程\(i+1\)ステップを\(ML\)論理式に対応させることで、\(\ulcorner M \urcorner (\ulcorner k \urcorner)\)の計算が\(\ulcorner i \urcorner\)ステップ以下で停止しないことの\(MT\)における証明を得る。特に\(MT\)は矛盾するが、これは\(MT\)の\(\omega\)無矛盾性に反し矛盾する。従って\(M(k)\)の計算が\(i\)ステップ以下で停止する。すなわち\(M(k) \downarrow\)である。以上より\(M\)は\(\mathbb{N}\)上全域である。特に\(\textrm{Total}_{ML}(M)\)は標準モデル\(\mathbb{N}\)において真である。\(MT\)が\(\omega\)無矛盾かつ\(\{\textrm{Total}_{ML}(M) \mid M \in S\}\)が標準モデル\(\mathbb{N}\)で真な文の集合であることから、\(MT \cup \{\textrm{Total}_{ML}(M) \mid M \in S\}\)は\(\omega\)無矛盾である。□

補題3（\(T_{n,m}\)の基本性質）

「任意の\(n,m \in \mathbb{N}\)に対し、チューリングマシンのある有限集合\(S\)が存在し、\(S\)の濃度を\(c \in \omega\)と置き、コード化により\(S\)を数え上げた列を\(M_0, \ldots, M_{c-1}\)と置くと、任意の\(i \in \mathbb{N}\)と\(k \in \mathbb{N}\)に対し\(i < c\)ならば\(MT \vdash \ulcorner M_i \urcorner (\ulcorner k \urcorner) \downarrow\)であり、かつ\(MT \vdash T \cup \{\textrm{Total}_L(\ulcorner M_0 \urcorner), \ldots, \textrm{Total}_L(\ulcorner M_{c-1} \urcorner) = T_{\ulcorner n \urcorner, \ulcorner m \urcorner}\)である」ということが\(MMT\)で証明可能である。

証明

\(m\)に関する数学的帰納法で示す。\(m = 0\)の時、\(T_{\ulcorner n \urcorner, \ulcorner m \urcorner} = T\)より\(S = \emptyset\)とすればよい。\(m > 0\)とする。帰納法の仮定より、チューリングマシンの有限集合\(S'\)であって、\(S'\)の濃度を\(c' \in \omega\)と置きコード化により\(S'\)を数え上げた列を\(M'_0, \ldots, M'_{c'-1}\)と置くと２条件

1. 任意の\(i \in \mathbb{N}\)と\(k \in \mathbb{N}\)に対し\(i < c'\)ならば「\(\ulcorner M'_i \urcorner (\ulcorner k \urcorner) \downarrow\)である」という\(ML\)論理式が\(MT\)で証明可能である。
2. \(MT \vdash T \cup \{\textrm{Total}_L(\ulcorner M'_0 \urcorner), \ldots, \textrm{Total}_L(\ulcorner M'_{c'-1} \urcorner) = T_{\ulcorner n \urcorner, \ulcorner m-1 \urcorner}\)である

を満たすものが存在する。

従って、

任意の\(M \in P_{\ulcorner n \urcorner, \ulcorner m \urcorner}\)に対し、\(T \cup \{\textrm{Total}_L(\ulcorner M'_0 \urcorner), \ldots, \textrm{Total}_L(\ulcorner M'_{c'-1} \urcorner)\}\)において\(\ulcorner n \urcorner\)文字以下で\(L\)論理式\(\forall k \in \mathbb{N}(FT \cup \{\textrm{Total}_{FL}(\ulcorner \ulcorner M'_0 \urcorner \urcorner), \ldots, \textrm{Total}_L(\ulcorner \ulcorner M'_{c'-1} \urcorner \urcorner)\} \vdash \ulcorner \ulcorner M \urcorner \urcorner(\ulcorner k \urcorner) \downarrow)\)が証明可能である

という\(ML\)論理式が\(MT\)で証明可能である。すると

任意の\(M \in P_{\ulcorner n \urcorner, \ulcorner m \urcorner}\)と\(k \in \mathbb{N}\)に対し、\(T \cup \{\textrm{Total}_L(\ulcorner M'_0 \urcorner), \ldots, \textrm{Total}_L(\ulcorner M'_{c'-1} \urcorner)\} \vdash \ulcorner M \urcorner(\ulcorner k \urcorner) \downarrow\)である

という\(ML\)論理式が\(MT\)で証明可能であることが最小の超越整数のwell-defined性と同様の議論により従う、特に\(MT \cup \{\textrm{Total}_{ML}(M'_0), \ldots, \textrm{Total}_{ML}(M'_{c'-1})\}\)でも証明可能である。従って任意の\(k \in \mathbb{N}\)に対し

任意の\(M \in P_{\ulcorner n \urcorner, \ulcorner m \urcorner}\)に対し、\(M(\ulcorner k \urcorner) \downarrow\)である

という\(ML\)論理式が\(MT \cup \{\textrm{Total}_{ML}(M'_0), \ldots, \textrm{Total}_{ML}(M'_{c'-1})\}\)で証明可能である。

また

任意のチューリングマシン\(M\)に対し、\(M \in P_{\ulcorner n \urcorner, \ulcorner m \urcorner}\)であることと\(M = \ulcorner M_{n,m,0} \urcorner\)または……または\(M = \ulcorner M_{n,m,c_{n,m}-1} \urcorner\)であることが同値である

という\(ML\)論理式が\(MT\)で証明可能であるので、任意の\(k \in \mathbb{N}\)に対し

任意のチューリングマシン\(M\)と\(M = \ulcorner M_{n,m,0} \urcorner\)または……または\(M = \ulcorner M_{n,m,c_{n,m}-1} \urcorner\)ならば、\(M(\ulcorner k \urcorner) \downarrow\)である

という\(ML\)論理式が\(MT \cup \{\textrm{Total}_{ML}(M'_0), \ldots, \textrm{Total}_{ML}(M'_{c'-1})\}\)で証明可能である。

従って\(MT\)の\(\omega\)無矛盾性と補題1（\(\Sigma_1\)健全拡大からのreduction）より、任意の\(k \in \mathbb{N}\)に対し

任意のチューリングマシン\(M\)に対し、\(M = \ulcorner M_{n,m,0} \urcorner\)または……または\(M = \ulcorner M_{n,m,c_{n,m}-1} \urcorner\)ならば、\(M(\ulcorner k \urcorner) \downarrow\)である

という\(ML\)論理式が\(MT\)でも証明可能である。\(S := P_{n,m}\)と置く。\(S\)の濃度\(c\)は\(c_{n,m}\)に他ならず、コード化により\(S\)を数え上げた列\(M_0, \ldots, M_{c-1}\)は\(M_{n,m,0} \urcorner, \ldots, \ulcorner M_{n,m,c_{n,m}-1}\)に他ならないので、上述したことにより、

任意の\(i \in \mathbb{N}\)と\(k \in \mathbb{N}\)に対し\(i < c\)ならば\(MT \vdash \ulcorner M_i \urcorner (\ulcorner k \urcorner) \downarrow\)

である。以上より、

\(MT \vdash T \cup \{\textrm{Total}_L(\ulcorner M_0 \urcorner), \ldots, \textrm{Total}_L(\ulcorner M_{c-1} \urcorner) = T_{\ulcorner n \urcorner, \ulcorner m \urcorner}\)である

ということを示せばよい。

先程示したように

任意のチューリングマシン\(M\)に対し、\(M \in P_{\ulcorner n \urcorner, \ulcorner m \urcorner}\)であることと\(M = \ulcorner M_{n,m,0} \urcorner\)または……または\(M = \ulcorner M_{n,m,c_{n,m}-1} \urcorner\)であることが同値である

という\(ML\)論理式が\(MT\)が証明可能である。そのため、\(T_{\ulcorner n \urcorner, \ulcorner m \urcorner}\)の定義から

\begin{eqnarray*} & & T_{\ulcorner n \urcorner, \ulcorner m \urcorner} = T \cup \{\textrm{Total}_L(M) \mid M \in PT_{\ulcorner n \urcorner, \ulcorner m \urcorner}\} \\ & = & T \cup \{\textrm{Total}_L(M) \mid M = \ulcorner M_{n,m,0} \urcorner \lor \cdots \lor M = \ulcorner M_{n,m,c_{n,m}-1} \urcorner\} \\ & = & T \cup \{\textrm{Total}_L(M) \mid M = \ulcorner M_0 \urcorner \lor \cdots \lor M = \ulcorner M_{c-1} \urcorner\} \end{eqnarray*}

という\(ML\)論理式が\(MT\)で証明可能である。□

それでは主定理の証明に移ります。

定理（\(f_{MT}\)の各点におけるwell-defined性）の証明

\(f_{MT}\)の定義とゲーデル数が有界な\(L\)論理式の集合の有限性より、

任意のチューリングマシン\(M\)に対し、\(T_{\ulcorner n \urcorner, \ulcorner n \urcorner}\)において\(\ulcorner n \urcorner\)文字以下で\(\ulcorner M \urcorner\)の停止性が証明可能であるならば、\(M\)が停止する

という\(ML\)論理式が\(MT\)で証明可能であることを示せばよい。補題3（\(T_{n,m}\)の基本性質）より、チューリングマシンの有限集合\(S\)であって、\(S\)の濃度を\(c \in \omega\)と置きコード化により\(S\)を数え上げた列を\(M_0, \ldots, M_{c-1}\)と置くと、２条件

1. 任意の\(i \in \mathbb{N}\)と\(k \in \mathbb{N}\)に対し\(i < c\)ならば\(MT \vdash \ulcorner M_i \urcorner (\ulcorner k \urcorner) \downarrow\)である
2. \(MT \vdash (T \cup \{\textrm{Total}_L(\ulcorner M_0 \urcorner), \ldots, \textrm{Total}_L(\ulcorner M_{c-1} \urcorner)\} = T_{\ulcorner n \urcorner, \ulcorner n \urcorner})\)である

を満たすものが存在する。

従って、

任意のチューリングマシン\(M\)に対し、\(T \cup \{\textrm{Total}_L(\ulcorner M_0 \urcorner), \ldots, \textrm{Total}_L(\ulcorner M_{c-1} \urcorner)\}\)において\(\ulcorner n \urcorner\)文字以下で\(\ulcorner M \urcorner\)の停止性が証明可能であるならば、\(M\)が停止する

という\(ML\)論理式が\(MT\)で証明可能であることを示せばよい。まず最小の超越整数のwell-defined性と同様の議論により、

任意のチューリングマシン\(M\)に対し、\(T \cup \{\textrm{Total}_L(\ulcorner M_0 \urcorner), \ldots, \textrm{Total}_L(\ulcorner M_{c-1} \urcorner)\}\)において\(\ulcorner n \urcorner\)文字以下で\(\ulcorner M \urcorner\)の停止性が証明可能であるならば、\(M\)が停止する

という\(ML\)論理式が\(MT \cup \{\textrm{Total}_{ML}(M) \mid M \in S\}\)で証明可能である。

ここで、\(MT \cup \{\textrm{Total}_{ML}(M) \mid M \in S\}\)において\(n\)文字以下で停止性が証明可能なチューリングマシン全体の集合を\(P_n\)と置き、\(P_n\)の濃度を\(c' \in \omega\)と置き、コード化による\(P_n\)の数え上げを\(M'_0, \ldots, M'_{c'-1}\)と置くと、

任意のチューリングマシン\(M\)に対し、\(T \cup \{\textrm{Total}_L(\ulcorner M_0 \urcorner), \ldots, \textrm{Total}_L(\ulcorner M_{c-1} \urcorner)\}\)において\(\ulcorner n \urcorner\)文字以下で\(\ulcorner M \urcorner\)の停止性が証明可能であることと、\(M = \ulcorner M'_0 \urcorner\)または……または\(M = \ulcorner M'_{c'-1} \urcorner\)であることは同値である

という\(ML\)論理式が\(MT\)で証明可能であるので、

任意のチューリングマシン\(M\)に対し、\(M = \ulcorner M'_0 \urcorner\)または……または\(M = \ulcorner M'_{c'-1} \urcorner\)であるならば、\(M\)が停止する

という\(ML\)論理式が\(MT \cup \{\textrm{Total}_{ML}(M) \mid M \in S\}\)で証明可能である。

補題2（\(\omega\)無矛盾性の遺伝性）より、\(MT \cup \{\textrm{Total}_{ML}(M) \mid M \in S\}\)は\(\omega\)無矛盾である。従って補題1（\(\Sigma_1\)健全拡大からのreduction）より、

任意のチューリングマシン\(M\)に対し、\(M = \ulcorner M'_0 \urcorner\)または……または\(M = \ulcorner M'_{c'-1} \urcorner\)であるならば、\(M\)が停止する

という\(ML\)論理式が\(MT\)でも証明可能である。先程述べたように

任意のチューリングマシン\(M\)に対し、\(T \cup \{\textrm{Total}_L(\ulcorner M_0 \urcorner), \ldots, \textrm{Total}_L(\ulcorner M_{c-1} \urcorner)\}\)において\(\ulcorner n \urcorner\)文字以下で\(\ulcorner M \urcorner\)の停止性が証明可能であることと、\(M = \ulcorner M'_0 \urcorner\)または……または\(M = \ulcorner M'_{c'-1} \urcorner\)であることは同値である

という\(ML\)論理式が\(MT\)で証明可能であることと合わせ、

任意のチューリングマシン\(M\)に対し、\(T \cup \{\textrm{Total}_L(\ulcorner M_0 \urcorner), \ldots, \textrm{Total}_L(\ulcorner M_{c-1} \urcorner)\}\)において\(\ulcorner n \urcorner\)文字以下で\(\ulcorner M \urcorner\)の停止性が証明可能であるならば、\(M\)が停止する

という\(ML\)論理式が\(MT\)で証明可能である。□

以上で\(f_{MT}\)が各点でwell-definedであることを、\(MT\)を強めることなく証明することが出来ました。

ただし\(MMT\)の項である自然数\(n\)に対し\(MT \vdash f_{MT}(\ulcorner n \urcorner) = \ulcorner m \urcorner\)が\(MMT\)で証明可能であるような\(MMT\)の項である自然数\(m\)が存在する保証はないので、少なくとも全く同じ議論では\(MT\)を強めることなく\(F_{MT}\)の全域性を\(MT\)が証明可能であることを\(MMT\)で証明できません。

一方で\(MMT\)を十分強く取っておけば\(MT\)を強めることなく\(F_{MT}\)の全域性を\(MT\)が証明可能であることを\(MMT\)は証明可能です。実際、\(MMT\)を十分強く取れば\(MMT\)においても\(f_{MT}\)と同様の関数\(f_{MMT}\)が定義可能であり、\(MMT\)を更に十分強く取れば\(f_{MMT}\)の全域性も証明可能であり、しかも\(MMT\)の項である任意の自然数\(n\)に対し\(f_{MMT}(n)\)の計算過程をそのまま論理式に落としたものが\(f_{MT}(\ulcorner n \urcorner)\)の計算過程を表すので、結果的に（\(MT\)を一切強めることなく）

\(MMT \vdash \forall n \in \mathbb{N}(MT \vdash f_{MT}(\ulcorner n \urcorner) = \ulcorner f_{MMT}(n) \urcorner)\)

となります。従って\(n = \ulcorner n \urcorner, \ulcorner f_{MMT}(n) \urcorner, \ulcorner f^2_{MMT}(n) \urcorner, \ldots, \ulcorner f_{MMT}^{n-1}(n) \urcorner\)に対し\(f_{MT}(n)\)の計算の停止性を\(MT\)で示すことで、\(F_{MT}(n)\)の計算の停止性を\(MT\)で示すことが出来ます。以上より、

\(MMT \vdash \forall n \in \mathbb{N}(MT \vdash F_{MT}(\ulcorner n \urcorner) \downarrow)\)

となります。もちろん\(MMT\)を矛盾させればこんな式はいつでも成り立ちますし何なら示したい証明可能性を公理に追加したり\(F_{MT}\)と同様に定義される\(F_{MMT}\)の全域性を追加したりするだけでもいいですけどね。\(MMT\)に\(f_{MMT}\)の全域性を課すのは少しずるいと思うので、今回はそこまで課さなくても各点での停止性が\(MT\)で証明可能であることが\(MMT\)で証明可能である\(f_{MT}\)の方が\(F_{MT}\)よりチート感がなく受け入れられるのではないでしょうか。

解析

\(f_{MT}(n)\)は\(MT\)において各点でのwell-defined性が証明可能であった\(\textrm{TR}(MT,n)\)を（定義域上で）支配する計算可能部分可能関数です。実際、\(\textrm{TR}(MT,n)\)の各点のwell-defined性が\(MT\)で証明可能であることが\(MMT\)で（現実的な長さで）証明可能であるため、十分大きな\(N \in \mathbb{N}\)に対し\(T_{N,1}\)は\(\textrm{TR}(MT,n)\)の全域性を含む公理系となります。これを踏まえると、\(f_{MT}(n)\)は\(\textrm{TR}(MT,n)\)のナイーブな拡大では到達できないほど（定義域内で）急増大する計算可能部分関数となります。

例えば\(f_{\textrm{ZFC}}(n)\)や\(\textrm{lim}_{\textrm{ZFC}}(n)\)は\(\textrm{TransInt}(n)\)や\(\textrm{ZFC}\)公理系における巨大数屋敷のナイーブな拡大では到達できないほど（定義域内で）急増大する計算可能部分関数となり、\(f_{\textrm{ZFC}+\textrm{I}0}(n)\)は\(\textrm{ZFC}+\textrm{I}0\)においてI0関数や\(\textrm{ZFC}+\textrm{I}0\)における巨大数屋敷のナイーブな拡大では到達できないほど（定義域内で）急増大する計算可能部分関数となります。従ってこの関数は僕が定義した中では最も強い計算可能関数となると思います。

命名

ついでですので\(\textrm{lim}_{\textrm{ZFC}}\)を用いて巨大数も１つ定義しておきましょう。\(\textrm{ZFC}\)公理系で定義される計算可能巨大数\(\textrm{lim}_{\textrm{ZFC}}(10 \uparrow^{10} 10)\)を

さあ盟友、

と名付けます。ただし\(\uparrow^{10}\)はハイパー演算子で冪乗の仲間です。どこかでミスをしていなければ、定義からこれは最小の超越整数よりも大きな数となります。