查看“︁AOCF”︁的源代码

'''Arai's Ordinal Collapse Function（AOCF）'''是一种类[[序数坍缩函数]]。

=== 系统与公理 ===
<math>\Sigma_{N+2}^1\text{-AC+BI}</math> 表示一个二阶算术系统，它由 <math>\rm \Pi_1^1-CA_0+BI</math> 加入公理 <math>\Sigma_{N+2}^1\text{-AC}</math> 得到：<math>\forall n \exists X F(n,X) \rightarrow \exists Y \forall n F(n,Y_n)</math>，其中 <math>F(n,X)</math> 是任意的 <math>\Pi_{N+2}^1</math>-公式。

<math>\Sigma_{N+2}^1\text{-DC+BI}</math> 表示一个二阶算术系统，它由 <math>\rm \Pi_1^1-CA_0+BI</math> 加入公理 <math>\Sigma_{N+2}^1\text{-DC}</math> 得到：<math>\forall n \forall X \exists Y F(n,X,Y) \rightarrow \forall X_0 \exists Y \forall n [Y_0 = X_0 \land F(n,Y_n,Y_{n+1})]</math>，其中 <math>F(n,X,Y)</math> 是任意的 <math>\Pi_{N+1}^1</math>-公式，<math>m \in Y_n \Rightarrow (n,m) \in Y</math>，且 <math>(\cdot,\cdot)</math> 是一个双射配对函数。容易看出，公理中的公式 <math>F</math> 可以是 <math>\Sigma_{N+2}^1</math>-公式。

集合论 <math>{\rm KP}\omega+\Pi_N\text{-Collection}+(V=L)</math> 的公理由 <math>{\rm KP}\omega</math>（带无穷公理的 Kripke-Platek 集合论）的公理加上以下公理组成：

* 可构成公理 <math>V=L</math>

* <math>\Pi_N\text{-Collection}</math> 公理：对于任意 <math>\Pi_N</math>-公式 <math>A(x,y)</math>，<math>\forall x \in a \exists y A(x,y) \rightarrow \exists b \forall x \in a \exists y \in b A(x,y)</math>

* <math>\Sigma_N\text{-Separation}</math> 公理：对于任意 <math>\Sigma_N</math>-公式 <math>\varphi(x)</math>，<math>\exists y \forall x (x \in y \rightarrow x \in a \land \varphi(x))</math>
* <math>\Delta_{N+1}\text{-Separation}</math> 公理：对于任意 <math>\Sigma_{N+1}</math>-公式 <math>\varphi(x)</math> 和 <math>\psi(x)</math>，<math>\forall x \in a (\varphi(x) \rightarrow \neg\psi(x)) \rightarrow \exists y \forall x (x \in y \rightarrow x \in a \land \varphi(x))</math>
* <math>\Sigma_{N+1}\text{-Replacement}</math> 公理：如果 <math>\forall x \in a \exists !y \varphi(x,y)</math>，那么存在一个函数 <math>f</math>，其定义域 <math>\mathrm{dom}(f)=a</math>，使得 <math>\forall x \in a \varphi(x,f(x))</math> 对每个 <math>\Sigma_{N+1}</math>-公式 <math>\varphi(x,y)</math> 成立。

=== <math>\Pi_N\text{-Collection}</math> 公理 ===

==== 引理 2.1 ====
'''引理 2.1''' <math>{\rm KP}\omega+\Pi_N\text{-Collection}</math> 可证以下每一条：

# <math>\Sigma_N\text{-Separation}</math>
# <math>\Delta_{N+1}\text{-Separation}</math>
# <math>\Sigma_{N+1}\text{-Replacement}</math>

