Rayo number

Rayo's number is a large number named after Agustin Rayo, who declared the largest number with his own name ^{[1] [2]} . Initially, he was given the exact definition of a “duel of large numbers” at the Massachusetts Institute of Technology on January 26, 2007 ^{[3] [4]} .

The definition of the Rayo number is a variation of the definition ^[5] :

The smallest number greater than any finite number defined by an expression in the language of set theory using symbol googol or less.

Later, the initial version of the definition was clarified, and now the definition is as follows: “The smallest number greater than any finite number that can be determined by an expression in the first order language of set theory using less than googol (10 ¹⁰⁰ ) characters” ^{[4 ]} .

The formal definition of a number uses the following second-order formula, where [φ] is the Gödel numbering formula, and s is the variable assignment ^[5] :

∀R {
{для любой (закодированной) формулы [ψ] и любой переменной 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 (θ)' и, для некоторого xi-вариантного t' от t, R([θ],t'))
)} →
R([φ],s)}

Given this formula, the Rayot number is determined as follows ^[5] :

The smallest number, greater than any finite number m with the following property: there is a formula φ (x ₁ ) in the first order language of set theory (as presented in the definition of `Sat ') with less than a googol of characters and x ₁ as the only free variable, such that (1) there is an assignment to s that defines m to x ₁ , so that Sat ([φ (x ₁ )], s) and (2) for any assignment to t if Sat ([ φ (x ₁ )], t), then t defines m to x ₁ .