라요 수

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

정의

라요 수의 정의는 다음 정의의 변형이다:^[5]

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

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

이 수의 공식적인 설명은 다음의 2차 공식을 사용한다. 이 때, [φ]는 괴델수로 코딩된 공식이고 s는 변수 할당이다:^[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 (θ)' 이고, t의 xi-변수 t'에 대해서 R([θ],t'))
)} →
R([φ],s)}

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

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

각주

1. “CH. Rayo's Number”. The Math Factor Podcast. 2014년 3월 24일에 확인함. 
2. Kerr, Josh (2013년 12월 7일). “Name the biggest number contest”. 2016년 3월 20일에 원본 문서에서 보존된 문서. 2014년 3월 27일에 확인함. 
3. Elga, Adam. “Large Number Championship” (PDF). 2019년 7월 14일에 원본 문서 (PDF)에서 보존된 문서. 2014년 3월 24일에 확인함. 
4. Manzari, Mandana; Nick Semenkovich (2007년 1월 31일). “Profs Duke It Out in Big Number Duel”. 《The Tech》. 2014년 7월 16일에 원본 문서에서 보존된 문서. 2014년 3월 24일에 확인함. 
5. Rayo, Augustin. “Big Number Duel”. 2014년 3월 24일에 확인함.