'''证明''' 我们将证明对于 <math>\Sigma_N</math>-公式 <math>\varphi \equiv \exists y \theta(x,y)</math>（其中 <math>\theta</math> 是 <math>\Pi_{N-1}</math>-公式），集合 <math>\{ x \in a : \varphi(x) \}</math> 存在。由逻辑知，<math>\forall x \in a \exists y (\exists z \theta(x,z) \rightarrow \theta(x,y))</math> 成立。应用 <math>\Pi_N\text{-Collection}</math>，我们可以找到一个集合 <math>b</math>，使得 <math>\forall x \in a \exists y \in b (\varphi(x) \rightarrow \theta(x,y))</math>。换句话说，<math>\{ x \in a : \varphi(x) \} = \{ x \in a : \exists y \in b \theta(x,y) \}</math>。

<math>\Delta_{N+1}\text{-Separation}</math> 可以从 <math>\Sigma_N\text{-Separation}</math> 推得，证明方法参见文献 [3] 第 17 页定理 4.5（∆-分离公理）。

<math>\Sigma_{N+1}\text{-Replacement}</math> 可以从 <math>\Delta_{N+1}\text{-Separation}</math> 推得，证明方法参见文献 [3] 第 17 页定理 4.6（Σ-替代公理）。

□

==== 引理 2.1 的一些解释 ====
Q: collection是 任意x∈A存在y φ(x,y)→存在B 任意x∈A 存在y∈B φ(x,y) 并不能够保证B里面没有多余的元素 所以真的能推出separation吗？collection并不能够保证没有多余的元素 只能保证想要的元素都在里面

A: 应用Πn-Collection后得到的集合b确实可能包含多余的元素（即，对于某些x ∈ a，b中可能包含y使得θ(x, y)不成立，但这些y不影响最终的集合等价性）。给定Σn公式φ(x) ≡ ∃y θ(x, y)，其中θ是Π_{n-1}公式。通过逻辑等价，有∀x ∈ a ∃y (φ(x) → θ(x, y))。应用Πn-Collection后，存在集合b，使得∀x ∈ a ∃y ∈ b (φ(x) → θ(x, y))。这导致{x ∈ a : φ(x)} = {x ∈ a : ∃y ∈ b θ(x, y)}。分析φ(x)的真假行为：如果φ(x)为真：则存在y使得θ(x, y)成立，因此∃y ∈ b θ(x, y)也为真（因为b包含了必要的见证y）；如果φ(x)为假：则对所有y，θ(x, y)都不成立，因此∃y ∈ b θ(x, y)也为假（即使b中有多余的y，但θ(x, y)对这些y都不成立）。因此，φ(x)为真当且仅当∃y ∈ b θ(x, y)为真，这意味着：<math>\{x \in a : \phi(x)\} = \{x \in a : \exists y \in b \theta(x, y)\}</math>。等价性成立，无论b中是否有多余元素。多余元素不影响集合定义，因为集合只关心是否存在y ∈ b满足θ(x, y)，而不关心b中是否有不相关的y。

Q: ∏ncoll+Δ0sep→∑nsep?所以{x∈a 存在y∈b θ(x,y)}为什么不需要∏_(n-1)-sep?

