ラヨ数
直観的には、ラヨ数は形式言語で次のように定義される:
"xi∈xj" と "xi=xj" は原子論理式である。
θ が式の際に、 "(~θ)" は式( θ の否定)である。
θ と ξ が式の際に、"(θ∧ξ)" は式( θ と ξ の連言)である。
θ が式の際に、 "∃xi(θ)" は式( θ の存在量化)である。
括弧を削除することは許可されていないことに注意が必要である。例えば、"∃xi(~θ)" では無く "∃xi((~θ))" と書かなくてはならない。
欠落している論理接続詞(英語版)をこの言語で表現することは可能である。例えば:
論理和: "(θ∨ξ)" は "(~((~θ)∧(~ξ)))" と同等。
論理包含(含意): "(θ⇒ξ)" は "(~(θ∧(~ξ)))" と同等。
二条件(英語版): "(θ⇔ξ)" は "((~(θ∧ξ))∧(~((~θ)∧(~ξ))))" と同等。
全称記号: "∀xi(θ)" は "(~∃xi((~θ)))" と同等。
この定義は、この言語の式の 1 つしかない自由変数、 x1 に関するものである。 x1 が有限の フォン・ノイマン順序数(英語版) k と 長さ n の式が同値の際、その様な式は k の "ラヨ文字列" であり、k は n 個の記号で "ラヨ命名可" であると言える。
ラヨ数(ラヨすう、英: Rayo's number)とはアグスティン・ラヨ(スペイン語版)にちなんで名付けられた巨大数であり、彼の手掛けた最大の数と主張されている 。これは元々2007年1月26日にマサチューセッツ工科大学 (MIT) にて行われたイベント「巨大数決闘(big number duelもしくはLarge Number Championship)」にて定義された。