ラヨの番号

ラヨ数はメキシコの哲学教授アグスティン・ラヨにちなんで名付けられた大きな数であり、最大の命名された数であると主張されている。^{[1] [2]}もともとは2007年1月26日にMITで行われた「大きな数の決闘」で定義された。^{[3] [4]}

自然数 の Rayo 関数は、 と表記され、あらゆる有限数よりも大きく、次の特性を持つ最小の数です。 1 階集合論の言語 ( の定義で示されているように) には、 より小さい記号と を唯一の自由変数として持つ式があり、次のようになります。(a)を に割り当てる変数割り当てがあり、(b) 任意の変数割り当て に対して、 であれば、を に割り当てます。この定義は Rayo 数の元の定義によって与えられます。 ${\displaystyle n}$${\displaystyle {\mbox{Rayo}}(n)}$${\displaystyle m}$${\displaystyle \phi (x_{1})}$${\displaystyle {\mbox{土}}}$${\displaystyle n}$${\displaystyle x_{1}}$${\displaystyle s}$${\displaystyle m}$${\displaystyle x_{1}}$${\displaystyle {\mbox{Sat}}([\phi (x_{1})],s)}$${\displaystyle t}$${\displaystyle {\mbox{Sat}}([\phi (x_{1})],t)}$${\displaystyle t}$${\displaystyle m}$${\displaystyle x_{1}}$

レイヨ数の定義は次の定義のバリエーションである: ^[5]

言語が 1グーゴル以下の記号のみを使用する、一階集合論の任意の言語の式によって命名される任意の有限数よりも大きい最小の数。

具体的には、後に明確化された定義の初期バージョンでは、「グーゴル（）記号未満の第一階集合論の言語の式で命名できる任意の数よりも大きい最小の数」と書かれていました。^[4]${\displaystyle 10^{100}}$

数の正式な定義は、次の2次式を使用する。ここで、はゲーデルコード化された式であり、は変数割り当てである。^[5]${\displaystyle [\phi ]}$${\displaystyle s}$

${\displaystyle {\begin{aligned}&{\mbox{For all }}R\ \{\\&\{{\mbox{for any (coded) formula }}[\psi ]{\mbox{ and any variable assignment }}t\\&(R([\psi ],t)\leftrightarrow \\&(([\psi ]={\mbox{''}}x_{i}\in x_{j}{\mbox{''}}\land t(x_{i})\in t(x_{j}))\ \lor \\&([\psi ]={\mbox{''}}x_{i}=x_{j}{\mbox{''}}\land t(x_{i})=t(x_{j}))\ \lor \\&([\psi ]={\mbox{''}}(\neg \theta ){\mbox{''}}\land \neg R([\theta ],t))\ \lor \\&([\psi ]={\mbox{''}}(\theta \land \xi ){\mbox{''}}\land R([\theta ],t)\land R([\xi ],t))\ \lor \\&([\psi ]={\mbox{''}}\exists x_{i}\ (\theta ){\mbox{'' and, for some an }}x_{i}{\mbox{-variant }}t'{\mbox{ of }}t,R([\theta ],t'))\\&)\}\rightarrow \\&R([\phi ],s)\}\end{aligned}}}$

この式から、レイヨ数は次のように定義される: ^[5]

あらゆる有限数よりも大きく、次の性質を持つ最小の数値です。1 階集合論の言語 ( の定義で示されているように) には、 グーゴル未満の記号と を唯一の自由変数とする式があり、次のようになります。(a)を に割り当てる変数割り当てがあり、(b) 任意の変数割り当て に対して、 であれば、を に割り当てます。${\displaystyle m}$${\displaystyle \phi (x_{1})}$${\displaystyle {\mbox{Sat}}}$${\displaystyle x_{1}}$${\displaystyle s}$${\displaystyle m}$${\displaystyle x_{1}}$${\displaystyle {\mbox{Sat}}([\phi (x_{1})],s)}$${\displaystyle t}$${\displaystyle {\mbox{Sat}}([\phi (x_{1})],t)}$${\displaystyle t}$${\displaystyle m}$${\displaystyle x_{1}}$

直感的に、ラヨ数は次のように形式言語で定義されます。

• ${\displaystyle {\mbox{''}}x_{i}\in x_{j}{\mbox{''}}}$および は原子式です。${\displaystyle {\mbox{''}}x_{i}=x_{j}{\mbox{''}}}$
• が式である場合、 は式です (の否定)。${\displaystyle \theta }$${\displaystyle {\mbox{''}}(\neg \theta ){\mbox{''}}}$${\displaystyle \theta }$
• および が式である場合、 は式です (との論理積)。${\displaystyle \theta }$${\displaystyle \xi }$${\displaystyle {\mbox{''}}(\theta \land \xi ){\mbox{''}}}$${\displaystyle \theta }$${\displaystyle \xi }$
• が式であれば、 は式です (存在量化)。${\displaystyle \theta }$${\displaystyle {\mbox{''}}\exists x_{i}(\theta ){\mbox{''}}}$

括弧を削除できないことに注意してください。たとえば、の代わりに と書く必要があります。 ${\displaystyle {\mbox{''}}\exists x_{i}((\neg \theta )){\mbox{''}}}$${\displaystyle {\mbox{''}}\exists x_{i}(\neg \theta ){\mbox{''}}}$

この言語では、欠けている論理接続詞を表現することが可能です。例えば、次のようになります。

• 選言：として。${\displaystyle {\mbox{''}}(\theta \lor \xi ){\mbox{''}}}$${\displaystyle {\mbox{''}}(\neg ((\neg \theta )\land (\neg \xi ))){\mbox{''}}}$
• 含意:として。${\displaystyle {\mbox{''}}(\theta \Rightarrow \xi ){\mbox{''}}}$${\displaystyle {\mbox{''}}(\neg (\theta \land (\neg \xi ))){\mbox{''}}}$
• 二条件文: as 。${\displaystyle {\mbox{''}}(\theta \Leftrightarrow \xi ){\mbox{''}}}$${\displaystyle {\mbox{''}}(\neg ((\neg (\theta \land \xi ))\land (\neg ((\neg \theta )\land (\neg \xi ))))){\mbox{''}}}$
• 全称量化:として。${\displaystyle {\mbox{''}}\forall x_{i}(\theta ){\mbox{''}}}$${\displaystyle {\mbox{''}}(\neg \exists x_{i}((\neg \theta ))){\mbox{''}}}$

定義は、この言語で自由変数1 つだけを持つ式、具体的にはに関するものです。長さ を持つ式がを満たす場合、かつ が有限のフォン ノイマン順序数と等しい場合、そのような式は の「Rayo 文字列」であり、 は記号で「Rayo 名付け可能」であるといいます。次に、は 記号で最大 の で Rayo 名付け可能なすべての数より大きい最小のものとして定義されます。 ${\displaystyle x_{1}}$${\displaystyle n}$ ${\displaystyle x_{1}}$ ${\displaystyle k}$${\displaystyle k}$${\displaystyle k}$${\displaystyle n}$${\displaystyle {\mbox{Rayo}}(n)}$${\displaystyle k}$${\displaystyle n}$