最小の証明を書けなくても戦え数

以下の項目と混同しないように注意してください：最小の証明を書けて戦え数

最小の証明を書けなくても戦え数はp進大好きbotが2018年3月21日に考案した東方巨大数である。第2回東方巨大数に投稿され、審査期間中に審査員による解析が終了しなかったため殿堂入りとなった。同じく第2回東方巨大数に投稿された最小の証明を書けて戦え数の亜種であり、名前の由来は東方Projectの登場キャラクターである秦こころのセリフ「最強の称号を賭けて私と闘え」である。

後述するように最小の証明を書けなくても戦え数はオラクルチューリングマシンで計算可能であるため、オラクルビジービーバー関数に十分大きい値を入力した数よりは小さいと考えられる。

定義

形式言語FOLのアルファベット集合を以下の和集合とし、

• FOL_{定項記号} := {2n+1 | n ∈ N}
• FOL_{変項記号} := {2(2n+1) | n ∈ N}
• 自然数 a に対し FOL_{a,引数関数記号} := {4(2^{a+1}(2n+1)+1) | n ∈ N}
• 自然数 a に対し FOL_{a,引数関係記号} := {8(2^{a+1}(2n+1)+1) | n ∈ N}
• FOL_{論理記号} := {16, 48, 80}
• FOL_{矛盾記号} := {32}
• FOL_{論理式記号} := {64(2n+1) | n ∈ N}

その統語を以下のように定める。

1. FOLの「項」とはFOLの文字列であって、FOL_{定項記号} の元か、FOL_{変項記号} の元か、またはある自然数 a と FOL_{a,引数関数記号} の元 f と a 個の項 (t₁, ..., t_a) を用いて f(t₁, ..., t_a) と表されるもののいずれかである。
2. FOLの「論理式」とはFOLの文字列であって、ある自然数 a と FOL_{a,引数関係記号} の元 r と a 個の項 (t₁, ..., t_a) を用いて r(t₁, ..., t_a) と表されるものか、FOL_{論理式記号} の元か、32か、FOL_{変項記号} の元 x と論理式 P を用いて 16x(P) と表されるものか、論理式 P と Q を用いて (P)48(Q) と表されるものか、論理式 P を用いて 80(P) と表されるもののいずれかである。
3. FOL の論理式が「1階」とは、文字列として FOL_{論理式記号} の元を含まないということである。

特に、FOL から FOL_{論理式記号} を除いた形式言語 FOL' は1階述語論理の形式言語であり、ZFC公理系の置換公理以外を FOL' における ∧ の解釈で結合したものと論理式記号を用いて置換公理の公理図式を表す論理式を FOL' における ∧ の解釈で結合して得られる文字列 A_{ZFC} は FOL の論理式である。

FOL の論理式 A と1階論理式 P に対し「A を公理として P を証明可能である」とは、A に含まれる FOL_{論理式記号} の元を全てある1階論理式に置き換えて得られる有限個の1階論理式を公理として P が FOL' において証明可能であるということである。

FOL の論理式 A に対し「A が無矛盾である」とは、A を公理として 32 を証明可能でないということである。無矛盾性に限らず一般の証明不可能性は全ての証明のゲーデル数を探索することで確認できるため、オラクルチューリングマシンで判定可能である。

自然数 n に対し、ペアノ算術の項 t_n を以下のように定める。

• n=0 の時、t_n は定項記号 0 である。
• n>0 の時、t_n は項 S(t_n-1) である。

自然数 n に対し、自然数 f(n) を「FOLの n 文字以下のある論理式 A と FOL の n 文字以下のある1階論理式 P が存在して『Aがペアノ算術を内包し、A_{ZFC} が無矛盾ならば A が無矛盾であり、P に出現する FOL_{変項記号} の元 x であって 16 で束縛されていないものがただ1つ存在し、P に出現する x であって 16 で束縛されていないものを全て t_m の A での像 t に置き換えた1階論理式と 16x((P)48(x=t)) を FOL' における ∧ の解釈で結合した1階論理式を Q とおいた時に 80(Q) が A において証明可能でないような最小の自然数が m である』ような任意の自然数 m」を超える最小の自然数、と定める。

