霜符「フロストコラヨス」はp進大好きbotが2019年5月12日に公開した東方巨大数である[1][2]。第3回東方巨大数に投稿され、審査期間中に審査員による解析が終了せず、かつ審査員が巨大数としての価値を見出したため殿堂入りとなった。名前の由来は東方Projectの登場キャラクターであるチルノ[3]のスペルカード・霜符「フロストコラムス」とラヨ数である。
定義
以下は出典[2]からの引用である。
巨大関数
自然数で添字付けられた変項記号\(x_0,x_1,\ldots\)と引数\(2\)の関係記号\(\in\)と論理結合子\(\neg\)と\(\to\)と量化子\(\forall\)とカッコ\((\)と\()\)のみからなる\(\textrm{ZFC}\)集合論の言語を\(L\)と置く。
\(L\)の閉論理式の有限集合\(S\)と自由変項がただ１つ出現する\(L\)の論理式\(f\)の組\((S,f)\)が「\(V\)の切片で充足可能」とは、「\(\mathbb{N} \subset V_{\alpha}\)かつ\(V_{\alpha} \models S\)かつ\((V_{\alpha},n) \models f\)」を満たす順序数\(\alpha\)と\(n \in \mathbb{N}\)が存在するということである。ただし\(V_{\alpha}\)は累積的階層である。
\(V\)の切片で充足可能な組\((S,f)\)全体の集合を\(\Sigma\)と置く。写像 \begin{eqnarray*} \textrm{eval} \colon \Sigma & \to & \mathbb{N} \\ (S,f) & \mapsto & \textrm{eval}(S,f) \end{eqnarray*} を以下のように定める：
- 「\(\mathbb{N} \subset V_{\alpha}\)かつ\(V_{\alpha} \models S\)かつ\((V_{\alpha},n) \models f\)を満たす\(n \in \mathbb{N}\)が存在する」という性質を満たす最小の順序数\(\alpha\)を\(\alpha_0\)と置く。
- \(\textrm{eval}(S,f)\)は\((V_{\alpha_0},n) \models f\)を満たす最小の\(n \in \mathbb{N}\)である。
\(n \in \mathbb{N}\)に対し、\(\textrm{CoRayo}(n) \in \mathbb{N}\)を「任意の\((S,f) \in \Sigma\)に対し、\(S\)の任意の要素も\(f\)も長さが\(n \uparrow^n n\)以下であるならば、\(\textrm{eval}(S,f) < m\)である」を満たす最小の\(m \in \mathbb{N}\)と定める。
命名
\(\textrm{CoRayo}(9)\)を霜符「フロストコラヨス」と名付ける。
説明
\(\textrm{CoRayo}\)関数はラヨ関数の亜種である。本家のラヨ関数は\(\textsf{ZFC}\)公理系で定義可能でないが、\(\textrm{CoRayo}\)関数は\(\textsf{ZFC}\)公理系において定義される。
\(S\)を\(\textsf{ZFC}\)公理系の有限切片とすると、反映原理によりそれを\(V_{\alpha}\)が充足するような順序数\(\alpha\)が必ず存在する。従って\(S\)で巨大数を定義可能な論理式\(f\)は\(V_{\alpha_0}\)で一意な巨大数を定める。これにより\(\textrm{CoRayo}\)が\(\textsf{ZFC}\)公理系の各有限切片を対角化する関数となることが分かる。ただし\(V_{\alpha_0}\)での充足関係は\(V\)での真偽と一致しないため、ラヨ関数と違って巨大数の定義文\(f\)が\(\textrm{CoRayo}\)のシステムで定める巨大数は\(f\)が定める巨大数そのものとは異なりうる。それでも\(\textsf{ZFC}\)公理系で証明可能な巨大数同士の大小関係は\(\textsf{ZFC}\)公理系の有限切片でも証明可能であるため、その有限切片に対応する\(V_{\alpha_0}\)でもその大小関係が成立するので、直感的には十分大きな巨大数の定義文\(f\)に対しては十分大きな巨大数が\(\textrm{CoRayo}\)のシステムで定まる。その意味で、\(\textrm{CoRayo}\)関数はラヨ関数の\(\textsf{ZFC}\)公理系における類似と考えられる。