最小の証明を書けて戦え数p進大好きbotが2018年3月21日に考案した東方巨大数である[1]。第2回東方巨大数に投稿され、審査期間中に審査員による解析が終了しなかったため殿堂入りとなった。

定義

形式言語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 個の項 (t1, ..., ta) を用いて f(t1, ..., ta) と表されるもののいずれかである。
  2. FOLの「論理式」とはFOLの文字列であって、ある自然数 a と FOL_{a,引数関係記号} の元 r と a 個の項 (t1, ..., ta) を用いて r(t1, ..., ta) と表されるものか、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 に対し、ペアノ算術の項 tn を以下のように定める。

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

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

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

その他

p進大好きbotは当初 f(n) が定義から自然に計算規則まで定まると思い込んでいたが、実は f(n) の計算可能性は疑わしいものであることが後に判明した。同日にp進大好きbotは同一の FOL の定義を用いて「f(n) を計算不可能関数になるように」定義した 最小の証明を書けなくても戦え数 も定義しているが、この記事の f(n) 自体も計算可能性が保証されていないため、最小の証明を書けて戦え数は実質最小の証明を書けなくても戦え数の下位互換である。つまり最小の証明を書けて戦え数は最小の証明を書けなくても戦え数で上から抑えられる(そして計算不可能巨大数の範疇ではあまり大きくない)計算不可能巨大数である。

出典

特に記載のない限り、コミュニティのコンテンツはCC-BY-SAライセンスの下で利用可能です。