f(10^100) を「最小の証明を書けなくても戦え数」と定義する。

背景

第2回東方巨大数のルールにおける巨大数は、ZFC公理系が無矛盾である仮定の下でZFC公理系で定義される自然数であると規定されている。そのため、\(\textrm{FOL}\)はZFC集合論をメタ理論としてその中で定義された形式言語である。

計算不可能巨大数の定義に形式体系を用いる手法として、具体的な形式体系内にメタ理論の自然数を埋め込んでその形式体系の表現力を利用してメタ理論の巨大数を定義するものがある。最小の証明を書けなくても戦え数でも同様であるが、メタ理論の自然数を埋め込んだ形式体系そのものを変数のように動かしているという点で少し異なる。これは第1回東方巨大数のエントリーである「こいし数」で用いられたことが元となった手法である。

形式体系の表現力を利用する際に「証明可能性」より強い「モデルでの真理値」が使われることが多々あるが、メタ理論の自然数をそこから定義するには形式体系のモデルを何らかの非標準な方法で指定し、そのモデルに相対化された自然数とメタ理論の自然数を対応付ける必要がある。形式体系自体が算術であるような特別な場合ならばモデルがメタ理論内の定義可能集合として具体的に構成できるし、集合論である場合はメタ理論自体のモデルを用いるかPlatonist's universeの抽象的な存在を課すことが流儀によっては許容されるが、一般の形式体系においてはモデルが無限に存在してしまう。具体的に構成できないものからといって任意のモデルから自然数を取り出してそれら全ての最大値を定義しようにも、現れる自然数も無限個になってしまっては最大値が存在しなくなってしまうという問題がある。そこで今回は「モデルでの真理値」よりさらに強い適用範囲の広い「反証不能性」が用いられている。

なお巨大数の定義に用いる上で、証明可能性よりモデルでの真理値を用いる方が使える論理式が増え、さらに反証不能性を用いる方が使える論理式が増えることは、証明可能性と恒真性の同値性から容易に従う。しかし使用可能な論理式が増えるという事実だけでは巨大数の大きさを一切保証せず、巨大数の大きさは使用可能な論理式から数を取り出す操作に強く依存する。実際、前述したようにf(n)は論理式を絞るだけでなく数を取り出す操作自体にも反証不能性しか用いていないためオラクルチューリングマシンで計算可能な手続きのみで定義されており、具体的なモデルにおける真理値や真理述語を用いた巨大関数よりは増大度が見込みにくい。

形式言語FOL

メタ論理であるZFC集合論の形式言語と区別するために\(\textrm{FOL}\)はメタ理論の自然数を用いてコード化されているが、それを通常の記法に戻すと以下のようになる。

• \(\textrm{FOL}_{\textrm{定項記号}} := \{c_n \mid n \in \mathbb{N}\}\)
• \(\textrm{FOL}_{\textrm{変項記号}} := \{x_n \mid n \in \mathbb{N}\}\)
• 自然数\(a\)に対し\(\textrm{FOL}_{a,\textrm{引数関数記号}} \ \ \ \ \ \ := \{f_{a,n} \mid n \in \mathbb{N}\}\)
• \(\textrm{FOL}_{2,\textrm{引数関係記号}} \ \ \ \ \ \ := \{=\} \cup \{r_{2,n} \mid n \in \mathbb{N}\}\)
• 自然数\(a \neq 2\)に対し\(\textrm{FOL}_{a,\textrm{引数関係記号}} \ \ \ \ \ \ := \{r_{a,n} \mid n \in \mathbb{N}\}\)
• \(\textrm{FOL}_{\textrm{論理記号}} := \{\forall,\to,\neg\}\)
• \(\textrm{FOL}_{\textrm{矛盾記号}} := \{\perp\}\)
• \(\textrm{FOL}_{\textrm{論理式記号}} := \{P_n \mid n \in \mathbb{N}\}\)