A: 在证明中，集合{x ∈ a : ∃y ∈ b θ(x, y)}的形成并不显式需要Π_{n-1}-Separation。这是因为：公式ψ(x) ≡ ∃y ∈ b θ(x, y)具有有界量词（y ∈ b），且b是集合。θ是Π_{n-1}公式，因此ψ(x)在计算复杂度上是Σ_n公式（因为∃y ∈ b将复杂度提升至Σ_n，但有界量化）。在KPω + Πn-Collection的背景下，这个集合的形成可以通过现有公理（Δ0-Separation和Πn-Collection）完成，无需更强分离。具体形成方式：由于b是集合，我们可以考虑笛卡尔积a × b（在KP中，Δ0-Separation保证a × b存在）。定义关系：<math>R = \{ (x, y) \in a \times b : \theta(x, y) \}</math>。R的形成需要分离公理，但θ是Π_{n-1}公式，因此R的定义依赖于公式的复杂度。如果n = 1，θ是Δ0，则R可直接由Δ0-Separation形成。如果n > 1，则我们需要确保分离复杂度可处理。在KP中，Πn-Collection结合Δ0-Separation足以证明Σn-Separation（包括此步骤）。标准证明使用复杂度归纳：基始n=0：Σ0-Separation是Δ0-Separation，已包含在KP中；归纳步n>0：假设较低复杂度分离（如Σ_{k}-Separation for k < n）可用，则Σn-Separation可证。对于ψ(x) ≡ ∃y ∈ b θ(x, y)：它等价于{x ∈ a : ∃y (y ∈ b ∧ θ(x, y))}。由于y的量化有界于b，并且θ是Π_{n-1}，这个公式的复杂度受限于Σn。使用Δ0-Separation和集合a × b，我们可以间接定义R（必要时通过有界量词处理），然后投影得到域：<math>\{x \in a : \exists y \in b \theta(x, y)\} = \text{dom}(R)</math>。在KP中，给定集合R（有序对的集合），dom(R)可以通过Δ0-Separation定义，因为量词"∃y ∈ b"有界，"θ(x, y)"的复杂度由Πn-Collection和较低分离处理。因此，在KPω + Πn-Collection中，集合{x ∈ a : ∃y ∈ b θ(x, y)}可以直接形成，无需额外Π_{n-1}-Separation。证明中的步骤是自洽的。

Q: 将y∈b变成x θ(x,y)然后将没有θ(x,y)的y变成0 然后再删掉0? 问题来了 我们无法保证没有添加新的元素的 所以如此收集也是有问题

A: 这个方法在理论上是可行的，但并不必要，原因如下：在集合论中，这种方法类似于使用替代公理（Replacement）定义一个部分函数：如果θ(x, y)成立，则映射y到x；否则映射到0。然后，移除0元素即可得到所需集合。但这需要显式的分离公理来形成中间集合（如{x : θ(x, y)}或{y : not θ(x, y)}），并可能引入复杂性。更重要的是，在KPω + Πn-Collection框架下，原有的证明已经通过有界量词和等价性简化了问题，无需此额外步骤。引入0或默认值反而可能增加不必要的复杂度。

'''引理 2.1.a''' <math>\Sigma_2\text{-Collection}</math> 可证 <math>\Pi_1\text{-Separation}</math> 

'''证明''' 给定集合 <math>A</math> 和 <math>\Pi_1</math>-公式 <math>\psi(x) \equiv \forall y \varphi(x,y)</math>，其中 <math>\varphi</math> 是 <math>\Delta_0</math>。目标是证明集合 <math>S = \{x \in A : \forall y \varphi(x,y)\}</math> 存在。

<math>\psi(x)</math> 的否定是 <math>\neg \psi(x) \equiv \exists y \neg \varphi(x,y)</math>，这是一个 <math>\Sigma_1</math>-公式。定义 <math>T = \{x \in A : \exists y \neg \varphi(x,y)\}</math>。这是 <math>S</math> 的补集，因为 <math>S = \{x \in A : \forall y \varphi(x,y)\} = A \setminus \{x \in A : \exists y \neg \varphi(x,y)\} = A \setminus T</math>。因此，如果 <math>T</math> 存在，则 <math>S = A \setminus T</math> 可以通过差集得到。令 <math>\theta(x,y) \equiv \neg \varphi(x,y)</math>，<math>\theta</math> 是 <math>\Delta_0</math>。应用 <math>\Sigma_1\text{-Collection}</math>：考虑类，对每个 <math>x \in A</math>，如果 <math>\exists y \theta(x,y)</math>，则存在这样的 <math>y</math>。<math>\Sigma_1\text{-Collection}</math> 保证：存在集合 <math>C</math>，使得对所有 <math>x \in A</math>，如果 <math>\exists y \theta(x,y)</math>，则存在 <math>y \in C</math> 使得 <math>\theta(x,y)</math> 成立。由 <math>\Delta_0\text{-Separation}</math>，集合 <math>T</math> 存在。因此差集 <math>S = A \setminus T = \{x \in A : x \notin T\}</math>，由 <math>\Delta_0\text{-Separation}</math>，集合 <math>S</math> 存在。

