1、Studies in Logic,Vol.16,No.3(2023):3652PII:16743202(2023)03003617KreiselLvytype Theorems for Set TheoriesMichael RathjenShuangshuang ShuAbstract.A famous result,due to Kreisel and Lvy(1968),characterizes the uniform reflection principle for Peano arithmetic,RFN(PA),in terms of the transfinite induct
2、ion principleTI(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 KripkePlatek set theory,KP,but their additional ax
3、ioms are required to be of restricted syntactic complexity,that is,thereexists a fixed n such that they are all of nform.A typical example is KP+Powerset+1Separation+2Collection with 1,2 nfor some n.ThecharacterizationofT+RFN(T)will begivenin termsofaninductionprincipleTI(+1),allowing induction up t
4、o the first class ordinal such that=,where stands for theclass of all(set)ordinals.The definition of the class ordering+1is akin to that of the ordinalrepresentationsystemfor0usedinprooftheory,wherebytheroleoftheordinal isnowplayedbytheentireclassofordinals.TheproofthatRFN(T)entailsTI(+1)overT isfai
5、rlystandardin that is uses techniques essentially developed by Gentzen.The converse entailment,though,is the hard part.In the case of PA,Kreisel and Lvy used the nocounterexample interpretationin a formalization due to Tait(1965).The idea of using a cut elimination procedure insteadis owed to Kreise
6、l and was implemented by Schwichtenberg(1977).Technically,it shows thatthecuteliminationprocedureforinfinitederivationscanbeengineeredviaaprimitiverecursivefunction for a natural(albeit quite subtle)coding of infinite derivations,which allow for delayinferences(called improper applications of the ru
7、le),where the premisses are the same as theconclusion.A mathematically rigorous and detailed account of how to work with such codesposes a considerable challenge.In this article we shall be avoiding codes for infinite derivationsentirely by utilizing a detour through a fragment of Constructive Zerme
8、loFraenkel set theory,CZF,in which general inductively defined classes can be handled without any problems.Theexposition 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 co
9、mplexity of the axioms of T that do not belong to KP isnecessary.For instance,the above characterization does not extend to ZF.Indeed,ZF provesTI(+1).Naturally,other ordinal representation systems come to mind,for instance,0,which was usedby Feferman and Schtte to characterize the strength of autono
10、mous progressions of theories.Itwould be interesting to figure out what kind of reflection principle corresponds to the inductionprinciple for the class version of 0,i.e.,+1.Received 20220319Michael RathjenDepartment of Pure Mathematics,University of Leedsm.rathjenleeds.ac.ukShuangshuang ShuDepartme
11、nt of Pure Mathematics,University of Leedsmmsshleeds.ac.ukMichael Rathjen,Shuangshuang Shu/KreiselLvytype Theorems for Set Theories371IntroductionIn the introduction to his 1939 paper(36),containing the results of his thesis,Turing explains the considerations that were the source of his work very vi
12、vidly:The wellknown theorem of Gdel 1931 shows that every systemof logic is in a certain sense incomplete,but at the same time it indicates means whereby from a system L of logic a more complete system Lmay be obtained.By repeating the process we get a sequenceL,L1=L,L2=L1,.each more complete than t
13、he preceding.Alogic Lmay then be constructed in which the provable theorems are thetotality of theorems provable with the help of the logics L,L1,L2,.Proceeding in this way we can associate a system of logic with any constructive ordinal.It may be asked whether such a sequence of logicsof this kind
14、is complete in the sense that to any problem A there corresponds an ordinal such that A is solvable by means of the logic L.I propose to investigate this question in a rather more general case,andto give some other examples of ways in which systems of logic may beassociated with constructive ordinal
15、s.The idea of transiting from a theory T to a“more complete”theory Tcan be implemented in various ways.In light of Gdels second incompleteness theorem,oneobvious move is to let Tbe T augmented by the statement Con(T),where Con(T)expresses the consistency of T.The idea of iterating such an augmentati
16、on throughthe“ordinals”calls for a constructive treatment of ordinals or rather ordinal representations.Turing used the recursive ordinals known as Kleenes O.He obtaineda remarkable result,namely that every true 01statement of number theory can beproved in a consistency progression through O(36).Tur
17、ing was also interested in true 02statements,in particular as he had demonstrated that the famous Riemann conjecture can be rendered in 02form.1For this heconsidered a stronger move from T to Tthat is nowadays called the local reflectionprinciple for T.Rfn(T)PrT()for every sentence here denotes the
18、Gdel number of while PrTstands foran arithmetized provability predicate of T.Alas,it turned out that not for all true 02statements a path through O can be found such that progressions based on iteratingRfn along this path prove.Alittlemorethan20yearslater,however,SolomonFefermanprovedanamazingcomple
19、teness theorem(13),not only for 02statements,but for all true arithmetic1However,Kreisel later showed that the Riemann hypothesis already has a 01form.38Studies in Logic,Vol.16,No.3(2023)statements.He considered a strengthening of Rfn(T)with parameters,which can beviewed as a formalized rule.RFN(T)x
20、PrT(x)(x)for every formula(x)with at most x free.2RFN(T)is known as the uniform reflection principle for T.The result alluded to is the following.Theorem(Fefermans completeness result)There is a hyperarithmetic path P withinO of length+1such that every true arithmetical statement is provable inaPTaw
21、here T0=PA and Tb1=Tb+RFN(Tb)with x 7 x 1 denoting the successoroperation of O.In 1968,Kreisel and Lvy(15)showed that RFN(PA),the uniform reflection principle for PA,is equivalent over PA to the schema of transfinite induction along 0,the first ordinal that satisfies =.In more detail,RFN(PA)is the s
22、chemaRFN(PA)=x(PrPA(x)(x)|a formula of PA with at most x freewhere we assume a standard coding for formulas as in the canonical reference34(x)is Fefermans dot notation from 12,that is,a formal version of theprimitiverecursive function which on input m outputs(Sm(0),where S is thesymbol for the succe
23、ssor function on N and S0(0):=0 and Sk+1(0):=S(Sk(0).The ordinal 0can be approached from below as follows.0=supnn,where 0=and n+1=n.Using an ordinal representation system for 0,the transfinite induction schema forordinals 0can be expressed in the language of arithmeticTI():=()()()()()|(x)a formula o
24、f PA,where stands for the ordering of the representation system.Then the theorem mentioned above reads as follows.RFN(PA)TI(0)over PA,2“RFN”signifies the“reflection principle for numbers”,which is the name of the schema used in15.We will follow standard notations as used,e.g.,in 34.Note that in set
25、theory,the phrase“reflection principle”can mean something else.Michael Rathjen,Shuangshuang Shu/KreiselLvytype Theorems for Set Theories39i.e.,PA+RFN(PA)proves all instances of TI(0),and,conversely,PA+TI(0)proves all instances of RFN(PA).This paper shows that similar results hold for set theories T,
26、which are syntactically bounded extensions of KripkePlatek set theory,KP.The proof of T+RFN(T)TI(+1)resembles Gentzens argument for showing that PA provesTI()for every 0.For the converse direction,we do not use the KreiselLvyapproach nor the one in Schwichtenbergs article(33),where in the latter the
27、 direction PA+TI(0)RFN(PA)is proved by a complicated encoding of infinitarydeductions.Instead,we take a detour through a fragment of Constructive ZermeloFraenkel set theory and draw on the realizability interpretation from 26,which deploys set recursive functions(or rather their codes)as realizers.1
28、.1Plan of the paperLet T be an extension of KP such all the axioms of T that do not belong to KPhave a fixed syntactic complexity,say n,where n is an arbitrary natural number.Moreover,we shall assume that all axioms of KP without the instances of Set Induction also have a complexity(more precisely t
29、heir prenex normal forms)that does notexceed n.Section 2 will introduce the(class)ordinal representation system OT(+1)andit will be shown that KP+RFN(KP)proves transfinite induction,TI(+1),for thisordinal representation system.As a corollary we then have T+RFN(T)TI(+1).The proof of the reversal,name
30、ly that T+TI(+1)yields RFN(T),is moredifficult.It involves a detour through an infinitary proof system,T,into which Tcan be embedded and which enables one to remove all cuts with formulas having acomplexity exceeding n.This is done in section 3.A problem,though,emerges asthe inductive definition of
31、Tprovability cannot be directly formalized in T.In KPone can carry out inductive definitions(see 6 VI.2)but this is not enough as oneneedsinductivedefinitionsentailingunversalquantifiersoverallsets.Toremedythis,we switch in section 4 to a subtheory of Constructive ZermeloFraenkel set theory,dubbed C
32、ZF,in which such definitions can be carried out with alacrity.CZFresultsfrom CZF by omitting the Subset Collection scheme.Partial cut elimination for Tturns out to be formalizable in CZF+TI(+1)+EM0,where EM0connotesthe law of excluded middle for 0formulas.To get back to the classical theoryT+TI(+1),
33、in section 5 we deploy a notion of realizability from 26 based onErecursive set functions.With it we get a realizability interpretation of CZF+TI(+1)+EM0in T+TI(+1).In the final section 6,the latter result is used toshow that T+TI(+1)RFN(T).The detour through an intuitionistic theory,that is,Heyting
34、 arithmetic with fixedpoints for strictly positive operators,was used by Buchholz(8)to overcome theobstacle of formalizing ordinal analysis in a weak metatheory.Buchholz approach40Studies in Logic,Vol.16,No.3(2023)has also been applied in 5 and 29.In this paper,however,we use this idea in a settheor
35、etic context,where CZFis the ideal theory for handling inductive definitions.Acknowledgements:The authors are grateful to the referees for very useful andinsightful comments that also changed the technical implementation of proofs in asubstantial way.2The(Class)Ordinal Representation System OT(+1)He
36、re we introduce the class ordinal representation system OT(+1),followingthe presentation in 23.But before we can define it,it is perhaps advisable to give aprecise definition of KP.2.1KripkePlatek set theoryFor the study of weak fragments of PA the 0formulas play a special role.These are formulas in
37、 which all quantifiers are of the form x t and x 2,as per usual:hx1,.,xni=hx1,hx2,.,xnii.Definition 2.1.(KP+1Set Induction)Let Ord be the class of ordinals.WesimultaneouslydefineaclassofordinalrepresentationsOT(+1)alongwithabinaryrelation on OT(+1)as follows:(1)0 OT(+1).(2)If 1 n,1,.,n Ord0,s1,.,sn
38、OT(+1)and s1 sn,thens11+snn:=hn,hs1,1i,.,hsn,nii OT(+1).(3)If s OT(+1)0,then 0 s.(4)If s=sn1+snn OT(+1)and t=t11+tkkOT(+1),then s t if one of the following holds:(i)n k and si=tias well as i=ifor 1 i n.(ii)There exists m n,k such that(a)si=tiand i=ifor 1 i m,(b)Either sm tmor sm=tmand m 0.In this wa
39、y they are isomorphic tothe initial segment of OT(+1)determined by.Lemma 2.2.Define 0:=0 and k+1:=k,where k:=k1.Then we haveKP TI(n).Proof.For details see 23 Lemma 4.5.Theorem 2.3.KP+RFN(T)TI(+1)Proof.Formalizing the proof of Lemma 2.2 ascertains thatKP x PrT(TI(x),42Studies in Logic,Vol.16,No.3(202
40、3)whence KP+RFN(T)x TI(x),hence KP+RFN(T)TI(+1)sinceKP s OT(+1)x s x.3An Infinitary Proof System for Set TheoryProof systems with infinitary rules,that is,rules with infinitely many premises,became an important tool in proof theory in the 1950s,notably through the work ofKurt Schtte(31,32).Here we i
41、ntroduce an infinitary proof system Tfor the set theory T.Sincewe will only be dealing with classical theories,we can assume that formulas are innegation normal form,i.e.,negations appear only in front of atomic formulas.Moreover,it will be assumed that the only propositional connectives are conjunc
42、tion anddisjunction.4Quantifiers come in four flavors,though,namely x,x s,x,and x s,where s is a term of the language.Bounded quantifiers are treated asquantifiers in their own right.The language of Twill contain a constant a for everyset a.On account of the infinitary rules for quantifiers it is no
43、t necessary to considerformulas with free variables henceforth by formula we will mean a formula withoutfree variables.To each such formula A we assign a complexity degree|A|,which isan element of OT(+1),as follows.Definition 3.1.For set a,let rank(a)be its settheoretic ordinal rank.(i)|a b|=max(ran
44、k(a),rank(b)+1.(ii)|A B|=|A B|=max(|A|,|B|)+1.(iii)|x aF(x)|=|x aF(x)|=max(rank(a)+3,|F(0)|+2).(iv)|xF(x)|=|xF(x)|=max(,|F(0)|+1).Note that for every 0formula A one has|A|,and for every formula B thereexists n such that|B|+n.Definition 3.2.From now on variables,.will range over elements of theclass
45、OT(+1).We will also just write instead of .We use upper case Greek letters,.for sequents,i.e.,for finite sets ofTformulas(which may be empty).If A is a formula,A stands for A.We give an inductive definition of deducibility in the theory Tconveyed byT,where,OT(+1).The idea is that “measures”the lengt
46、h of the deductionwhile is a strict upper limit on|C|for all formulas that get removed via a(Cut)inference.4Of course,none of this is important.Practically,it saves some space when introducing the rules ofT.Michael Rathjen,Shuangshuang Shu/KreiselLvytype Theorems for Set Theories43The precise defini
47、tion is as follows,where,.are assumed to be elementsof OT(+1)and is any finite set of Tformulas.(i)If A is an axiom of T,then T,A.(ii)Let a,b be sets.If a b then T,a b.If a/b then T,a/b.(iii)If there exist 0,1 such that T0,A and T1,B,then T,A B.(iv)If there exists 0 such that T0,A,then T,A B andT,B
48、A for any formula B.(v)If for all a s there exists a such that Ta,F(a),then T,x sF(x).(vi)If there exist c s and 0 such that T0,F(c),then T,x sF(x).(vii)If for all sets a there exists a such that Ta,F(a),then T,xF(x).(viii)Ifthereexistasetcand0 suchthatT0,F(c),thenT,xF(x).(ix)If there exist 0,1 such
49、 that T0,A and T1,A and|A|,then T.Theorem 3.3.If T (x1,.,xr)where(x1,.,xr)is a sequent containingexactly the free variables x1,.,xr,then there is an m (which we may computefrom the Tdeduction)such thatTm+m(s1,.,sr)for any T terms s1,.,sr.Proof.The proof is by induction on the deduction T (x1,.,xr).N
50、ote thatexcept for Set Induction all axioms of T are also axioms of T.Showing provabilityofSetInductioninTisalsostraightforward.ThisisactuallywhatTwasdesignedfor.Proofs can be found in many places,e.g.7,14,21,23,and in a lot of detail in9 Lemma 2.27.Theorem 3.4.Let n(T)be a natural number chosen suc
