- この記事は執筆中です。
この関数は計算不可能な関数にみられる共通点に着目したアイデアにより作られました。まず、非常に大雑把に言ってしまえば、計算不可能な関数は次のように表現できると思っています。
- ビジービーバー関数は「x文字以下のプログラムで表現できる自然数」の内で最も小さい物を返します。
- クサイ関数は「x文字以下の、神託コンビネータ\(Ω\)を追加したSKIコンビネータ計算(=プログラム)で表現できる自然数」の内で最も小さい物を返します。
- ラヨ数を生成する関数は「x文字以下の、一階集合理論(FOST)の言語で表現できる自然数」の内で最も小さい物を返します。
このように書くと、「x文字以下の〇〇で表現できる自然数」という共通点が見られます。〇〇の表現力が高いほど、この形式の関数の増加速度は速くなると考えられます。つまり、この推測が正しければ、〇〇の表現力を一階集合理論(FOST)よりも高めると、ラヨ数を生成する関数よりも増加速度が速い関数を作れると考えられます。この方法で作られた関数がビッグフットを生成する関数だと認識しています。
Hex関数は、上の「x文字以下の〇〇で表現できる自然数」という共通点に関する認識が正しいことを前提にした関数です。つまり、これが正しくなければ崩壊する「取らぬ狸の皮算用」的な関数です。ただ、作ってしまったので、このまま正しいとして進めていきます。
また、この関数は、「理論とは、論理式に関する記号と公理規則と推論規則しか定義されていない一階述語論理に、対象記号と関数記号と述語記号を付け加えたものである。」という認識に依存しています。
定義[]
まず、「x文字以下の〇〇で表現できる自然数」の〇〇に何を入れるかですが、「一階述語論理において、自然数を表現できる理論全て」を入れようと思います。この理論群に入るための条件は、大前提として矛盾していないことです。次に、ペアノの公理を満たすように関数記号\( \text{suc} \)と定数記号\( 0 \)を追加できる事です。これは数を取り扱えないような弱い理論を除くためです。
この理論群は少なくともペアノの公理を満たすシステム、つまり自然数を含むようになっています。この理論群において、x文字以下で論理式を作ります。この論理式には限定がなく、自由変数なども自由に含めても良いです(ただし、括弧などは文字数に数えません)。その後、考えられる全ての論理式に次の操作をします。まず、矛盾しているものを除きます。その後、全ての自由変数に対して、一意的に自然数を定めるものの内で、……