查看“︁Rayo函数”︁的源代码

Rayo函数，是目前被命名的增长速度最快速的函数之一。

== 定义 ==

=== 通俗定义 ===
在集合论中我们知道，每个自然数 n 都可以用一个集合来表示，而一个一阶逻辑语句的自由变元所能够取为的值同样能够构成一个集合。因此，如果这个一阶逻辑语句所描述的集合恰好对应于一个自然数，那么我们就用这个一阶逻辑语句成功地描述了一个自然数。

通俗地说，Rayo 函数 Rayo(n) 的定义为：不能够用包含字符数为 n 的[[一阶逻辑]]语句定义的最小的自然数。

Rayo数定义为<math>\text{Rayo}(10^{100})</math>

关于 Rayo 函数，有几点值得说明一下。首先，它不是用自然语言表述出的“不能用 n个字确定的最小自然数”。例如，我们可以考虑“不能用二十个字确定的最小自然数”，这句话确定了一个自然数。但是这句话本身又少于 20 个字，因此这个数也能够用小于 20 个字来确定。因此这句话产生了悖论，我们称之为 Perry 悖论。究其原因，这种悖论是由于自然语言的模糊性导致的。相比之下，Rayo 数的规则是明确的，因此不会产生这一问题。

另外，它也与“用 n 个字符所不能得到的最小自然数”不同。因为计算机程序总是递归的，而一阶逻辑不是递归的，它的描述能力要比计算机语言强得多。尽管初看起来，一阶逻辑的语言十分低效，但是一旦字符数量增加，我们就可以利用它定义一些非常高效的函数，它们的表示能力将大得惊人。