□

'''引理 2.1.b''' <math>\Sigma_N\text{-Separation}</math> 和 <math>\Pi_N\text{-Separation}</math> 等价。

'''证明''' 设 <math>\varphi(x)</math> 是 <math>\Pi_N</math>-公式，<math>\neg \varphi(x)</math> 是 <math>\Sigma_N</math>-公式。由 <math>\Sigma_N\text{-Separation}</math>，集合 <math>\{x \in A : \neg \varphi(x)\}</math> 存在。则 <math>\{x \in A : \varphi(x)\} = A \setminus \{x \in A : \neg \varphi(x)\}</math>，由 <math>\Delta_0\text{-Separation}</math>，差集存在。类似，设 <math>\psi(x)</math> 是 <math>\Sigma_N</math>-公式，则 <math>\neg \psi(x)</math> 是 <math>\Pi_N</math>。由 <math>\Pi_N\text{-Separation}</math>，<math>\{x \in A : \neg \psi(x)\}</math> 存在，则 <math>\{x \in A : \psi(x)\} = A \setminus \{x \in A : \neg \psi(x)\}</math>，由 <math>\Delta_0\text{-Separation}</math> 得到。因此，<math>\Sigma_N\text{-Separation}</math> 和 <math>\Pi_N\text{-Separation}</math> 在 <math>\Delta_0\text{-Separation}</math> 的系统中等价。

□

==== 引理 2.2 - 2.3 ====
'''引理 2.2''' 对于每个 <math>\Sigma^1_{N+1}</math>-公式 <math>F(n, a, Y)</math>，存在集合论语言中的一个 <math>\Sigma_N</math>-公式 <math>A_\Sigma(n, a, Y)</math>，使得对于定义的 <math>F_\Sigma(n, a, Y) :\Leftrightarrow \exists d[Ad(d) \land Y \in d \land A_\Sigma^d(n, a, Y)]</math>，下列等价关系在系统 <math>\rm KPl^r</math> 中可证：

<math>{\rm KPl^r} \vdash n, a \in \omega \land Y \subset \omega \to \{F^{set}(n, a, Y) \leftrightarrow F_\Sigma(n, a, Y)\}</math>

'''引理 2.3''' 对于二阶算术语言中的每个句子 <math>A</math>，有：

<math>\Sigma^1_{N+2}\text{-DC} + \text{BI} \vdash A \Rightarrow \text{KP}\omega + \Pi_N\text{-Collection} + (V = L) \vdash A^{set}</math>

'''证明''' 根据量词定理（定理 2.2），对于一个 <math>\Pi^1_{N+1}</math>-公式 <math>F(n, X, Y)</math>（其中 <math>n \in \omega, X \subset \omega</math>），其集合论翻译 <math>F^{set}(n, X, Y)</math> 等价于一个 <math>\Pi_N</math>-公式 <math>\varphi(n, X, Y)</math>。现在只需证明如下结论：对于一个 <math>\Pi_N</math>-公式 <math>\varphi(n, X, Y)</math>，如果假设 <math>\forall n \in \omega \forall X \subset \omega \exists Y \subset \omega \varphi(n, X, Y)</math> 成立且给定 <math>X_0 \subset \omega</math>，那么存在一个函数 <math>f</math> 满足 <math>\text{dom}(f) = \omega</math> 且 <math>\forall n \in \omega [f(0) = X_0 \land \phi(n, f(n), f(n+1))]</math>。

