拉约数

拉约数（英语：Rayo's number），是一个由阿古斯丁·拉约（Agustín Rayo）所创造并命名的大数。这个数在当时比其他任何数都来得大（后来出现一个叫做BIG FOOT的大数比它更大），就算是葛立恒数，跟拉约数比起来也是微不足道的。这个数是在麻省理工学院在2007年1月26日举办的一场“大数战斗”中被定义的。

定义

拉约数最初被定义为：

符合“大于任何使用集合论语言，并用不超过古戈尔个符号所能表示的数”的最小数

后来它被重新定义为“符合‘大于任何使用一阶逻辑语言，并用不超过古戈尔个符号所能表示的数’的最小数”。

这个数的正式定义使用了二阶逻辑，在下式中，$[\phi ]$为哥德尔编号，而$s$则代表一个可被赋值的变数：

∀R {
{for any (coded) formula [ψ] and any variable assignment t
(R([ψ], t) ↔
(([ψ] = `x_i ∈ x_j' ∧ t(x_1) ∈ t(x_j)) ∨
([ψ] = `x_i = x_j' ∧ t(x_1) = t(x_j)) ∨
([ψ] = `(∼θ)' ∧ ∼R([θ], t)) ∨
([ψ] = `(θ∧ξ)' ∧ R([θ], t) ∧ R([ξ], t)) ∨
([ψ] = `∃x_i (θ)' and, for some an xi-variant t' of t, R([θ], t'))
)} →
R([φ], s)}