\(\textrm{FOL}\)の部分集合である\(\textrm{FOL}'\)は1階述語論理の形式言語としてよく採用されるものの１つであり、その流儀において例えば論理式\(P,Q\)に対する\(P \wedge Q\)は\(\neg(P \to (\neg Q)\)の略記であると解釈され、論理式\(P\)に対する\(\exists x_n(P)\)は\(\neg(\forall x_n(\neg P))\)の略記であると解釈される。この他、\(\vee\)や\(\exists !\)や\(\leftrightarrow\)も略記として用いられる。

\(\textrm{FOL}_{\textrm{論理式記号}}\)は通常の1階述語論理の形式言語に用いられないものであるため、\(\textrm{FOL}\)自体は1階述語論理の形式言語ではない。しかしながら、1階述語論理の形式言語である\(\textrm{FOL}'\)の論理式を動く変数のように扱う統語律が定義されているため、\(\textrm{FOL}'\)の公理図式を有限文字で記述するために用いることが出来る。

これにより、1階述語論理の公理系としては有限文字で記述することの出来ないZFC公理系やペアノ算術の公理系も、\(\textrm{FOL}\)においては有限文字の公理系\(A_{\textrm{ZFC}}\)や\(A_{\textrm{PA}}\)として表現することが出来る。以下にその具体的な方法を述べる。

ペアノ算術の実現

例えばペアノ算術の定項記号\(0\)を\(c_0\)に対応させ、後続を表す関数記号\(S\)を\(f_{1,0}\)に対応させ、加法を表す関数記号\(+\)を\(f_{2,0}\)に対応させ、乗法を表す関数記号\(\times\)を\(f_{2,1}\)に対応させる。数学的帰納法の公理図式以外は有限文字で記述されるためそれぞれ\(\textrm{FOL}'\)の論理式を定める。数学的帰納法は \begin{eqnarray*} ((((x_0 = 0) \to P_0) \wedge (\forall x_1(((x_0 = x_1) \to P_0) \to ((x_0 = S(x_1)) \to P_0)))) \to (\forall x_0(P_0)) \end{eqnarray*} という\(\textrm{FOL}\)の論理式を定める。これらを\(\wedge\)で結ぶことで、\(\textrm{FOL}\)の論理式\(A_{\textrm{PA}}\)を得る。\(\textrm{FOL}\)における証明可能性の定義から、\(A_{\textrm{PA}}\)での証明を考える時は数学的帰納法に対応する論理式の\(P_0\)を\(\textrm{FOL}'\)の任意の論理式に置き換えて良いので、これで実際に数学的帰納法の公理図式が実現されている。なおペアノ算術の公理系自体にはいくつかの等価な流儀がある（例えば関係記号\(\leq\)を持つか否か等）が、その差は今回ほとんど影響がないため各自好きな流儀を想定して良い。

ここでペアノ算術の項や項の定義文は自然数であるが、それはメタ論理のZFC集合論にとってはコード化された文字列に過ぎず、メタ論理の自然数とは異なる概念である。そのため、双方を関連付けるために\(n \mapsto t_n\)という「メタ論理の自然数からペアノ算術の項を対応させる写像」がメタ論理の写像として帰納的に定義されている。要するに、自然数\(n\)に対応するペアノ算術の項\(t_n\)とは\(\textrm{FOL}'\)の項である文字列\(S( \cdots S(0) \cdots)\)（\(S\)が\(n\)個）すなわち\(f_{1,0}( \cdots f_{1,0}(c_0) \cdots )\)（\(f_{1,0}\)が\(n\)個）に他ならない。

ZFC集合論の実現

例えばZFC集合論の関係記号\(\in\)を\(r_{2,0}\)に対応させる。置換公理の図式以外は有限文字で記述されるためそれぞれ\(\textrm{FOL}'\)の論理式を定める。置換公理の図式は \begin{eqnarray*} (\forall x_0(\exists ! x_1(P_0))) \to (\forall x_2(\exists x_3(\forall x_1((x_1 \in x_3) \leftrightarrow (\exists x_0((x_0 \in x_2) \wedge P_0)))))) \end{eqnarray*} という\(\textrm{FOL}\)の論理式を定める。これらを\(\wedge\)で結ぶことで、\(\textrm{FOL}\)の論理式\(A_{\textrm{ZFC}}\)を得る。

ペアノ算術の内包

\(\textrm{FOL}\)の論理式\(A\)がペアノ算術を内包するとは、\(A_{\textrm{PA}}\)の包含が固定されているということである。すなわち、引数\(1\)の関係記号\(r_{1,k}\)が存在して、\(A_{\textrm{PA}}\)を公理として証明可能であるような\(\textrm{FOL}'\)の任意の論理式\(\Phi\)に対し、\(\Phi\)の量化を全て\(r_{1,k}\)に制限したものが、\(A\)を公理として証明可能であるということである。

量化の制限は1階述語論理と同じ方法で行う。すなわち量化を\(r_{1,k}\)に制限するとは、「\(\forall x_m(P)\)を\(\forall x_m((r_{1,k}(x_m) \to P))\)に置き換える」という操作を（１つの量化子についてただ一度だけ適用されるように論理式の構造に関する再帰によって）繰り返すということである。これにより、量化された変数の動く範囲が\(r_{1,k}\)を満たすものだけに制限される。要するに、「ペアノ算術の項である」ということを表現する関係記号\(r_{1,k}\)を１つ固定したということである。

メタ理論の自然数\(m\)に対し、ペアノ算術の項\(t_m\)は再帰的な方法で\(\textrm{FOL}'\)の項として定義されているため、それは\(A\)の定める1階述語論理の項でもある。それを\(t_m\)の像と呼ぶ。\(A_{\textrm{PA}}\)における\(\{t_m \mid m \in \mathbb{N}\}\)の論理式は全て\(r_{1,k}\)への制限によって\(A\)の論理式へ翻訳される。以下にペアノ算術の内包の例を挙げる。

ペアノ算術に内包されたペアノ算術

\(A_{\textrm{PA}}\)自身への\(A_{\textrm{PA}}\)の包含はいかなる\(r_{1,k}\)によっても定めることが出来る。このような自明な包含以外にも、\(A_{\textrm{PA}}\)を等価な論理式に少し変更することで\(A_{\textrm{PA}}\)の項を全て「\(1\)ずらして」埋め込むことも可能である。これは\(1\)以上の自然数全体の集合が再びペアノの公理を満たすことから容易に確認できる。

ZFC集合論に内包されたペアノ算術

\(A_{\textrm{ZFC}}\)で表現される空集合と自然数全体の集合の定義文をそれぞれ\(\emptyset\)と\(\omega\)で略記し、定義による拡大の標準記法を用いて項のように書く。\(A_{\textrm{ZFC}}\)に\(\textrm{FOL}'\)の論理式 \begin{eqnarray*} & & c_0 = \emptyset \\ & & \forall x_0(r_{1,0}(x_0) \leftrightarrow (x_0 \in \omega)) \\ & & \forall x_0(r_{1,0}(x_0) \to (f_{1,0}(x_0) = x_0 \cup \{x_0\}) \\ & & \forall x_0(r_{1,0}(x_0) \to (f_{2,0}(x_0,c_0) = x_0)) \\ & & \forall x_0(\forall x_1((r_{1,0}(x_0) \wedge r_{1,0}(x_1)) \to (f_{2,0}(x_0,f_{1,0}(x_1)) = f_{1,0}(f_{2,0}(x_0,x_1))))) \\ & & \forall x_0(r_{1,0}(x_0) \to (f_{2,1}(x_0,c_0) = c_0)) \\ & & \forall x_0(\forall x_1((r_{1,0}(x_0) \wedge r_{1,0}(x_1)) \to (f_{2,1}(x_0,f_{1,0}(x_1)) = f_{2,0}(f_{2,1}(x_0,x_1),x_0)))) \end{eqnarray*} を\(\wedge\)で結合したものを\(A_{\textrm{ZFC}+\textrm{PA}}\)と置くと、\(c_0,f_{1,0},f_{2,0},f_{2,1},r_{1,0}\)のいずれも含まない\(\textrm{FOL}'\)の論理式が\(A_{\textrm{ZFC}}\)を公理として証明可能であることと\(A_{\textrm{ZFC}+\textrm{PA}}\)を公理として証明可能であることは同値である。実際、\(\omega\)が自然な構造についてペアノ算術のモデルをなすため、この拡大が通常の1階述語論理の定義による拡大で実現されるが容易に確認できる。従って\(A_{\textrm{ZFC}+\textrm{PA}}\)はZFC公理系と等価な公理系であり、\(r_{1,0}\)によってペアノ算術を内包させることが出来る。

f(n)の定義

コード化された\(\textrm{FOL}\)の記述を見やすく書き直すと、自然数\(n\)に対して\(f(n)\)は「\(\textrm{FOL}\)の\(n\)文字以下のある論理式\(A\)と\(\textrm{FOL}'\)の\(n\)文字以下のある論理式\(P\)が存在して『\(A\)はペアノ算術を内包し、\(A_{\textrm{ZFC}}\)が無矛盾ならば\(A\)が無矛盾であり、\(P\)に出現する\(\textrm{FOL}\)の変項記号\(x_k\)であって\(\forall\)で束縛されていないものがただ1つ存在し、\(P\)に出現する\(x_k\)であって\(\forall\)で束縛されていないものを全て\(t_m\)の\(A\)での像\(t\)に置き換えた\(\textrm{FOL}'\)の論理式と\(\textrm{FOL}'\)の論理式\(\forall x_k(P \to (x_k = t))\)を\(\wedge\)で結合した\(\textrm{FOL}'\)の論理式を\(Q\)とおいた時に\(\neg Q\)が\(A\)において証明可能でないような最小の自然数が\(m\)である』ような任意の自然数\(m\)」を超える最小の自然数、であった。

『』内の論理式を\(\Phi(A,P,m)\)と置く。\(n\)文字以下という制約を満たす\(A\)と\(P\)は有限個しかなく、また与えられた\(A\)と\(P\)に対して\(\Phi(A,P,m)\)を満たす\(m\)は、その最小性から一意である。従って、\(\Phi(A,P,m)\)を満たすような\(n\)文字以下の\(A\)と\(P\)が存在するような\(m\)は有限個しかなく、それら全てを超える最小の自然数\(f(n)\)は確かに存在する。これにより巨大関数\(f\)が定義される。

なお、\(A\)への\(A_{\textrm{PA}}\)の埋め込み\(r_{1,k}\)自体は\(\Phi(A,P,m)\)の主張に明示的に出現しない。単にペアノ算術を内包できれば何でもよく、包含自体の性質は用いていないためである。となるとそもそもペアノ算術を包含する必要すらないのだが、ペアノ算術を包含しないとどうせ十分大きな\(m\)を表現しないと推測される。例えば\(A_{\textrm{PA}}\)を埋め込めないが相対無矛盾であるような\(A\)として、任意の\(m \in \mathbb{N}\)に対して\(t_0 = t_m\)が証明可能であるものが構成できるが、そのような\(A\)に対して\(\Phi(P,A,m)\)を満たす\(m\)は、その最小性から\(0\)となる。同様に、\(A_{\textrm{ZFC}}\)との相対無矛盾性が課されているがそれを課さなくても良く、矛盾している場合は単に\(\Phi(A,P,m)\)を満たす\(m\)は存在しなくなるため、\(f(n)\)の定義に影響しない。

外部リンク

• 西宮 七南-解説channel, ゆっくりと学ぶ巨大数論～最小の証明を書けなくても戦え数～, YouTube.