リトルビッゲドン

リトルビッゲドン (Little Bigeddon) は集合論の言語を拡張した巨大数である。Googology Wiki のユーザーEmlightened によって、2017年1月5日に定義された。リトルビッゲドンはビッグフットよりも大きい。

リトルビッゲドンは「2つのビッゲドンの中で小さい方」であり、大きい方のビッグビッゲドンはサスクワッチと名付けられた。

定義

リトルビッゲドンは、集合論の言語に階数変数と３項真理述語を加えた言語 \(\mathcal L = \{\in,T\}\) によって定義される。

通常の集合論の記法によって、以下のように定義する。

\begin{eqnarray*} a = \langle b,c\rangle &\leftrightarrow& a=\{\{b,b\},\{b,c\}\} \\ a = \langle b,c,d\rangle &\leftrightarrow& a=\langle \langle b,c\rangle ,d \rangle \\ a = \langle b,c,d,e\rangle &\leftrightarrow& a=\langle \langle b,c,d \rangle ,e \rangle \\ On(a) &\leftrightarrow& \forall b\in a(\cup b\in a \wedge\forall c\in b(\cup c \in b)) \end{eqnarray*}

真理述語にはパラメーターの3つの変数があり、1つ目（コード変数）は述語のゲーデル数化によるエンコード、２つ目（階数変数）は階数、３つ目（パラメータ）はパラメータを自由変数番号に当てはめる関数である。\(T(a,\beta,c)\) は \(T_\beta(a,c)\) とも表記できる。述語は階数でランク分けされているため、真理述語が低いランクの真理述語を呼び出す、といったようなことができる。すなわち、\(T_\beta\) は \(\alpha<\beta\) の真理述語 \(T_\alpha\) を使う式のみ決定できる。たとえば、ある \(\phi\) に対して \(\forall \alpha<\beta (T_\alpha(\ulcorner\phi(\alpha)\urcorner,c)\) とするような量化をすることもできる。

パラメータのない式を以下のようにゲーデル数化することで \(\in V_\omega\) の集合へと変換できる（ここで \(i<\omega, j<\omega, k<\omega\)）。

\begin{eqnarray*} \ulcorner x_i = x_j \urcorner &=& \langle 0, i, j \rangle \\ \ulcorner x_i \in x_j \urcorner &=& \langle 1, i, j \rangle \\ \ulcorner T(x_i, x_j,x_k) \urcorner &=& \langle 2, i, j,k \rangle \\ \ulcorner \varphi \wedge \psi \urcorner &=& \langle 3, \ulcorner \varphi \urcorner, \ulcorner \psi \urcorner \rangle \\ \ulcorner \lnot\varphi \urcorner &=& \langle 4, \ulcorner \varphi \urcorner \rangle \\ \ulcorner \forall x_i\varphi \urcorner &=& \langle 5, i, \ulcorner \varphi \urcorner \rangle \\ \ulcorner \forall_R x_i\varphi \urcorner &=& \langle 6, i, \ulcorner \varphi \urcorner \rangle \end{eqnarray*}

ここで、いくつかの変数を暗黙のうちに2種類の異なった型に分けている。それは、階数変数に対する量化をある型のみに制限したいためである。そして、\(\forall_R\) は階数変数を量化するための記号である。

そしてさらに、エンコードされたパラメータのない式における（使用されている）自由変数 \(\texttt{fr}(\cdot)\) 、束縛変数 \(\texttt{bd}(\cdot)\) 、階数変数 \(\texttt{rk}(\cdot)\) を、次のように帰納的に特定する。

• \(\texttt{fr}(\ulcorner x_i = x_j \urcorner) = \texttt{fr}(\ulcorner x_i \in x_j \urcorner)= \{i, j\}\)
• \(\texttt{fr}(\ulcorner T(x_i, x_j, x_k) \urcorner) = \{i, j, k\}\)
• \(\texttt{fr}(\ulcorner \varphi \wedge \psi \urcorner) = \texttt{fr}(\ulcorner \varphi \urcorner) \cup \texttt{fr}(\ulcorner \psi \urcorner)\)
• \(\texttt{fr}(\ulcorner \lnot \varphi \urcorner) = \texttt{fr}(\ulcorner \varphi \urcorner)\)
• \(\texttt{fr}(\ulcorner \forall x_i\varphi \urcorner) = \texttt{fr}(\ulcorner \forall_R x_i\varphi \urcorner) = \texttt{fr}(\ulcorner \varphi \urcorner) \setminus \{i\}\)

• \(\texttt{bd}(\ulcorner x_i = x_j \urcorner) = \texttt{bd}(\ulcorner x_i \in x_j \urcorner) = \texttt{bd}(\ulcorner T(x_i, x_j, x_k) \urcorner) = \emptyset\)
• \(\texttt{bd}(\ulcorner \varphi \wedge \psi \urcorner) = \texttt{bd}(\ulcorner \varphi \urcorner) \cup \texttt{bd}(\ulcorner \psi \urcorner)\)
• \(\texttt{bd}(\ulcorner \lnot \varphi \urcorner) = \texttt{bd}(\ulcorner \varphi \urcorner)\)
• \(\texttt{bd}(\ulcorner \forall x_i\varphi \urcorner) = \texttt{bd}(\ulcorner \forall_R x_i\varphi \urcorner) = \texttt{bd}(\ulcorner \varphi \urcorner) \cup \{i\}\)

• \(\texttt{rk}(\ulcorner x_i = x_j \urcorner) = \texttt{rk}(\ulcorner x_i \in x_j \urcorner) = \emptyset\)
• \(\texttt{rk}(\ulcorner T(x_i, x_j, x_k) \urcorner) = \{j\}\)
• \(\texttt{rk}(\ulcorner \varphi \wedge \psi \urcorner) = \texttt{rk}(\ulcorner \varphi \urcorner) \cup \texttt{rk}(\ulcorner \psi \urcorner)\)
• \(\texttt{rk}(\ulcorner \lnot \varphi \urcorner) = \texttt{rk}(\ulcorner \forall x_i\varphi \urcorner) = \texttt{rk}(\ulcorner \forall_R x_i\varphi \urcorner) = \texttt{rk}(\ulcorner \varphi \urcorner)\)

有効な（パラメータのない）式 \(\texttt{form}\) を、次のように帰納的に定義する。

• \(\texttt{form} = \cup_{n<\omega} form_n\)
• \(form_0 = \{\langle 0, i, j \rangle: \wedge i+j<\omega\} \cup \{\langle 1, i, j \rangle: \wedge i+j<\omega\} \cup \{\langle 2, i, j, k \rangle: \wedge i+j+k<\omega\}\)
• \(form_{n+1} = form_n \cup \{\ulcorner \varphi \wedge \psi \urcorner, \ulcorner \lnot\varphi \urcorner : \varphi, \psi \in form_n\} \) \( \cup \{\ulcorner \forall x_i\varphi \urcorner: i\in \texttt{fr}(\ulcorner\varphi\urcorner)\setminus \texttt{rk}(\ulcorner\varphi\urcorner) \wedge \ulcorner\varphi\urcorner \in form_n\} \) \( \cup \{\ulcorner \forall_R x_i\varphi \urcorner: i\in \texttt{fr}(\ulcorner\varphi\urcorner)\cap \texttt{rk}(\ulcorner\varphi\urcorner) \wedge \ulcorner\varphi\urcorner \in form_n\}\)

最後に、 \(T\) の公理を定義する必要がある。

• \( T(a,b,c)\leftrightarrow[a\in \texttt{form} \wedge On(b)\) \( \wedge \forall d\in c(\exists e\exists f(d=\langle e,f\rangle)\wedge\forall e [\exists!f(d=\langle e,f\rangle)\) \( \wedge\forall f(d=\langle e,f\rangle \rightarrow [e\in \texttt{fr}(a)\wedge(e\in\texttt{rk}(a)\rightarrow f\in b)])])\) \(\wedge (\exists d\in\omega\exists e\in\omega[a=\ulcorner d=e\urcorner\wedge c(d)=c(e)]\) \(\vee\exists d\in\omega\exists e\in\omega[a=\ulcorner d\in e\urcorner\wedge c(d)\in c(e)]\) \(\vee\exists d\in\omega\exists e\in\omega\exists f\in\omega[a=\ulcorner T(d,e,f)\urcorner\wedge T(c(d),c(e),c(f))]\) \(\vee\exists d\in \texttt{form}\exists e\in \texttt{form}[a=\ulcorner d\wedge e\urcorner\wedge T(d,b,c)\wedge T(e,b,c)]\) \(\vee\exists d\in\texttt{form}[a=\ulcorner \lnot d\urcorner\wedge \lnot T(d,b,c)]\) \(\vee\exists d\in\omega\exists e\in \texttt{form}[a=\ulcorner \forall x_de\urcorner\wedge\forall f(T(e,b,c\cup\{\langle d,f\rangle\}))]\) \(\vee\exists d\in\omega\exists e\in \texttt{form}[a=\ulcorner \forall_Rx_de\urcorner\wedge\forall f\in b(T(e,b,c\cup\{\langle d,f\rangle\}))])]\)

リトルビッゲドンは、言語\(\mathcal L = \{\in,T\}\) で \(\exists! a(\varphi(a))\wedge \varphi(k)\) すなわち「\(\varphi(a)\) が真であるような \(a\) がただ1つ存在し、\(\varphi(k)\) が真である」が真となるような、階数が \(12\uparrow\uparrow 12\) 以下の1変数式 \(\varphi\) が存在するような最大の \(k\) である。