라요 수

라요 수(영어: Rayo's number)는 아구스틴 라요의 이름을 딴 가장 큰 이름있는 수로 제안된 큰 수이다. 이 수는 원래 2007년 1월 26일에 MIT의 "big number duel"에서 정의되었었다.

정의

라요 수의 정의는 다음 정의의 변형이다:

구골 이하의 기호를 사용한 집합론의 언어로 표현할 수 있는 어떤 수 보다 큰 가장 작은 수.

특히, 나중에 확인된 초기 버전의 정의에서는 "구골(10¹⁰⁰) 미만의 기호를 사용한 1차 집합론의 언어로 표현할 수 있는 어떤 수보다 큰 가장 작은 수"라고 정의되어 있었다.

이 수의 공식적인 설명은 다음의 2차 공식을 사용한다. 이 때, [φ]는 괴델수로 코딩된 공식이고 s는 변수 할당이다:

∀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 (θ)' 이고, t의 xi-변수 t'에 대해서 R([θ],t'))
)} →
R([φ],s)}

이 식이 주어지면 라요수는 다음과 같이 정의된다:

다음 특성을 가지는 모든 유한한 수 m보다 큰 가장 작은 수: 구골 미만의 기호를 사용하고 x₁만을 자유변수로 가지며 다음을 만족하는 (`Sat'의 정의에서 표현되어 있듯이) 1차 집합론의 언어의 공식 φ(x₁)이 있다: (a) m을 x₁에 할당하여 Sat([φ(x₁)],s)인 변수 할당 s가 있고, (b) 어떤 변수 할당 t에 대해서 Sat([φ(x₁)],t)이면 t는 m을 x₁으로 할당한다.