Kreisel–Lévy type Theorems for Set Theories

Michael Rathjen Shuangshuang Shu

Abstract. A famous result,due to Kreisel and Lévy(1968),characterizes the uniform reflec tion 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 no counterexample 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 Zermelo Fraenkel set theory,CZF,in which general inductively defined classes can be handled without any problems.The exposition of this technical move in a set theoretic 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.

1 Introduction

In 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 vividly:

The well known theorem of Gödel 1931 shows that every system of logic is in a certain sense incomplete,but at the same time it indi cates means whereby from a systemLof logic a more complete sys temL′may be obtained.By repeating the process we get a sequenceL,L1=L′,L2=each more complete than the preceding.A logicLωmay then be constructed in which the provable theorems are the totality of theorems provable with the help of the logicsL,L1,L2,....Proceeding in this way we can associate a system of logic with any con structive ordinal.It may be asked whether such a sequence of logics of this kind is complete in the sense that to any problemAthere corre sponds an ordinalαsuch thatAis solvable by means of the logicLα.I propose to investigate this question in a rather more general case,and to give some other examples of ways in which systems of logic may be associated with constructive ordinals.

The idea of transiting from a theoryTto a “more complete” theoryT′can be im plemented in various ways.In light of Gödel’s second incompleteness theorem,one obvious move is to letT′beTaugmented by the statement Con(T),where Con(T)expresses the consistency ofT.The idea of iterating such an augmentation through the “ordinals” calls for a constructive treatment of ordinals or rather ordinal repre sentations.Turing used the recursive ordinals known asKleene’sO.He obtained a remarkable result,namely that every truestatement of number theory can be proved in a consistency progression through O([36]).

Turing was also interested in truestatements,in particular as he had demon strated that the famous Riemann conjecture can be rendered inform.1However,Kreisel later showed that the Riemann hypothesis already has a form.For this he considered a stronger move fromTtoT′that is nowadays called thelocal reflection principleforT.

for every sentenceθ; here ┍θ┑denotes the Gödel number ofθwhile PrTstands for an arithmetized provability predicate ofT.Alas,it turned out that not for all truestatementsθa path through O can be found such that progressions based on iterating Rfn along this path proveθ.

A little more than 20 years later,however,Solomon Feferman proved an amazing completeness theorem([13]),not only forstatements,but for all true arithmetic statements.He considered a strengthening of Rfn(T)with parameters,which can be viewed as a formalizedωrule.

for every formulaφ(x)with at mostxfree.2“RFN” signifies the “reflection principle for numbers”,which is the name of the schema used in[15].We will follow standard notations as used,e.g.,in[34].Note that in set theory,the phrase“reflec tion principle”can mean something else.RFN(T)is known as theuniform reflec tion principleforT.The result alluded to is the following.

Theorem(Feferman’s completeness result)There is a hyperarithmetic pathPwithin O of lengthωωω+1such thateverytrue arithmetical statement is provable in

whereT0=PA andTb⊕1=Tb+RFN(Tb)with1 denoting the successor operation of O.

In 1968,Kreisel and Lévy([15])showed that RFN(PA),the uniform reflection prin ciple 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 schema

where we assume a standard coding ┍·┑for formulas as in the canonical reference[34]; ┍ϕ()┑is Feferman’s dot notation from [12],that is,a formal version of the primitive recursive function which on inputmoutputs ┍ϕ(Sm(0))┑,where S is the symbol for the successor function on N and S0(0)：=0 and Sk+1(0)：=S(Sk(0)).

The ordinalε0can be approached from below as follows.

Using an ordinal representation system forε0,the transfinite induction schema for ordinalsα≤ε0can be expressed in the language of arithmetic

where

Then the theorem mentioned above reads as follows.

i.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,which are syn tactically bounded extensions of Kripke–Platek set theory,KP.The proof of T +RFN(T)⊢TI(εΩ+1) resembles Gentzen’s argument for showing that PA proves TI(α)for everyα <ε0.For the converse direction,we do not use the Kreisel Lévy approach nor the one in Schwichtenberg’s article ([33]),where in the latter the di rection PA+TI(ε0)⊢RFN(PA)is proved by a complicated encoding of infinitary deductions.Instead,we take a detour through a fragment of Constructive Zermelo Fraenkel set theory and draw on the realizability interpretation from[26],which de ploys set recursive functions(or rather their codes)as realizers.

