Generalized Decidability via Brouwer Trees

あなたは、ある謎を解こうとしている探偵だと想像してください。コンピュータサイエンスの世界では、通常、謎を3つのバケツに分類します：決定可能（Decidable）（素早く答えを見つけられる）、半決定可能（Semidecidable）（「はい」という答えは見つけられるが、「いいえ」の場合は永遠に待ち続ける可能性がある）、そして決定不能（Undecidable）（全く解けない）です。

しかし、もし他のものよりも「より」半決定的な謎があるとしたらどうでしょう？ もし、ある「はい」の答えを見つけるのに少し時間がかかるものの、それでも永遠にはかからないとしたら？

これこそが、トム・デ・ヨング、ニコライ・クラウス、アレフ・モハママザデ、そしてフレドリック・ノルドヴァル・フォスベリが、彼らの新しい論文で探求していることです。彼らは、**ブルアの木順序数（Brouwer tree ordinals）*と呼ばれる特別な数体系を用いて、答えの「はい」を見つけるのに正確にどれくらいの時間*がかかるかを測定する方法を提案しています。これは、通常の1、2、3といった数字ではなく、無限を遥かに超えていく、魔法の階段のようなものです。

時間の魔法の梯子

彼らの枠組みでは、単に「解ける」とは言いません。「それは**$\alpha$-決定可能（$\alpha$-decidable）**である」と言います。ここで、$\alpha$ は彼らの魔法の梯子の特定の段（ステップ）を指します。

• レベル1（決定可能）： ある問題が1-決定可能である場合、それは有限のステップで答えを見つける（あるいは不可能であることを証明する）ことができることを意味します。これは素数かどうかをチェックするようなものです。数を数えていけば、最終的には確信が得られます。
• レベル $\omega + 1$（半決定可能）： ある問題が$(\omega + 1)$-決定可能である場合、もし答えが「はい」であれば、$\omega$ ステップ以内にそれを見つけることができます。しかし、$\omega$ は普通の数字ではありません。それは「永遠に数え続けること」を表しています。したがって、もし答えが「はい」であれば、いつかは見つかりますが、もし「いいえ」であれば、止まることなく数え続けてしまうかもしれません。これが、半決定可能の古典的な定義です。

著者たちは、この新しいシステムが古いシステムと完璧に一致することを証明しています。問題が「決定可能」であれば、それは段1に当てはまります。もし「半決定可能」であれば、それは段$\omega + 1$に当てはまります。しかし、魔法は、その間やさらに上の段についても語れるようになった点にあります。

双子素数の謎

これがどのように機能するかを示すために、彼らは有名な数学のパズルである双子素数予想を使用します。これは、「数字を数え上げても、常に（3と5や11と13のように）2の差しかない素数のペアが存在するか？」と問うものです。

• 特定のペアが存在するかどうかをチェックするのは簡単です（決定可能）。
• ある一定の数以上の範囲に（少なくとも一つ）ペアが存在するかどうかをチェックするのは半決定可能です（探し続け、もし見つかれば停止します）。
• しかし、大きな問いは、これがすべての数に対して真であるかどうかです。

著者たちは、この特定の問いが$\omega^2$-決定可能であることを示しました。$\omega$ を一つの無限のステップの列だとすると、$\omega^2$ は、それらの列が無数に積み重なったようなものです。つまり、もし双子素数予想に対する反例が存在するならば、それを見つけることはできますが、それには「無限の列が無限に積み重なった中を歩く」ことに相当する時間経過が必要になるかもしれない、ということです。

彼らはまた、これらの問題を組み合わせた場合に何が起こるかも調べました：

• AND（かつ）： 二つの問題が$\alpha$-決定可能であるとき、それらの「AND」（両方が真であること）もまた$\alpha$-決定可能です。これは二つのボックスをチェックするようなもので、両方を同じ時間制限内でチェックできれば問題ありません。
• OR（または）： これはより複雑です。二つの問題があるとき、それらの「OR」（どちらかが真であること）が決定可能であると保証されるのは、時間制限が十分に小さい場合（具体的には、レベルが $\omega \cdot k + n$ のような場合）に限られます。もし時間制限があまりに巨大になりすぎると、「OR」は彼らのシステムのルールを壊してしまう可能性があります。

「選択」の問題

ここからが非常に興味深いところです。著者たちは、無限個の「半決定可能」な問題（すべての開始数に対して双子素数予想をチェックすることなど）を組み合わせようとすると、壁に突き当たることを発見しました。**可算選択（Countable Choice）**という特別な数学的ルールがなければ、組み合わせた結果が半決定可能であることを証明できません。

実際、もしそのルールなしでそれを証明できるとしたら、それは他の基本的な論理法則を破壊してしまうことを彼らは証明しました。したがって、彼らは、無限の組み合わせにおいて数学をスムーズに機能させるためには、可算選択を仮定する必要があると示唆しています。

しかし、彼らは回避策も見つけました！ 彼らは、**シェルピンスキー・半決定可能（Sierpiński-semidecidable）**と呼ばれる、別の種類の「半決定可能」を調べました。これは、元のものよりも少し弱いバージョンの半決定可能性であり、可算選択のルールを必要とせずに無限のリストを組み合わせることができます。それは、明るさは少し劣るかもしれませんが、電池（選択ルール）がなくても点灯できる、異なる種類の懐中電灯のようなものです。

彼らが解かなかったこと

この論文が「していないこと」を知っておくことも重要です。著者たちは非常に明確に、彼らは双子素数予想を解いたわけではないと述べています。彼らは単に、この新しい「物差し」がどのように機能するかを示すための、おもちゃの例としてこれを使用したに過ぎません。

また、彼らは自分たちの梯子の全体像をまだ完全には把握していないことも認めています。彼らは、もし問題が段 $\alpha$ にあり、別の問題が段 $\beta$ にあり、$\alpha$ が $\beta$ よりも低い場合、$\alpha$ の問題は $\beta$ でも解けるはずだと考えていますが、まだすべての段についてこれを証明してはいません。これは、事実ではなく「予想（コンジェクチャー）」です。

結論

この論文は、数学やコンピューティングにおいて「はい」という答えを見つけるのがどれほど難しいかを語るための、新しい方法を提案しています。単に「見つけられる」か「見つけられない」かと言う代わりに、彼らは無限のステップで作られた精密な定規を与えてくれます。彼らは、この定規が既知のもの（決定可能および半決定可能）に対して機能することを証明し、双子素数予想のような複雑な問題を、$\omega^2$ という特定の測定可能な高さに位置づけました。

また、この定規は強力ですが、限界もあることも示しました。無限のリストの問題を組み合わせるには、可算選択という特定の仮定が必要であるか、あるいは、少し異なる種類の定規（シェルピンスキー半決定可能性）に切り替える必要があるということです。

これらすべては、Cubical Agida というコンピュータプログラムの中で構築され、検証されました。これは、論理のあらゆるステップが完璧であることを保証するための、極めて厳格な審判として機能します。したがって、アイデア自体は新しく刺激的なものですが、その数学的根拠は極めて堅実です。