在 (V = L) 的可构造宇宙公理下，我们通过归纳法证明：对于任意的 <math>k \in \omega</math>，存在唯一的子集序列 <math>(Y_n)_{n<k} \subset \omega</math> 使得 <math>\forall n < k [\phi(n, Y_n, Y_{n+1}) \land \forall Z <_L Y_{n+1} \neg \phi(n, Y_n, Z)]</math> 成立。然后，利用 <math>\Sigma_{N+1}\text{-Replacement}</math>，我们可以选取一个函数 <math>g</math> 满足 <math>\text{dom}(g) = \omega</math> 且 <math>\text{rng}(g) \subset {^{<\omega}\!P(\omega)}</math>，使得对于任意 <math>k \in \omega</math>，<math>g(k)</math> 是那个唯一的序列 <math>(Y_n)_{n<k} \in {^k\!P(\omega)}</math>，并满足 <math>Y_0 = X_0</math>。最后，定义函数 <math>f(n) = (g(n+1))(n)</math> 即为所求的函数。

□

==== 引入 <math>S_{\mathbb{I}_N}</math> ====
接下来我们证明 <math>\text{KP}\omega + \Pi_N\text{-Collection} + (V = L)</math> 包含于一个集合论理论 <math>S_{\mathbb{I}_N}</math>。理论 <math>S_{\mathbb{I}_N}</math> 的语言为 <math>\{\in, \Omega\} \cup \{St_i \mid 0 < i \leq N\}</math>，其中 <math>St_i</math> 是一元谓词常元，<math>\Omega</math> 是个体常元。<math>St_i(\alpha)</math> 表示 <math>\alpha</math> 是 <math>i</math>-稳定序数，<math>\Omega</math> 表示最小的递归正则序数 <math>\omega_{CK}^1</math>。<math>S_{\mathbb{I}_N}</math> 的公理由 <math>\text{KP}\omega</math> 的公理添加以下公理得到。这里，<math>\Delta_0(\{St_i \mid 0 < i < k\})</math>-公式指语言 <math>L_k = \{\in, \Omega\} \cup \{St_i \mid i < k\}</math> 中的有界公式。

记 <math>ON</math> 为所有序数的类。对序数 <math>\alpha</math>，<math>\alpha^{\dagger i}</math> 表示大于 <math>\alpha</math> 的最小 <math>i</math>-稳定序数。一个后继 <math>i</math>-稳定序数是指形如 <math>\alpha^{\dagger i}</math> 的序数（其中 <math>\alpha</math> 为任意序数）。注意，最小的 <math>i</math>-稳定序数 <math>0^{\dagger i}</math> 是一个后继 <math>i</math>-稳定序数。定义 <math>SSt_i(\alpha) \iff \exists \beta (\alpha = \beta^{\dagger i}), LSt_i(\alpha) \iff \forall \beta < \alpha (\beta^{\dagger i} < \alpha) \quad (\alpha > 0)</math>。

<math>S_{\mathbb{I}_N}</math> 的公理：

# 构造性公理 <math>V = L</math>，以及关于 <math>\Omega</math> 递归正则性的公理：<math>\Omega \in ON</math>，<math>\omega < \Omega</math>，且 <math>\Omega</math> 上的 <math>\Delta_0</math>-收集公理模式。
# <math>\Delta_0(\{St_i \mid 0 < i \leq N\})</math>-收集公理：对每个 <math>\Delta_0(\{St_i \mid 0 < i \leq N\})</math>-公式 <math>\theta</math>（允许出现谓词 <math>St_i</math>），有：<math>\forall x \in a \exists y \, \theta(x, y) \to \exists b \forall x \in a \exists y \in b \, \theta(x, y)</math>。注记：<math>\Sigma_1(\{St_i \mid 0 < i \leq N\})</math>-收集公理可由该公理推出。
# <math>\forall \alpha \exists \kappa [\alpha < \kappa \land St_N(\kappa)]\quad(1)</math>
# 对每个 <math>i + 1 \leq N</math>，<math>SSt_{i+1} \subset LSt_i \cap St_i</math>：<math>St_{i+1}(\mathbb{S}) \to \left[\forall \alpha < \mathbb{S} \exists \sigma < \mathbb{S} (\alpha < \sigma \land St_i(\sigma))\right] \land St_i(\mathbb{S}) \quad(2)</math>。其中 <math>St_0(x) \iff (x = x)</math>。这里 <math>\alpha^{\dagger i} > \alpha</math> 表示大于 <math>\alpha</math> 的最小 <math>i</math>-稳定序数（<math>0 < i \leq N</math>）。
# 对 <math>0 < i \leq N</math>，每个后继 <math>i</math>-稳定序数 <math>\sigma</math> 满足 <math>L_\sigma \prec_{\Sigma_1(\{St_j \mid j < i\})} L</math>：<math>SSt_i(\sigma) \land \varphi(u) \land u \in L_\sigma \to \varphi^{L_\sigma}(u) \quad(3)</math>，其中 <math>\varphi</math> 是语言 <math>\mathcal{L}_i = \{\in, \Omega\} \cup \{St_j \mid j < i\}</math> 中的 <math>\Sigma_1(\{St_j \mid j < i\})</math>-公式。

