大数花园数

大数花园数（英语：The Large Number Garden Number，缩写：LNGN，日语：巨大数庭園数）是 $f^{10}(10{\uparrow }^{10}10)$ 大数的缩写名称。这里 $f(\cdot )$ 是超越高阶集合论的一阶理论中定义的函数。

理论

首先，通过在具有可数多个变量项符号和集合隶属关系符号 $\in$ 的一阶集合论语言中加入一个一元函数符号 $U$ 来定义语言 L。将 ZF_L 定义为属于 ZF 集合论公理的 L 公式集合。在这里，ZF_L 中理解和替换的公理模式由所有 L-公式（即可以包含 $U$ 的公式）参数化。 通过使用显式 Gödel 对应关系将可数多个常数项符号、可数多个函数符号、可数多个关系符号和一个新的一元函数符号 \Theta 添加到 L 的显式形式化中，定义一阶逻辑的形式语言 L。然后，我们用 ZFC_L 表示属于 ZFC 集合论公理的 L-公式集合，在这里，ZFC_L 中理解和替换的公理模式由所有 L-公式参数化，即公式可以包括 $U$ 的形式化，附加常数项符号，附加函数符号，附加关系符号和 $\mathrm{\Theta }$。 我们将 ${\epsilon }_0$ 和 L-公式下面的序数显式编码为 ZF_L 中的自然数，并将 Henkin 公理“如果存在满足 $P$ 的 x，则 $\mathrm{\Theta }(n)$ 满足 $P$”的形式化，对于每个变量项符号 x，每个带有代码 n 的 L-公式 $P$ 通过重复后继运算形式化为 ZFC_L，

用 ZFCH_L 表示由 Henkin 公理模式增强的理论 ZFC_L。新的函数符号 $\mathrm{\Theta }$ 起着“Henkin 常数族”的作用。请不要混淆基本理论 ZF_L 和形式化理论 ZFCH_L。用 $U1$ 表示 L-公式“对于任何序数 $\alpha$，$U(\alpha )\models {\text{ZFCH}}_{\text{L}}$”。在 $U1$ 增强的 ZFC_L 下，$U(\alpha )$ 形成了 ZFC_L 的模型，从而形成了任何序数 $\alpha$ 的 L-结构。我们用 $U^{U(\alpha )}$ 表示 $U(\alpha )$ 中 $U$ 的解释。我们用 $U2$ 表示 L-公式“对于任何序数 $\alpha$ 和任何 $\beta \in \alpha$，$U^{U(\alpha )}=U(\beta )$”，用 $U3$ 表示 L-公式“对于任何序数 $\alpha$，存在一个序数 $\beta$ 使得 $|U(\alpha )|={\text{V}}_{\beta }$，对于任何 $x\in {\text{V}}_{\beta }$ 和任何 $y\in {\text{V}}_{\beta }$，$x{\in }^{U(\alpha )}y$ 等价于 $x\in y$”，其中 ${\text{V}}_{\beta }$ 表示 von Neumann 层次。将 T 定义为 L-公式的集合 ${\text{ZF}}_{\text{L}}\cup \{U1,U2,U3\}$。

嵌入

通过给 ZFC 集合论中每个原子式 $x_i\in x_j$ 赋值 L-公式 $\{x_i\in x_j\}\wedge \{x_j\in U(0)\}$，理论 T 可以看作是 ZFC 集合论的扩展。特别是，ZFC 集合论中定义的集合 $N$ 在 $U(0)$ 处被解释为 T 的项，这与 ZF_L 下定义的项 $N$ 一致，因为 $U(0)$ 是 ZFC_L 的传递模型。因此，在 ZFC 集合论中可定义的大数也可以在 T 中定义，并形成一个大数项。此外，由于 L 承认可数无限多的常数项符号、函数符号和关系符号，因此，即使是在 ZFC 集合论中加入可数多个常数项符号、函数符号和关系符号的理论中的闭式，也可以在 $U(0)$ 处解释为 T 中的闭式。此外，通过给未排序的 MK 集合论中的每个原子公式 $x_i\in x_j$ 赋值 L-公式 $\{x_i\in x_j\}\wedge \{x_j\in U(0)\}$，理论 T 可以看作是 MK 集合论的扩展。粗略地说，$U(0)$ 在形式上起着一阶集合论宇宙的作用，$U(0)$ 的幂集在形式上起着二阶集合论和一阶类理论的宇宙的作用，它的幂集在形式上起着三阶集合论宇宙的作用。由于它们都包含在 $U(1)$ 中，因此 $U$ 正式扮演着高阶集合论宇宙的严格递增序列的角色。请注意，这种严格递增序列的存在可以在 ZFC 集合论中构造，并由 Grothendieck 宇宙公理增强，这在通常的数学中出现。

大数

显式定义一个满射映射：$\text{CNF}:N\to {\epsilon }_0$ 使用 Cantor 范式。 对于 L-公式 $P$，用 $\text{IsDefinition}(P)$ 表示 L-公式“存在一个 x，使得 $P$ 并且对于任何 $i$，$(P)[i/x]$ 意味着 $i=x$”。用 $\text{Definable}(m,i,P)$ 表示 L-公式“$i\in N$，$P$ 是 L-公式，$U(\text{CNF}(i))\models \text{IsDefinition}(P)$，$U(\text{CNF}(i))\models (P)[m/x]$”，其中 $P[/x]$ 中的 m$m$ 以显式方式被视为参数。对于 $n\in N$，将 $f(n)$ 定义为满足 $i\in N,P\in N$ 和 $\text{Definable}(m,i,P)$ 的 $m\in N$ 之和，这样，最终就有一个不可计算的大函数 $f:N\to N,n\mapsto N$。从这里开始，大数花园数是 $f^{10}(10{\uparrow }^{10}10)$。