1.1 Plan of the paper

Let T be an extension of KP such all the axioms of T that do not belong to KP have a fixed syntactic complexity,say Πn,wherenis an arbitrary natural number.Moreover,we shall assume that all axioms of KP without the instances of Set Induc tion also have a complexity(more precisely their prenex normal forms)that does not exceed Πn.

Section 2 will introduce the(class)ordinal representation system OT(εΩ+1)and it will be shown that KP+RFN(KP)proves transfinite induction,TI(εΩ+1),for this ordinal representation system.As a corollary we then have T+RFN(T)⊢TI(εΩ+1).

The proof of the reversal,namely that T+TI(εΩ+1) yields RFN(T),is more difficult.It involves a detour through an infinitary proof system,T∞,into which T can be embedded and which enables one to remove all cuts with formulas having a complexity exceeding Πn.This is done in section 3.A problem,though,emerges as the inductive definition of T∞provability cannot be directly formalized in T.In KP one can carry out Σ inductive definitions(see[6]VI.2)but this is not enough as one needs inductive definitions entailing unversal quantifiers over all sets.To remedy this,we switch in section 4 to a subtheory of Constructive Zermelo Fraenkel set theory,dubbed CZF′,in which such definitions can be carried out with alacrity.CZF′results from CZF by omitting the Subset Collection scheme.Partial cut elimination for T∞turns out to be formalizable in CZF′+TI(εΩ+1)+EM∆0,where EM∆0connotes the law of excluded middle for ∆0formulas.To get back to the classical theory T+TI(εΩ+1),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)+EM∆0in T+TI(εΩ+1).In the final section 6,the latter result is used to show that T+TI(εΩ+1)⊢RFN(T).

The detour through an intuitionistic theory,that is,Heyting arithmetic with fixed points for strictly positive operators,was used by Buchholz ([8]) to overcome the obstacle of formalizing ordinal analysis in a weak metatheory.Buchholz’approach has also been applied in[5]and[29].In this paper,however,we use this idea in a set theoretic context,where CZF′is the ideal theory for handling inductive definitions.

Acknowledgements：The authors are grateful to the referees for very useful and insightful comments that also changed the technical implementation of proofs in a substantial way.

2 The(Class)Ordinal Representation System OT(εΩ+1)

Here we introduce the class ordinal representation system OT(εΩ+1),following the presentation in[23].But before we can define it,it is perhaps advisable to give a precise definition of KP.

2.1 Kripke Platek set theory

For the study of weak fragments of PA the ∆0formulas play a special role.These are formulas in which all quantifiers are of the form∀x

KP is a subtheory of ZF consisting of the following axioms:3In some sources one finds KP axiomatized without the infinity axioms,especially when considered with urlements(see[6])while others(e.g.,[10])count Infinity among the axioms of KP.Also note that central results of[6],such as the Barwise Completeness and Compactness Theorems,are carried out in a metatheory with Infinity.Proof theoretically,KP without the Infinity axiom(as well as ZFC without Infinity)is a subtheory of Ackermann’s set theory,which is bi interpretable with PA by Ackermann’s interpretation of hereditarily finite sets in PA,and thus this case is essentially already covered by Kreisel and Lévy[15].

Proof theoretically,KP resembles PA with regard to some features.For example,it is a well known result,due to Parsons([20])and others,that the primitive recursive functions on natural numbers are exactly the class of the provably total functions of the fragment of PA wherein induction is restricted to Σ1formulas.In set theory we may define primitive recursive functions on sets as well,and by[22]Theorem 1.2,a set functionFis primitive recursive iff it is provably total in KP with(set)induction restricted to Σ1formulas.

2.2 OT(εΩ+1)

We define,as usual,the ordered pair〈x,y〉ofx,yby〈x,y〉={{x},{x,y}}and prove that〈x,y〉=〈z,w〉iffx=zandy=w.This gives rise to define orderedn–tuples forn>2,as per usual:

Definition 2.1.(KP−+Σ1Set Induction) Let Ord be the class of ordinals.We simultaneously define a class of ordinal representations OT(εΩ+1)along with a binary relation ◁on OT(εΩ+1)as follows:

OT(εΩ+1)as well as ◁are defined by a Σ+inductive definition with closure ordinalω(cf.[6]VI).Such definitions can already be formalized in KP−+Σ1Set Induction(see e.g.[23,p.267]).

