巨大数庭園数

巨大数庭園数 (large number garden number) とは、P進大好きbotが2019年12月20日に幻想巨大数2に投稿した巨大数名の略名である^[1]。2023年5月時点で、定義されている中で最も大きい巨大数であると予想されている^[2]。また、幻想巨大数2 のFHLASR部門でmrnaが選出している。

正式名称は、

さあ盟友、ついに巨大数庭園の完成だ！　この庭園の機能を説明しよう。まず１つ目は住所と間取り図の判定機能。文字列を読み込むと、それがどの箱庭の住所を表しているかやどの箱庭で再現可能な巨大数庭園の間取り図なのかを自動で判定してくれるんだ。次に２つ目が間取り図の解析機能。箱庭の住所を指定してそこで再現可能な巨大数庭園の間取り図を読み込むと、その庭園が生み出せる巨大数を教えてくれるのさ。そして肝心の３つ目の機能が巨大数の生成機能。ひとたび自然数を入力すると、それを文字数の上限とした範囲内にある全文字列を探索し、それぞれを住所と間取り図の判定機能に読み込ませることで箱庭ごとに再現可能な間取り図のみを残して列挙し、更に間取り図の解析機能に読み込ませることでそれらが生み出せる巨大数を入手し、それら全てをまとめ上げることで新たな巨大数を生み出せるんだ！　え？　それで本当に巨大な数が得られるのかって？　相変わらず盟友は疑り深いなあ。でもいいさ、この巨大数庭園自体の間取り図がここにある。これを解析機能に読み込ませれば、どれほど巨大な数を生み出せるのかを教えてくれるからね。え？　この間取り図の文字数？　そんなものを知って何になるんだい？

である。長いため略名で進める。

定義[]

P進大好きbotのブログ^[1]に定義が載っている。

解説[]

定義を見ても訳がわからないと思うので、ここでは幻想巨大数2でP進大好きbotと巨大数庭園数を審査したmrnaとのやりとりを参考に解説をする^[3]。

言語[]

表示をデスクトップ版に切り替えて数式を表示する。

言語\(L\)は\(i\)を自然数としたとき\(x_i,∈,U\)だけであり、これに\(∃, ¬, →\)を組み合わせて論理式を考える。\(∀, ∧, ∨, =\)等はこれらの組み合わせで定義される。例えば\(P∨Q\)は\((¬P)→Q\)と表せる。

\(ZF\)公理系を言語\(L\)で書いたものが\(ZF_L\)である。

形式言語[]

言語\(┌L┐\)は\(L\)よりも構造の多い言語を\(ZF_L\)で作った順序数を文字として\(ZF_L\)内で構成された言語である。また、\(┌L┐\)で\(ZFC\)を構築したのが\(ZFC_{┌L┐}\)である。

\(\textrm{Parameter}(c):=(\textrm{Constant},c)\)である。例えば\(\textrm{Parameter}(\Omega_{I+1})=(\textrm{Constant},\Omega_{I+1})=(6,\Omega_{I+1})\)になる。

\(\textrm{Interpret}(p)\)は\((6,c)\)の形をしている\(p\)の第二成分を取り出す関数である。つまり、\(c\)を出力する関数である。

一般の言語に対し、構造\(M\)とは集合\(M\)と言語の関数記号に対応する\(M\)の関数と、言語の関係記号に対応する\(M\)の関係の組である。例えば、算術の言語\((0,S,+,×)\)ならその構造\(M\)とは集合\(M\)と何らかの元\(c_0∈M\)と何らかの写像\(f_S:M→M\)と\(f_+:M×M→M\)と\(f_×:M×M→M\)の組\((M,c_0,f_S,f_+,f_×)\)のことである。これにより\(┌L┐\)の論理式は全て\(M\)で置き換える事ができ、\(┌L┐\)の論理式というハリボテな文字列から\(M\)に関する論理式という実際の論理式を得ている。

構造\(M\)の領域とは構造\(M\)の組の内、集合のことである。算術の場合、構造\((A,c_0,f_S,f_+,f_×)\)の領域とは\(A\)である。

言語\(┌L┐_{|M|}\)は言語\(┌L┐\)に\(\{(6,c)|c∈|M|\}\)を追加した言語である。しかしこの状態では言語\(┌L┐_{|M|}\)の\((6,c)\)という形に対して\(|M|\)の元を割り当てる方法が無いため\(┌L┐_{|M|}\)構造は\(M\)と見なせない。そこで\((6,c)\)を\(c\)にする写像を与えることで\(|M|\)の元に割り当てる方法が得られたので\(┌L┐_{|M|}\)構造\(M\)を得れる。これにより、\(┌L┐\)構造から\(┌L┐_{|M|}\)構造に拡張している。

