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

Kreisel–Lévytype Theorems for Set Theories

作　　者：米夏尔·拉特延 舒双爽 Michael Rathjen;Shuangshuang Shu(Department of Pure Mathematics,University of Leeds)

机构地区：[1]利兹大学纯数学系

出　　处：《逻辑学研究》2023年第3期36-52,共17页Studies in Logic

摘　　要：克莱瑟与列维(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以外公理所加的复杂度�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

关 键 词：集合论 弗兰克尔 构造主义 普拉特 证明论 归纳定义 如下所述 克莱 

分 类 号：B81-0[哲学宗教—逻辑学]