==== 引理 2.4-2.5 ====
'''引理 2.4''' 在 <math>S_{\mathbb{I}_N}</math> 中可证：对每个 <math>i</math>-稳定序数 <math>\sigma</math>，有 <math>L_\sigma \prec_{\Sigma_i} L</math>，即 <math>\text{SIN} \vdash \text{St}_i(\sigma) \land u \in L_\sigma \rightarrow [\varphi^{L_\sigma}(u) \leftrightarrow \varphi(u)]</math>，其中 <math>\varphi</math> 为集合论 <math>\Sigma_i</math>-公式。  

'''证明''' 在 <math>S_{\mathbb{I}_N}</math> 中展开论证。首先证明：对语言 <math>\mathcal{L}_i</math> 中 <math>\Pi_1(\{St_j\}_{j<i})</math>-公式 <math>\varphi</math>，有 <math>St_i(\sigma) \land u \in L_\sigma \land \varphi(u) \rightarrow \varphi^{L_\sigma}(u) \quad(4)</math>。通过关于 <math>\sigma \leq \alpha</math> 的超限归纳法证明：<math>\varphi^{L_\alpha}(u) \rightarrow \varphi^{L_\sigma}(u)</math>。根据归纳假设，不妨设 <math>\alpha</math> 为后继序数。由公理 (1)(2)，存在 <math>i</math>-稳定序数 <math>\tau</math> 使得 <math>\tau < \alpha < \tau^\dagger_i</math>。此时 <math>\varphi^{L_{\tau^\dagger_i}}(u)</math>、<math>u \in L_\tau</math> 且 <math>\sigma \leq \tau</math> 成立。由公理 (3) 得 <math>\varphi^{L_\tau}(u)</math>，再由归纳假设得 <math>\varphi^{L_\sigma}(u)</math>。故 (4) 得证。特别地，对 1-稳定序数 <math>\sigma</math>，有 <math>L_\sigma \prec_{\Sigma_1} L</math>。

接下来定义 <math>St_{N+1}(\mathbb{I}_N) :\Leftrightarrow (0=0)</math>，并设 <math>\theta^{L_{\mathbb{I}_N}}(u) :\Leftrightarrow \theta</math>。进一步证明：对 <math>0 \leq i < k \leq N+1</math> 及 <math>\Pi_1(\{St_j\}_{j<i-1})</math>-公式 <math>\theta(u)</math>，有 <math>St_k(\sigma) \rightarrow \left[\theta^{L_\sigma}(u) \leftrightarrow \exists \kappa < \sigma \left\{St_i(\kappa) \land u \in L_\kappa \land \theta^{L_\kappa}(u) \right\} \right] \quad(5)</math>。假设 <math>St_k(\sigma)</math> 且 <math>\theta^{L_\sigma}(u)</math>。由公理 (1)(2)，存在 <math>\kappa < \sigma</math> 满足 <math>St_i(\kappa)</math> 且 <math>u \in L_\kappa</math>，从而 <math>\theta^{L_\kappa}(u)</math> 逻辑成立。反之，若存在 <math>\kappa < \sigma</math> 满足 <math>St_i(\kappa)</math>、<math>u \in L_\kappa</math> 且 <math>\theta^{L_\kappa}(u)</math>，则由 (4) 得 <math>\theta(u)</math>，进而 <math>\theta^{L_\kappa}(u)</math> 成立。

