集合论中的类克莱瑟-列维定理（英文）

作者：米夏尔·拉特延; 舒双爽

来源：逻辑学研究, 2023, 16(03): 36-52.

克莱瑟与列维(1968)曾作过一个著名的表征皮亚诺算术反射原则(RFN(PA))的定理。该定理将RFN(PA)与超限归纳原则TI(ε0)联系起来;后者即是超限归纳至序数ε0——最小的取ω-幂定点。在这篇文章中我们将此结果推广至一大部分的集合论。我们所要讨论的集合论如下所述:它们包含克里普克-普拉特克集合论(KP);追加的公理必须被限制在一定的句法复杂度内,即存在一个固定的n使得它们皆为Πn。比如说如果取任意n,句法复杂度Ξ1,Ξ2?Πn,KP+幂集+Ξ1-分离+Ξ2-收集就是一个典型的例子。现在假设T是在我们的考虑范围之内的一种集合论。我们对于T+RFN(T)的表征会以超限归纳原则TI(εΩ+1)给出,其中Ω所表示的是所有序数的类,εΩ+1则是最小的取Ω-幂定点。εΩ+1并非集合序数;其定义类似于证明论中ε0的表示系统,不同之处仅在于ω被序数之类所替换。在T中从RFN(T)推导TI(εΩ+1)的证明相当常规;其本质是根岑已证过的内容。逆命题则是更难的部分。对PA的这个方向,克莱瑟与列维使用了忒特(1965)证明算术“无反例”(no-counterexample)定理。后来克莱瑟想到使用切消法(cut elmination),而施维希滕伯格(1977)在中将其实现出来,在技术上,告诉我们无限证明的切消可以用原始递归函数实现。这些原始递归函数取值于无限证明树的某种代码(该种无限证明允许“延迟”推理,即使用ω-rule使得前提与结论一致;施维希滕伯格称之为ω-rule的非常规应用)。如何严谨而详细地定义及操作这些代码,可称是一个挑战。在这篇文章中我们将借用构造主义策梅洛-弗兰克尔集合论(CZF)中归纳定义类的技术,从而回避先前所提到的那种代码。因此——类比布赫霍兹(1977)——本文的技术要素处于集合论语境之中,其本身也是有启发意义的。通常而言,我们对T中KP以外公理所加的复杂度限制是必要的。比如说,我们的表征不能应用于T=ZF;事实上ZF已经证明TI(εΩ+1)。我们自然会联想到其它序数表示系统,比如费法曼和舒特曾使用Γ0来表征理论自主扩充的强度。如果考虑超限归纳至类似Γ0的序数表示系统类(即ΓΩ+1),怎样的反射原则对应于这种超限归纳原则,将是一个有趣的命题。