Note that the sums in(2)are purely formal,i.e.,they do not refer to the usual ordi nal addition.Also note that the usual set theoretic ordinals are injected into OT(εΩ+1)via the mapping 00 andΩ0αforα>0.In this way they are isomorphic to the initial segment of OT(εΩ+1)determined by Ω.

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 that

whence KP+RFN(T)⊢∀x∈ωTI(Ωx),hence KP+RFN(T)⊢TI(εΩ+1)since KP⊢∀s ∈OT(εΩ+1)∃x ∈ω s◁Ωx.□

3 An Infinitary Proof System for Set Theory

Proof 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 of Kurt Schütte([31,32]).

Here we introduce an infinitary proof system T∞for the set theory T.Since we will only be dealing with classical theories,we can assume that formulas are in negation normal form,i.e.,negations appear only in front of atomic formulas.More over,it will be assumed that the only propositional connectives are conjunction∧and disjunction∨.4Of course,none of this is important.Practically,it saves some space when introducing the rules of T∞.Quantifiers come in four flavors,though,namely∀x,∀x ∈s,∃x,and∃x ∈s,wheresis a term of the language.Bounded quantifiers are treated as quantifiers in their own right.The language of T∞will contain a constant ˙afor every seta.On account of the infinitary rules for quantifiers it is not necessary to consider formulas with free variables;henceforth by formula we will mean a formula without free variables.To each such formulaAwe assign a complexity degree|A|,which is an element of OT(εΩ+1),as follows.

Definition 3.1.For seta,let rank(a)be its set theoretic ordinal rank.

Note that for every ∆0formulaAone has|A| <Ω,and for every formulaBthere existsn ∈ωsuch that|B|<Ω+n.

Definition 3.2.From now on variablesα,β,γ,...will range over elements of the class OT(εΩ+1).We will also just writeα<βinstead ofα◁β.

We use upper case Greek letters Γ,Λ,Ξ,...forsequents,i.e.,for finite sets of T∞formulas(which may be empty).IfAis a formula,Γ,Astands for Γ∪{A}.

We give an inductive definition of deducibility in the theory T∞conveyed by

whereα,ρ ∈OT(εΩ+1).The idea is thatα“measures”the length of the deduction whileρis a strict upper limit on|C|for all formulas that get removed via a (Cut)inference.

The precise definition is as follows,whereα,ρ,...are assumed to be elements of OT(εΩ+1)and Γ is any finite set of T∞formulas.

Theorem 3.3.IfT⊢Γ(x1,...,xr)whereΓ(x1,...,xr)is a sequent containing exactly the free variables x1,...,xr,then there is an m<ω(which we may compute from theTdeduction)such that

for anyTterms s1,...,sr.

Proof.The proof is by induction on the deduction T⊢Γ(x1,...,xr).Note that except for Set Induction all axioms of T are also axioms of T∞.Showing provability of Set Induction in T∞is also straightforward.This is actually what T∞was designed for.Proofs can be found in many places,e.g.[7,14,21,23],and in a lot of detail in[9]Lemma 2.27.□

Theorem 3.4.Let n(T)be a natural number chosen such that the complexity of all axioms A ofTsatisfies|A|<Ω+n(T).Define.If

then

Proof.This is proved by the standard cut elimination procedure and can be found in the same places as for the previous result.For details as to doing this in an intu itionistic metatheory see also[9]Lemma 2.15 and Theorem 2.16.□

4 Constructive Zermelo Fraenkel Set Theory

Constructive Zermelo Fraenkel set theory,CZF,is a very important constructive set theory with remarkable properties.It was singled out by Aczel([1])as an extension as well as simplification of Myhill’s Constructive Set Theory,CST([18]).5For more on CZF see[3,4,28].CZF is a formal set theory whose language just has the primitive relation symbols∈and=for membership and equality,respectively,and only intuitionistic reasoning will be allowed.

Definition 4.1.Here are the axioms of CZF:

Strong Infinity

where we use the following abbreviations.

stands for falsum or“absurdity”.6In intuitionistic logic, ⊥is used to express negation ¬ϕ as ϕ →⊥.Crucially,one has ex falso quodlibet,i.e.,⊥→ψ for every formula ψ.

Subset Collection

for all formulasψ(x,y,u).

Strong Collection

for all formulasφ(x,y).

Set Induction

for all formulasψ(u).