设 <math>\varphi(u) \in \Sigma_{1+n}(\{St_j\}_{j<i})</math> 且 <math>St_{i+n}(\sigma)</math>（<math>u \in L_\sigma</math>）。通过关于 <math>n</math> 的归纳，由 (5) 可知存在 <math>\Sigma_1(\{St_j\}_{j<i+n})</math>-公式 <math>\theta</math>，使得 <math>\varphi^{L_\sigma} \leftrightarrow \theta^{L_\sigma}</math> 且 <math>\varphi \leftrightarrow \theta</math>。

现在证明：当 <math>0 \leq n < N</math>、<math>St_{1+n}(\sigma)</math>、<math>\varphi \in \Sigma_{1+n}</math> 且 <math>u \in L_\sigma</math> 时，<math>\varphi^{L_\sigma}(u) \leftrightarrow \varphi(u)</math>。假设 <math>\varphi^{L_\sigma}(u)</math>。取 <math>\Sigma_1(\{St_j\}_{j<n})</math>-公式 <math>\theta</math>，使得 <math>\varphi^{L_\sigma}(u) \leftrightarrow \theta^{L_\sigma}(u)</math> 且 <math>\varphi(u) \leftrightarrow \theta(u)</math>。由 <math>\theta(u)</math> 逻辑成立，故 <math>\varphi(u)</math> 成立。反之，假设 <math>\varphi(u)</math>。则 <math>\theta(u)</math> 成立，由 (4) 得 <math>\theta^{L_\sigma}(u)</math>，从而 <math>\varphi^{L_\sigma}(u)</math> 成立。

□

'''引理 2.5''' <math>S_{\mathbb{I}_N}</math> 是 <math>\text{KP}\omega + \Pi_N\text{-Collection} + (V = L)</math> 的一个扩张。即，<math>S_{\mathbb{I}_N}</math> 能证明 <math>\Pi_N\text{-Collection}</math>。

'''证明''' 在 <math>S_{\mathbb{I}_N}</math> 中展开论证。设 <math>A(x, y)</math> 为语言中的 <math>\Pi_N</math>-公式。由公理 (1) 和引理 2.4，我们可得

<math>A(x, y) \leftrightarrow \exists \sigma \left(St_n(\sigma) \land x, y \in L_\sigma \land A^{L_\sigma}(x, y) \right) \quad(6)</math>。假设 <math>\forall x \in a \exists y A(x, y)</math>。由 (6) 式，可推出 <math>\forall x \in a \exists y \exists \sigma \left(St_n(\sigma) \land x, y \in L_\sigma \land A^{L_\sigma}(x, y) \right)</math>。由于 <math>St_n(\sigma) \land x, y \in L_\sigma \land A^{L_\sigma}(x, y)</math> 是一个关于 <math>\{St_i\}_{0 < i \leq n}</math> 的 <math>\Sigma_1</math>-公式，根据 <math>\Delta_0\text{-Collection}</math>（依赖于 <math>\{St_i\}_{0 < i \leq n}</math>），存在集合 <math>c</math> 使得 <math>\forall x \in a \exists y \in c \exists \sigma \in c \left(St_n(\sigma) \land x, y \in L_\sigma \land A^{L_\sigma}(x, y) \right)</math>。再由 (6) 式，即可得 <math>\forall x \in a \exists y \in c A(x, y)</math>。

□

=== <math>\Pi_N\text{-Collection}</math> 公理的序数系统 ===
我们在集合论 <math>\text{ZFC}(\{St_i\}_{0<i\leq N})</math> 中工作，其中每个 <math>St_i</math> 是一元谓词符号。