代入[]

\(\textrm{Symbol}\)は\(┌⊥┐,┌⇒┐,┌¬┐,┌∃┐,┌L┐\)の集まりである。また\(\textrm{Symbol}\)の元たちは\(\omega^4\)より小さい順序数で書かれているので\(\textrm{Symbol}⊂\omega^4\)と表せる。そして\(\textrm{Formula}\)は\(\textrm{Symbol}\)の記号列である言語\(┌L┐\)で作れる論理式全体の集合である。

\(\textrm{New}(S)\)は\(S\)に出てこない\(┌x_i┐\)の添え字\(i\)の中で一番小さいものを返す関数である。

\((P)[t/x]\)は\(P\)における\(x\)の自由な出現への\(t\)の代入を表す。例えば関数記号\(f\)に対して\(f(x,y)[t/x]\)は\(f(t,y)\)のことで、関係記号\(R\)に対して\(R(x,y,z)[t/x]\)は\(R(t,y,z)\)のことである。

ただし、\((∃y(R(x,y,z)))[t/x]\)の様に存在量化文でありかつ\(t\)に\(┌L┐\)の変項記号\(y\)が出現する場合は単に\(∃y(R(t,y,z))\)とせず\(R(x,y,z)\)にも\(t\)にも現れない変数\(\textrm{New}(\{R(x,y,z),t,x\})=w\)を使って\((∃w(R(x,y,z)[w/y]))[t/x]\)とする。また代入操作は言語に属する１つ１つの記号に対して適用されるだけで、添え字の中身には適応されない。

形式論理[]

\(\textrm{Symbol}\)は\(\textrm{Symbol}⊂\omega^4\)であり、\(\omega^4\)の元は一意な\(a_0,a_1,a_2,a_3∈\mathbb{N}\)を用いて\(\omega^3×a_3+\omega^2×a_2+\omega^1×a_1+\omega^0×a_0\)と表せるため、\(\mathbb{N}^{<\omega}\)の元である配列\((a_0,a_1,a_2,a_3)\)に対応する。よって\(\textrm{Symbol}\)の元は\(\mathbb{N}^{<\omega}\)の元と対応する。

\(\textrm{Encode}\)は素因数分解の一意性を利用した、自然数の配列を１つの自然数に変換するものである。この\(\textrm{Encode}\)により\(\textrm{Symbol}\)の記号列である\(┌L┐\)論理式\(P\)を\(\mathbb{N}^{<\omega}\)の元に対応でき、更にもう一度\(\textrm{Encode}\)を用いることで\(\mathbb{N}\)の元とも対応することができる。この\(\mathbb{N}\)の元が\(\textrm{MetaCode}(P)\)である。

\(\textrm{Formalize}(n)\)とは\(ZF_L\)という集合論の自然数である\(n\)の定義文（\(0\)に\(1\)を\(n\)回足したもの）である\(ZFC_{┌L┐}\)の論理式のことである。\(\textrm{Formalize}(0)\)なら\(¬∃┌x_1┐(┌x_1┐∈┌x_0┐)\)になる。また\(\textrm{Formalize}(n)\)の論理式の自由変数は\(┌x_0┐\)のみである。

\(\textrm{Code}(P):=\textrm{Formalize}(\textrm{MetaCode}(P))\)である。つまり、\(┌L┐\)論理式\(P\)に対応する自然数の定義文である\(ZFC_{┌L┐}\)の論理式を出力している。よって\(\textrm{Code}(P)\)とは\(┌x_0┐\)は\(\textrm{MetaCode}(P)\)の定式化であるということになる。

\(\overline{ZFC}_{┌L┐}\)は\(ZFC_{┌L┐}\)に\(\{\textrm{Henkin}_{i,P}|i<\omega∧P∈\textrm{Formula}\}\)、つまり\(\omega\)より小さい\(i\)と\(\textrm{Formula}\)の元\(P\)について、「\(P\)を満たす\(x_i\)が存在するならば、\(x_0 = \textrm{MetaCode}(P)\)（の形式化）とすると論理式\(P\)に現れる自由変数\(x_i\)を\(Θ(x_0)\)に置き換えた論理式が成り立つ」という公理を追加した公理系である。

理論[]