For this article,only the subtheory of CZF without the Subset Collection axiom will be of relevance.7The Subset Collection axiom is native to CZF.It is perhaps the most unfamiliar axiom.It is a consequence of the Powerset axiom but does not have any proof theoretic strength as long as one adheres to intuitionistic logic.Classically,it implies the Powerset axiom.It is an extension of Myhill’s Exponentiation axiom [18].One can roughly rephrase it as follows: For all sets A,B there exists a“sufficiently large”set of multi valued functions from A to B.This fragment will be referred to by the acronym CZF′.We will also consider the theory CZF′+EM∆0,where EM∆0stands for theprinciple of excluded middle for∆0formulas,that is,φ ∨¬φfor ∆0formulasφ.The proof strength of CZF′+EM∆0is not greater than that of KP,however,adding EM∆0to CZF results in a theory whose proof theoretic strength is bigger than that of Zermelo set theory(see[25],Theorem 15.1).

Of course,we owe the reader an explanation for incorporating EM∆0.One rea son is that without it ordinals cannot be shown to be linearly ordered,and as a result it would not be possible to show that the ordering on OT(εΩ+1)is a linear ordering.It is quite possible that this problem can be circumvented by the methods of[27],section 6,making a completely constructive treatment of infinitary cut elimination possible.However,for our purposes,where the ultimate target theory is a classical one,this does not seem to provide any additional benefits.

4.1 Inductive Definitions of Classes

A very interesting aspect of CZF′is that classes can be defined inductively,re gardless of the complexity of the formula that defines the class.Here,in addition to Set Induction,the Strong Collection axiom comes into its own.

Definition 4.2.

1.We take aninductive definitionto be any class of ordered pairs.

2.If Φ is an inductive definition and〈X,a〉∈Φ then we prefer to write

and callX/aan(inference)stepof Φ,with setXofpremissesandconclusion a.

3.We associate with an inductive definition Φ the operator ΓΦon classes that assigns to each classYthe class ΓΦ(Y)of all conclusionsaof inference stepsX/aof Φ,with a setXof premisses that is a subset ofY,in other words(or rather symbols),

We define a classYto be Φclosedif ΓΦ(Y)⊆Y.

4.The classinductively defined byΦ,if it exists,is the smallest Φ closed class and will be denoted byI(Φ).

Theorem 4.3(CZF′).(Class Inductive Definition Theorem)For any inductive defi nitionΦthere is a smallestΦclosed class I(Φ).

Proof.This was proved in[2].For more details see([3],§5.1; [4],§12.1.1; [28],§1.3.7) □

5 Defining Realizability with Sets of Witnesses for Set Theory

A generalization of the notion of computability,as familiar from the context of arithmetic,to set theory is known asErecursion or set recursion.In it one makes sense of applying a seteto an arbitrary setx.It was introduced by Moschovakis([17]) and Normann ([19]); a textbook account appeared in Sacks’ book ([30]).A treatment in constructive set theory can be found in [24,26].Here we will deploy indices ofErecursive as realizers for set theoretic formulas.

Realizability semantics are a crucial tool in the study of intuitionistic theories.A notion of realizability based on indices of general set recursive functions was intro duced in[24].Below we use a crucial modification from[25,26],where a realizer for an existential statement merely provides a set of witnesses for the existential quan tifier rather than a single witness.This is important for the avoidance of the axiom of choice,for otherwise we would have to bake a universal choice function into the notion of set computable function and thus of realizability.8This problem is also familiar from functional interpretations of constructive set theory;see[11].

Definition 5.1.([25,Definition 15.7],[26,Definition 3.1]) Let(a)0=uand(a)1=vifais an ordered paira=〈u,v〉,and(a)0=(a)1=0 ifais not an ordered pair.

In the notion of realizability below,bounded quantifiers will be treated as quan tifiers in their own right,i.e.,bounded and unbounded quantifiers are treated as syn tactically different kinds of quantifiers.

We use the expressiona∅to convey that the setais inhabited,that is∃x x ∈a.

Instead of[a](b)≃cwe shall writea•b ≃c.a•f⊩wDwill be an abbreviation for∃x[a•f ≃x ∧x⊩wD].

Theorem 5.2.Let A(u1,...,ur)be a formula of set theory all of whose free variables are among u1,...,ur.If

then one can effectively construct an index of an E recursive function g such that