令 <math>St_0</math> 表示小于 <math>\mathbb{I}_N</math> 的不可数基数集合。<math>\Omega<\mathbb{I}_N</math> 是强临界数，即满足以下条件的非零序数：其在二元 Veblen 函数 <math>\varphi\alpha\beta=\varphi_\alpha(\beta)</math> 下封闭。我们假设：对所有 <math>i<N</math>，有 <math>St_{i+1} \subset St_i</math>；每个 <math>St_i</math> 是小于 <math>\mathbb{I}_N</math> 的序数的无界类；<math>St_i</math> 的最小元满足 <math>\Omega<\min\left(\bigcup_{0<i\leq N}St_i\right)</math>。谓词 <math>St_i</math> 等价于类 <math>\{\alpha\in ON:\alpha\in St_i\}</math>。<math>\alpha^{\dagger i}</math> 表示大于 <math>\alpha</math> 的最小 <math>St_i</math> 中的序数（当 <math>\alpha<\mathbb{I}_N</math> 时）；若 <math>\alpha\geq\mathbb{I}_N</math>，则定义为 <math>\mathbb{I}_N</math>。<math>\alpha^\dagger:=\alpha^{\dagger1}</math>。<math>SSt_i:=\{\alpha^{\dagger i}:\alpha\in ON\},LSt_i:=St_i\setminus SSt_i</math>。

序数 <math>\alpha>0</math> 是强临界数当且仅当 <math>\forall b, \xi < \alpha (\varphi_b(\xi) < \alpha)</math>。<math>\Gamma(\alpha)</math> 表示第 <math>a</math> 个强临界数；<math>\varepsilon(\alpha)</math> 代表大于 <math>\alpha</math> 的最小 ε 数；<math>\Gamma(\alpha)</math> 代表大于 <math>\alpha</math> 的最小强临界数。

对序数 <math>\alpha,\beta,\gamma</math>：<math>\gamma=\alpha-\beta</math> 表示 <math>\alpha=\beta+\gamma</math>；

<math>\alpha\dot{+}\beta</math> 表示当 <math>\alpha+\beta</math> 等于交换和（自然和）<math>\alpha\#\beta</math> 时的和（即 <math>\alpha=0</math>，或 <math>\alpha=\alpha_0+\omega^{\alpha_1}</math> 且 <math>\omega^{\alpha_1+1}>\beta</math>）。

变量约定：<math>u,v,w,x,y,z,\cdots</math> 代表集合；<math>a,b,c,\alpha,\beta,\gamma,\delta,\cdots</math> 代表小于 <math>\varepsilon(\mathbb{I}_N)</math> 的序数；<math>\xi,\zeta,\eta,\cdots</math> 代表小于 <math>\Gamma(\mathbb{I}_N)</math> 的序数；<math>\pi,\kappa,\rho,\sigma,\tau,\lambda,\cdots</math> 代表小于等于 <math>\mathbb{I}_N</math> 的序数。

对 <math>\mathbb{S}\in St_i \quad (i>0)</math>，序数 <math>\pi<\mathbb{S}</math> 的马洛度 <math>m(\pi)</math> 是一个有限函数 <math>f:\mathbb{I}_N\rightarrow\varphi_{\mathbb{I}_N}(0)</math>。

设 <math>\Lambda<\mathbb{I}_N</math> 为强临界数。为表示小于 <math>\varphi_\Lambda(0)</math> 的序数，引入序数函数：<math>\tilde{\theta}_b(\xi;\Lambda)<\varphi_{\mathbb{I}_N}(0)</math>（其中 <math>\xi<\varphi_\Lambda(0),b<\Lambda</math>），该函数第 <math>b</math> 个是以 <math>\Lambda</math> 为底的指数迭代，其中 <math>\tilde{\theta}_1(\xi;\Lambda)=\Lambda^\xi</math>。