von Neumann階層は宇宙に記述されている。\(x∈V_\alpha\)である必要十分条件は\(x⊂V_\beta\)を満たす\(\beta<\alpha\)が存在することである。\(V_0\)ならそのような\(\beta\)は存在しないため\(V_0=∅\)になり、\(V_1\)は\(x∈V_1⇔x⊂V_0=∅⇔x=∅\)なので\(V_1=\{∅\}\)になる。ちなみに\(V_2=\{∅,\{∅\}\}\)になる。

\(X⊨P\)で構造\(X\)は論理式\(P\)を満たすであり、\(X\)は\(P\)を満たすとは「\(|X|\)を構造\(X\)の領域としたとき論理式\(P\)の\(∀x\)等を\(∀x∈|X|\)等で置き換えたものが真である」である。つまり\(U1\)とは「任意の順序数\(x_0\)に対し構造\(U(x_0)\)は論理式\(\overline{ZFC}_{┌L┐}\)を満たす」という公理である。

\(X\)は\(P\)のモデルであるとは、いかなる\(Q∈P\)に対しても\(X⊨ Q\)（つまり構造\(X\)は\(Q\)を満たす）となる。任意の順序数\(\alpha\)に対して\(U(\alpha)\)は\(ZFC_{┌L┐}\)のモデルであることは\(U1\)の公理より自明である。そのため、\(┌L┐\)構造\(U(\alpha)\)となる。

構造\(U(\alpha)\)における\(┌U┐\)の解釈とは構造\(U(\alpha)\)の領域を\(|U(\alpha)|\)としたとき、言語\(┌L┐\)の関数記号である\(┌U┐\)に対応する関数\(|U(\alpha)|→|U(\alpha)|\)があってこれが\(┌U┐\)の解釈である。ここで、\(U2\)は「任意の順序数\(x_0\)と\(x_1∈x_0\)に対し\(U(x_0)\)における\(┌U┐\)解釈した関数と\(U(x_1)\)は一致する」という公理である。また、\(U3\)は「任意の順序数\(x_0\)に対してある順序数\(x_1\)が存在し構造\(U(x_0)\)の領域\(|U(x_0)|\)と\(V_{x_1}\)が一致するかつ任意の\((x_2,x_3)∈V_{x_1}^{2}\)に対し関係\(x_2┌∈┐^{U(x_0)}x_3\)と\(x_2∈x_3\)が同値である」という公理である。

そして、\(ZF_L\)公理系に公理\(U1,U2,U3\)を追加した公理系こそが\(T\)である。

埋め込み[]

モデル\(M=(|M|,...)\)が推移的とは任意の\(x∈|M|\)と任意の\(y∈x\)に対して\(y∈|M|\)が成り立つことであり、それによって\(ZFC\)の\(\mathbb{N}\)と\(ZF_L\)の\(\mathbb{N}\)と同一のものになる。よって\(ZFC\)で定義ができる巨大数は全て\(T\)で構築ができる。他にもP進大好きbotが作成した\(MK_+\)集合論との対応もあるがここでは割愛する。

巨大関数[]

\(\textrm{Definable}(x_0,x_1,x_2)\)は\(x_0\)と\(x_1\)が自然数で\(x_2\)に論理式が入る。\(\textrm{CNF}(x_1)\)によって順序数が生成される。

自然数\(n\)を代入すると\(i∈n\)かつ\(P∈\textrm{Formula}\)かつ\(\textrm{MetaCode}(P)∈n\)かつ\(\textrm{Definable}(m,i,P)\)を満たす\(i,P\)が存在するような\(m∈\mathbb{N}\)の総和を出力するのが\(f\)である。\(n\)によって\(i\)と\(P\)が有限に決まるのて、\(m\)が有限個決まる。

この時、\(f^{10}(10↑^{10}10)\)が巨大数庭園数である！！ちなみに\(↑\)は矢印表記である。

大きさ[]

P進大好きbotは、理論Tは2階ZFC集合論もMK+集合論も内包するため、\(f\)はRayo関数よりも著しく強く、十分大きな入力値での\(f\)の各値は対応するMK+集合論を対角化した計算不可能巨大数よりも著しく大きいと予想している。

出典[]

↑ ^1.0 ^1.1 p進大好きbot, 高階集合論を超えた1階述語論理, 巨大数研究 Wiki ユーザーブログ.
↑ 西宮七南-解説channel, ゆっくりと学ぶ巨大数論～巨大数庭園数～, YouTube.
↑ 幻想巨大数2でのmrnaとのやりとり