Proof.This is essentially the same proof as for[25]Theorem 15.2 or[26]Theorem 3.7 (where in the latter case one just ignores the truth component of that notion of realizability).The only new thing to ascertain is that all instances of TI(εΩ+1) get realized,too.This is similar to verifying realizability of Set Induction.Of course,one needs TI(εΩ+1)to hold in the target theory.□

6 The Hard Direction

The tool of realizability withErecursive functions allows us to finish the proof of the main result of this paper.

Wev will assume a Gödel numbering(or rather a Gödel set coding)of formulas of T∞,where ┍ψ┑refers to the Gödel code of a formulaψ.

Theorem 6.1.InCZF′+EM∆0+TI(εΩ+1)one can prove that9Strictly speaking,T∞deduces sequents Γ(x1,...,xr),but we allow ourselves to be sloppy by∨identifying Γ(,...,)with the formula (,..., ),i.e.,the disjunction over all formulas of Γ(,...,).

Proof.This follows from Theorems 3.3 and 3.4 since CZF′+EM∆0+TI(εΩ+1)is a background theory capacious enough to prove these theorems.□

Theorem 6.2.To save space,let x be the tuple x1,...,xr,˙x be˙x1,...,˙xr,and x ∈ω abbreviate x1∈ω,...,xr ∈ω.

There is an E recursive function f such thatT+TI(εΩ+1)proves that

Proof.In view of Theorem 6.1 and Theorem 5.2,there exists anErecursive func tiongsuch that T+TI(εΩ+1)proves that

Since the formulax ∈ω ∧PrT(┍φ(˙x)┑) is ∆0it follows by [26],Proposition 4.4 that it has a canonical realizer t,that is,

Lettingf(x)：={g(v)|v ∈t(x)}it follows from from(1)and(2)that,provably in T+TI(εΩ+1),we have

The final step we have to take amounts to verifying thatu⊩w∃η ∈OT(εΩ+1)entails thatφ(x)is true.This can be shown by induction onη(or rather the ordinal(s)provided by the realizeru).For this we shall exploit general facts about partial truth predicates.Although a consistent theory cannot have a global truth predicate,theories like PA and set theories like KP have a truth predicate TrueΠrfor the collection of Πrformulas for everyr,satisfying

whereψis a formula of complexity Πrwith at most the free variables shown.For more details see,e.g.,[35,CH.3,§20]and[6,Chap.III.1].

Lemma 6.3.Let r >n(T)and also assume that ψ(x1,...,xk)belongs toΠr.ThenT+TI(εΩ+1)proves the following:

Proof.The proof in T+TI(εΩ+1)proceeds by induction on the length of the deduc tion which is assumed to be realized byu.A realizer of Tdecides which of the inference clauses of Definition 3.2 applies.Since the ordinals assigned to the premisses are smaller,they are true by the induction hypothesis.Due to the nature of these inferences,this entails that the conclusion is also true.

One should also note that the Lemma must be proved in full generality,that is,not only for standard formulasψ(x1,...,xr)given at the metalevel,but for arbitrary(codes of)formulas.10Speaking model theoretically,in a nonstandard model of T+TI(εΩ+1)the last T∞ inference could have been a cut with a nonstandard formula.□

Theorem 6.4.T+TI(εΩ+1)⊢RFN(T).

Proof.This is the sum of Theorem 6.2,(3),and Lemma 6.3.□

The foregoing result,however,does not extend to ZF.

Theorem 6.5.ZFprovesTI(εΩ+1),and therefore is not equivalent toRFN(ZF)overZF.

Proof.Given a formulaφ(v)with one free variablev,we want to show that ZF⊢TI(εΩ+1,φ).By the reflection theorem for ZF(e.g.,[16,Ch.IV Theorem 7.4])we have

where TI(εΩ+1,φ)Vω+αresults from TI(εΩ+1,φ) by relativizing all the quantifiers toVω+α,i.e.,theω+α–th level of the von Neumann hierarchy.But surely ZF⊢∀αTI(εΩ+1,φ)Vω+α,whence ZF⊢TI(εΩ+1,φ).□

There are many more interesting ordinal representations known to proof theo rists that give rise to class induction principles in the same vein asε0does.One ordinal representation systems that comes to mind is the one for Γ0,which was used by Feferman and Schütte to characterize the strength of autonomous progressions of theories.We conjecture that the corresponding induction principle for the class ver sion of Γ0,i.e.,ΓΩ+1,can be captured via transfinite progressions of theories obtained by iterating the uniform reflection principle.