集合论中的类克莱瑟-列维定理

Kreisel–Lévytype Theorems for Set Theories

克莱瑟与列维(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)证明算术“无反例”(nocounterexample)定理。后来克莱瑟想到使用切消法(cut elmination),而施维希滕伯格(1977)在中将其实现出来,在技术上,告诉我们无限证明的切消可以用原始递归函数实现。这些原始递归函数取值于无限证明树的某种代码(该种无限证明允许“延迟”推理,即使用ωrule使得前提与结论一致;施维希滕伯格称之为ωrule的非常规应用)。如何严谨而详细地定义及操作这些代码,可称是一个挑战。在这篇文章中我们将借用构造主义策梅洛弗兰克尔集合论(CZF)中归纳定义类的技术,从而回避先前所提到的那种代码。因此——类比布赫霍兹(1977)——本文的技术要素处于集合论语境之中,其本身也是有启发意义的。通常而言,我们对T中KP以外公理所加的复杂度限制是必要的。比如说,我们的表征不能应用于T=ZF;事实上ZF已经证明TI(ε_(Ω+1))。我们自然会联想到其它序数表示系统,比如费法曼和舒特曾使用Γ_(0)来表征理论自主扩充的强度。如果考虑超限归纳至类似Γ_(0)的序数表示系统类(即Γ_(Ω+1)),怎样的反射原则对应于这种超限归纳原则,将是一个有趣的命题。

A famous result,due to Kreisel and Lévy(1968),characterizes the uniform reflection principle for Peano arithmetic,RFN(PA),in terms of the transfinite induction principle TI(ε_(0)),namely induction up the ordinalε_(0),which is the first ordinalαsuch thatω^(α)=α.In this article we prove a generalization of this result germane to large swathes of set theories.These set theories T are of the following kind.They comprise Kripke–Platek set theory,KP,but their additional axioms are required to be of restricted syntactic complexity,that is,there exists a fixed n such that they are all ofΠ_(n) form.A typical example is KP+Powerset+■_(1)Separation+■_(2)Collection with■_(1),■_(2)⊆Π_(n) for some n.The characterization of T+RFN(T)will be given in terms of an induction principle TI(ε_(Ω+1)),allowing induction up to the first class ordinalαsuch thatΩ^(α)=α,whereΩstands for the class of all(set)ordinals.The definition of the class orderingε_(Ω+1) is akin to that of the ordinal representation system forε_(0) used in proof theory,whereby the role of the ordinalωis now played by the entire class of ordinals.The proof that RFN(T)entails TI(ε_(Ω+1))over T is fairly standard in that is uses techniques essentially developed by Gentzen.The converse entailment,though,is the hard part.In the case of PA,Kreisel and Lévy used the nocounterexample interpretation in a formalization due to Tait(1965).The idea of using a cut elimination procedure instead is owed to Kreisel and was implemented by Schwichtenberg(1977).Technically,it shows that the cut elimination procedure for infinite derivations can be engineered via a primitive recursive function for a natural(albeit quite subtle)coding of infinite derivations,which allow for delay inferences(called improper applications of theωrule),where the premisses are the same as the conclusion.A mathematically rigorous and detailed account of how to work with such codes poses a considerable challenge.In this article we shall be avoiding codes for infinite derivations entirely by utilizing a detour through a fragment of Constructive ZermeloFraenkel set theory,CZF,in which general inductively defined classes can be handled without any problems.The exposition of this technical move in a settheoretic context,which parallels the one by Buchholz(1997)for arithmetic,is quite interesting in its own right.In general,the restriction on the complexity of the axioms of T that do not belong to KP is necessary.For instance,the above characterization does not extend to ZF.Indeed,ZF proves TI(ε_(Ω+1)).Naturally,other ordinal representation systems come to mind,for instance,Γ_(0),which was used by Feferman and Schütte to characterize the strength of autonomous progressions of theories.It would be interesting to figure out what kind of reflection principle corresponds to the induction principle for the class version ofΓ_(0),i.e.,Γ_(Ω+1).