查看“︁用户:U3Vzc3liYWth”︁的源代码

果糕的页面。

<math>\mathbf{L}_a \prec \mathbf{L}_{a+1} \Longrightarrow a</math> 是 <math>\Pi^1_0</math>-反射。

'''理论'''

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

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