拉約數（英語：Rayo's number），是一個由阿古斯丁·拉約（Agustín Rayo）所創造並命名的大數[1][2]。這個數在當時比其他任何數都來得大（後來出現一個叫做BIG FOOT的大數比它更大[3][4][5]），就算是葛立恆數，跟拉約數比起來也是微不足道的。[6][7]這個數是在麻省理工學院在2007年1月26日舉辦的一場「大數戰鬥」中被定義的。[8][9]
定義
拉約數最初被定義為：[10]
後來它被重新定義為「符合『大於任何使用一階邏輯語言，並用不超過古戈爾個符號所能表示的數』的最小數」。[9]
這個數的正式定義使用了二階邏輯，在下式中，為哥德爾編號，而則代表一個可被賦值的變數：[10]
![{\displaystyle [\phi ]}](http://wikimedia.org/api/rest_v1/media/math/render/svg/ea331bb6ec06f4426444af6f2cc1d5ed7665f6ae)
∀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)}
參考文獻
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