=== 正式定义 ===
令<math>[\phi]</math>和<math>[\psi]</math>为 Gödel 编码公式，s 和 t 为变量。定义<math>\text{Sat}([\phi], s)</math>如下:

  <math>\forall R \{</math>
  {
    <math>\forall[\psi],t:R([\psi],t)\leftrightarrow([\psi]=''x_i\in x_j''\land t(x_i)\in t(x_j))</math>
                    <math>\lor([\psi]=''x_i=x_j''\land t(x_i)=t(x_j))</math>
                    <math>\lor([\psi]=''(\neg\theta)''\land\neg R([\theta],t))</math>
                    <math>\lor([\psi]=''(\theta\land\xi)''\land R([\theta],t)\land R([\xi],t))</math>
                    <math>\lor([\psi]='\exists x_i(\theta)''\land\exists t':R([\theta],t'))</math>
                    (where t′ is a copy of t with <math>x_i</math> changed)
    <math>\} \Rightarrow R([\phi],s)</math>
  }

我们称自然数 m 为 Rayo 可命名的，如果存在一个公式 <math>\phi(x_1)</math> 小于 n 个符号且<math>x_1</math>作为其唯一的自由变量满足以下性质：

# 存在一个变量赋值 s，赋值 x1 := m，使得<math>\text{Sat} ([\phi (x_1)] , s)</math>。
# 对于任何变量赋值 t，如果 <math>\text{Sat} ([\phi (x_1)] , t)</math>，则 t 必须有 <math>x_1 = m</math>。

Rayo(n) 是大于使用 n 个符号的 Rayo 可命名的所有数的最小数。

对 Rayo 函数定义的阐述如下：

# 原子公式“<math>x_a \in x_b</math>”表示第 a 变量是第 b 变量的元素。
# 原子公式<math>x_a=x_b</math>”表示第 a 变量等于第 b 变量。
# 公式 e 的公式“(<math>\neg e</math>) ”表示 e 的否定。
# 公式 e 和 f 的公式“(<math>e \land f</math>) ”表示 e 和 f 的合取（逻辑与）。
# 公式 e 的公式“<math>\exist x_a(e)</math>”意味着我们可以修改 a 变量的自由出现，即用 e 中所有集合的 V 类的另一个成员替换<math>x_a</math>使得公式 e 为真。

以上五条定义只是更加精确地给出了 ∈, =, ¬, ∧, ∃ 这五个逻辑的含义。这样我们就给出了用公式定义自然数的方法。若一个自然数是不能够以上述方式从长度为 n 的语句中定义的最小数，那么它就是 Rayo(n)。

== 取值 ==
我们有：

\begin{eqnarray*}0 & = & \{\} = (\neg\exists x_2(x_2 \in x_1)) \ \textrm{(10 symbols)} \\1 & = & \{\{\}\} = (\exists x_2(x_2 \in x_1) \land (\neg\exists x_3((x_3 \in x_1 \land \exists x_4(x_4 \in x_3))))) \ \textrm{(30 symbols)} \\2 & = & \{\{\},\{\{\}\}\} \\& = & (\exists x_2(\exists x_3((x_3 \in x_2 \land (x_2 \in x_1 \land x_3 \in x_1)))) \\& & \land (\neg \exists x_4(\exists x_2(\exists x_3((x_4 \in x_3 \land (x_3 \in x_2 \land x_2 \in x_1))))))) \ \textrm{(56 symbols)}\end{eqnarray*}

因此我们有：

<math>\begin{align}\text{Rayo}(0) &=& 0 \\\text{Rayo}(10) &\ge& 1 \\\text{Rayo}(30) &\ge& 2 \\\text{Rayo}(56) &\ge& 3 \\\end{align}</math>

这只是给出了下限，精确值是由Plain'N'Simple、Emk 和 Ytosk给出的<ref>Plain'N'Simple, [https://googology.fandom.com/wiki/User_blog:Plain%27N%27Simple/Proof_that_Rayo(n)_is_0_for_n_less_than_10 Proof that Rayo(n) is 0 for n less than 10], Googology Wiki user blog.</ref><ref>Emk, [https://googology.fandom.com/wiki/User_blog:Emk/Rayo(10)_is_exactly_1_(not_a_lower_bound) Rayo(10) is exactly 1 (not a lower bound)], Googology Wiki user blog.</ref><ref>Plain'N'Simple, [https://googology.fandom.com/wiki/User_blog:Plain%27N%27Simple/Proof_that_Rayo(n)_is_1_for_n_between_10_to_19 Proof that Rayo(n) is 1 for n between 10 and 19], Googology Wiki user blog.</ref><ref name="Yto">Ytosk, [https://googology.fandom.com/wiki/User_blog:Ytosk/Small_improvements_to_bounds_on_values_of_Rayo%27s_function Small improvements to bounds on values of Rayo's function], Googology Wiki user blog.</ref>

<math>\begin{align}\text{Rayo}(0) &=& 0 \\&\vdots& \\\text{Rayo}(9) &=& 0 \\\text{Rayo}(10) &=& 1 \\&\vdots& \\\text{Rayo}(29) &=& 1 \\\text{Rayo}(30) &\ge& 2 \\\end{align}</math>

除此之外，Ytosk还展示了<math>Rayo(88)\geq4</math>以及<math>Rayo(34+20n)>n</math>.<ref name="Yto"/>

从 2020 年 4 月开始，[[googology]]爱好者关于如何使用Rayo字符串表示数字<math>65536=2\uparrow\uparrow 4</math>以及类似的，2的指数塔，做了大量的研究。Plain'N'Simple 是第一个完成这项任务的人，表明<math>\text{Rayo}(835+96n) > 2 \uparrow\uparrow n</math>.当然，这是早期成果，还有很多改进要做。最后，通过 Plain'N'Simple、P进大好きbot 和 Ytosk 的各种努力，表明<math>\text{Rayo}(260+20n) > 2\uparrow\uparrow n</math><ref name="Yto"/>，因此我们有：

<math>\begin{align}\text{Rayo}(320) &>& 16 \\\text{Rayo}(340) &>& 65536 \\\text{Rayo}(360) &>& 2^{65536} \\\text{Rayo}(380) &>& 2^{2^{65536}} \\ \end{align}</math>

Emk 已经证明<math>\text{Rayo}(7901)>\text{S}(2^{65536}-1)</math>,其中S(n)是[[忙碌海狸函数#疯狂青蛙函数 S(n)|疯狂青蛙函数]]<ref>Emk, [https://googology.fandom.com/wiki/User_blog:Emk/A_Rayo_name_larger_than_BB(10%5E100) A Rayo name larger than BB(10^100)], Googology Wiki user blog.</ref>。然而，由于他的博客文章使用过时的 Rayo 字符串，这个下限没有应有的那么强。目前我们有<math>\text{Rayo}(7339)>\text{S}(2^{65536}-1)</math>。

== 历史 ==
2007 年，Elga 与 Rayo 在麻省理工大学进行了一场别开生面的比赛[[Big Number Duel]]，其内容是尽可能地写出一个有限的自然数。比赛的规则是两人轮流写出一个更大的数，要求不能够使用原始语义词汇，例如不能说“比迄今为止人类命名的任何数字都大的最小数字”等；且后一个被提出的数字不能够容易地由前面的数字的构造方法容易地抵达，例如不能够在前一个数字上简单地 +1 来得到更大的数字。这场比赛的获胜者是 Rayo，他在这场比赛中提出的最大数字就是著名的 Rayo 数

据信Rayo和Elga的大数对决的灵感来自斯科特·亚伦森 （Scott Aaronson） 的文章[https://www.scottaaronson.com/writings/bignumbers.html 谁能说出更大的数字？]

== 讨论 ==
为了在集合论中定义一个自然数，我们需要明确基于哪些公理进行定义。Rayo数定义中的一个问题在于，Rayo并未阐明所使用的公理。在数学中，只要我们在ZFC集合论的框架下工作，通常会省略对公理的声明。按照这一传统，许多大数研究者认为Rayo数是在ZFC集合论中定义的，或者与公理选择无关，但这种观点是错误的。

至少，由于ZFC集合论无法在[[冯诺依曼宇宙|冯·诺伊曼宇宙]]中形式化真值谓词，除非我们将Rayo数的定义解释为可证性，否则它在ZFC集合论中是不良定义的。即使我们以这种方式解释其定义，所得到的大数也不会显著大于例如<math>\Sigma(10^{100})</math>（其中<math>\Sigma</math> 为[[忙碌海狸函数]]），因为递归可枚举理论中的可证性可以通过图灵机的停机信息判定。要显著超越忙碌海狸函数，我们必须放弃可证性，转而讨论特定模型中的真值——而该模型的存在性在ZFC集合论的一致性前提下是无法被证明的。

另一方面，FOST（一阶集合论语言）本质上只是一种形式语言，根据其定义与公理系统无关——但这并不意味着Rayo数的定义也与公理无关。FOST与公理的无关联性，或者忙碌海狸函数与Rayo数基于可证性解释之间的关系，可能是导致人们误认为"Rayo数与公理无关"的主要原因。

正如Rayo在其原始描述中所述，他使用二阶集合论来形式化原始语义词汇。因此，Rayo数实际上是基于某种未明确说明的二阶集合论公理系统定义的。在不可计算的大数研究中，明确公理系统至关重要，因为只有当两个不可计算大数采用相同的定义公理时，它们之间才能进行有意义的比较。幸运的是，存在多种二阶集合论公理系统可供选择来定义Rayo数。由此可以得出结论：'''对于那些关注公理明确性的研究者来说，Rayo函数是不良定义的'''。

2020年，Rayo新增了以下关于如何处理Rayo数的说明<ref>[https://web.mit.edu/arayo/www/bignums.html A. Rayo, "Big Number Duel", 2007]</ref><blockquote>"注：哲学家有时会采用集合论的实在论解释。在这种解释下，集合论表达式具有'标准'含义，能为语言中的每个句子确定明确的真值，而无需考虑这些真值是否可能被认知（例如参见Vann McGee的这篇文章）。在竞赛期间，Adam和我默认（二阶）集合论语言采用标准解释，这保证了最终条目对应确定的数。如果该语言基于某个公理系统进行解释，最终条目就会失效。这是因为每个（一致的）公理化系统都存在非同构模型，无法保证最终条目在不同模型中对应相同的数。"</blockquote>这意味着Rayo采用了一种哲学上的"解释"方式，将集合论公式与现实中"真值"相对应——这种做法在数学上是无法形式化的，且并未涉及具体公理系统的选择。这是大数研究在数学框架之外的一种合理探索方向。然而，最后一句中的辩解（关于为何要接受这种无法形式化的"真值"）更像是一种托词：虽然数值对模型的依赖性确实存在，但这与"无效性"并无逻辑关联。

在数学中，存在许多良定义但非绝对的概念（即依赖于模型），例如满足条件<math>(CH\rightarrow n=0)\land(\neg CH\rightarrow n=1)</math>的唯一自然数n。同样在大数领域，许多数值本身就具有模型依赖性，比如忙碌海狸函数的值。值得注意的是，在"大数对决"竞赛中，从未禁止过依赖模型的数值定义，甚至允许参与者不指定公理系统。

== 引证 ==
{{默认排序:相关问题}}
[[分类:记号]]